environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, ORDINAL4, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL02, RLVECT_3, RMOD_2, INT_3, VECTSP_1, VECTSP_2, LOPBAN_1, MESFUNC1, REALSET1, RSSPACE, MONOID_0, SETFAM_1, VECTSP10, EC_PF_1, INT_2, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2, REALSET1, FINSEQ_1, VALUED_1, FINSEQ_4, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, RLVECT_2, INT_3, EC_PF_1, GROUP_1, VFUNCT_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, ZMODUL01;
definitions FUNCT_1, XBOOLE_0, RLVECT_1, FUNCT_2, ALGSTR_0, VECTSP_1, ZMODUL01, BINOP_1, TARSKI, VECTSP_4, VECTSP_6, VECTSP_7;
theorems FUNCT_1, FUNCT_2, INT_1, RLSUB_2, RLVECT_1, TARSKI, ZMODUL01, RLVECT_2, ZFMISC_1, RELAT_1, VECTSP_1, ALGSTR_0, EULER_1, EULER_2, EC_PF_1, VECTSP_4, VECTSP_6, NUMBERS, INT_2, MOD_3, VECTSP_7;
schemes BINOP_1, FUNCT_2, XBOOLE_0;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, VALUED_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, ZMODUL01, XXREAL_0, ALGSTR_0, INT_3, VECTSP_1, XCMPLX_0, ORDINAL1, VECTSP_4, VECTSP_7, NAT_1;
constructors HIDDEN, BINOP_2, FINSEQ_4, RELSET_1, RLVECT_2, ZMODUL01, VECTSP_4, REALSET1, FUNCT_7, INT_3, NAT_D, GCD_1, VECTSP10, ALGSTR_1, VECTSP_6, BINOP_1, VECTSP_7, VECTSP_5, PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, MEMBERED, VFUNCT_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, RELAT_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, REALSET1, ZMODUL01, BINOP_1, VECTSP_4, VECTSP_6;
expansions FUNCT_1, XBOOLE_0, RLVECT_1, FUNCT_2, STRUCT_0, ALGSTR_0, ZMODUL01, BINOP_1, TARSKI, VECTSP_4, VECTSP_6;
definition
let V be
Z_Module;
let W be
Submodule of
V;
existence
ex b1 being BinOp of (CosetSet (V,W)) st
for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W
uniqueness
for b1, b2 being BinOp of (CosetSet (V,W)) st ( for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b2 . (A,B) = (a + b) + W ) holds
b1 = b2
end;
definition
let V be
Z_Module;
let W be
Submodule of
V;
existence
ex b1 being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) st
for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b1 . (z,A) = (z * a) + W
uniqueness
for b1, b2 being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) st ( for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b1 . (z,A) = (z * a) + W ) & ( for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b2 . (z,A) = (z * a) + W ) holds
b1 = b2
end;
definition
let V be
Z_Module;
let W be
Submodule of
V;
existence
ex b1 being strict Z_Module st
( the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) )
uniqueness
for b1, b2 being strict Z_Module st the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) & the carrier of b2 = CosetSet (V,W) & the addF of b2 = addCoset (V,W) & 0. b2 = zeroCoset (V,W) & the lmult of b2 = lmultCoset (V,W) holds
b1 = b2
;
end;
Lem1:
for i being Integer holds i in the carrier of INT.Ring
definition
let p be
prime Element of
INT.Ring;
let V be
Z_Module;
existence
ex b1 being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) st
for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
b1 . (a,x) = (i mod p) * x
uniqueness
for b1, b2 being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) st ( for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
b1 . (a,x) = (i mod p) * x ) & ( for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
b2 . (a,x) = (i mod p) * x ) holds
b1 = b2
end;
Lm3:
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds
W1 is Submodule of W2 /\ W3
Lm4:
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds
W1 + W2 is Submodule of W3