environ
vocabularies HIDDEN, NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, ARYTM_3, PARTFUN1, SUPINF_2, FUNCT_5, MCART_1, ARYTM_1, CARD_1, FINSEQ_1, CARD_3, TARSKI, XXREAL_0, RLVECT_1, REALSET1, RLSUB_1, ZMODUL01, INT_1, FINSEQ_4, LATTICES, EQREL_1, PBOOLE, RLSUB_2, RMOD_2, RMOD_3, BINOM, NAT_1, INT_3, VECTSP_1, MESFUNC1, BINOP_2, MOD_2, VECTSP_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCT_5, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_1, REALSET1, FINSEQ_1, BINOP_2, XREAL_0, FINSEQ_4, STRUCT_0, ALGSTR_0, LATTICES, RLVECT_1, VECTSP_1, BINOM, GROUP_1, VECTSP_2, INT_3, VECTSP_4, VECTSP_5, MOD_2;
definitions TARSKI, STRUCT_0, ALGSTR_0, RLVECT_1, XBOOLE_0, VECTSP_1, VECTSP_4, INT_3, VECTSP_5;
theorems FUNCT_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, FINSEQ_1, ALGSTR_0, BINOM, FINSEQ_3, INT_1, RLVECT_1, LATTICES, PARTFUN1, RELSET_1, XREAL_1, VECTSP_1, VECTSP_4, VECTSP_5, INT_3, BINOP_2, GR_CY_1, MOD_2;
schemes NAT_1, BINOP_1;
registrations ORDINAL1, NUMBERS, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, SUBSET_1, INT_1, REALSET1, LATTICES, RELAT_1, ALGSTR_1, XTUPLE_0, INT_3, XCMPLX_0, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5;
constructors HIDDEN, BINOP_1, NAT_1, FUNCT_3, FUNCT_5, REALSET1, RELSET_1, GROUP_1, LATTICES, RLSUB_1, ALGSTR_1, BINOM, FINSEQ_4, VECTSP_1, INT_3, VECTSP_2, VECTSP_4, BINOP_2, MOD_2, VECTSP_5;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, ALGSTR_0, LATTICES, XBOOLE_0, REALSET1, BINOP_1, BINOM, VECTSP_4, INT_3, SUBSET_1, VECTSP_5, VECTSP_1;
expansions TARSKI, STRUCT_0, ALGSTR_0, LATTICES, XBOOLE_0, BINOP_1, VECTSP_4, VECTSP_1, INT_3, VECTSP_5;
Lm1:
for V being Z_Module holds Sum (<*> the carrier of V) = 0. V
Lm2:
for V being Z_Module
for F being FinSequence of V st len F = 0 holds
Sum F = 0. V
Lm6:
for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
Lm8:
for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1
Lm9:
for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
Lm10:
for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
Lm11:
for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
Lm12:
for V being Z_Module
for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
Lm13:
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
by VECTSP_5:27;
Lm14:
for V being Z_Module
for W1, W2, W3 being Submodule of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
Lm15:
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
Lm16:
for V being Z_Module
for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds
W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
Lm17:
for V being Z_Module
for W1, W2 being Submodule of V holds
( W1 + W2 = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) iff for v being Vector of V ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
Lm18:
for V being Z_Module
for W being Submodule of V
for v being Vector of V ex C being Coset of W st v in C
definition
let AG be non
empty addLoopStr ;
existence
ex b1 being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG st
for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies b1 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b1 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) )
uniqueness
for b1, b2 being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG st ( for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies b1 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b1 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) & ( for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies b2 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b2 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) holds
b1 = b2
end;
Lm19:
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i, j being Element of INT.Ring st i <> 0 & j <> 0 holds
(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))
Lm20:
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i, j being Element of INT.Ring st ( i = 0 or j = 0 ) holds
(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))