begin
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
begin
Lm3:
for V being Z_Module
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed
Lm4:
for V being Z_Module
for W being Submodule of V holds (0. V) + W = the carrier of W
Lm5:
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W )
begin
Lm6:
for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
Lm7:
for V being Z_Module
for W1 being Submodule of V
for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = 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))
Lm14:
for V being Z_Module
for W2, W1, 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 = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
Lm17:
for V being Z_Module
for W1, W2 being Submodule of V holds
( W1 + W2 = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1
Lm19:
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 V be
Z_Module;
existence
ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2
uniqueness
for b1, b2 being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
end;
definition
let V be
Z_Module;
existence
ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
uniqueness
for b1, b2 being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
end;
begin
definition
let AG be non
empty addLoopStr ;
existence
ex b1 being Function of [:INT, the carrier of AG:], the carrier of AG st
for i being Element of INT
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 [:INT, the carrier of AG:], the carrier of AG st ( for i being Element of INT
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
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;
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 st i <> 0 & j <> 0 holds
(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))
Lm21:
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 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)))