:: Quotient Module of \$\mathbb Z\$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Copyright (c) 2012-2014 Association of Mizar Users

definition
let V be Z_Module;
let a be Element of INT.Ring;
func a * V -> non empty Subset of V equals :: ZMODUL02:def 1
{ (a * v) where v is Element of V : verum } ;
correctness
coherence
{ (a * v) where v is Element of V : verum } is non empty Subset of V
;
proof end;
end;

:: deftheorem defines * ZMODUL02:def 1 :
for V being Z_Module
for a being Element of INT.Ring holds a * V = { (a * v) where v is Element of V : verum } ;

definition
let V be Z_Module;
let a be Element of INT.Ring;
func Zero_ (a,V) -> Element of a * V equals :: ZMODUL02:def 2
0. V;
correctness
coherence
0. V is Element of a * V
;
proof end;
end;

:: deftheorem defines Zero_ ZMODUL02:def 2 :
for V being Z_Module
for a being Element of INT.Ring holds Zero_ (a,V) = 0. V;

definition
let V be Z_Module;
let a be Element of INT.Ring;
func Add_ (a,V) -> Function of [:(a * V),(a * V):],(a * V) equals :: ZMODUL02:def 3
the addF of V | [:(a * V),(a * V):];
correctness
coherence
the addF of V | [:(a * V),(a * V):] is Function of [:(a * V),(a * V):],(a * V)
;
proof end;
end;

:: deftheorem defines Add_ ZMODUL02:def 3 :
for V being Z_Module
for a being Element of INT.Ring holds Add_ (a,V) = the addF of V | [:(a * V),(a * V):];

definition
let V be Z_Module;
let a be Element of INT.Ring;
func Mult_ (a,V) -> Function of [: the carrier of INT.Ring,(a * V):],(a * V) equals :: ZMODUL02:def 4
the lmult of V | [:INT,(a * V):];
correctness
coherence
the lmult of V | [:INT,(a * V):] is Function of [: the carrier of INT.Ring,(a * V):],(a * V)
;
proof end;
end;

:: deftheorem defines Mult_ ZMODUL02:def 4 :
for V being Z_Module
for a being Element of INT.Ring holds Mult_ (a,V) = the lmult of V | [:INT,(a * V):];

definition
let V be Z_Module;
let a be Element of INT.Ring;
func a (*) V -> Submodule of V equals :: ZMODUL02:def 5
ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);
coherence
ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #) is Submodule of V
proof end;
end;

:: deftheorem defines (*) ZMODUL02:def 5 :
for V being Z_Module
for a being Element of INT.Ring holds a (*) V = ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);

definition
let V be Z_Module;
let W be Submodule of V;
func CosetSet (V,W) -> non empty Subset-Family of V equals :: ZMODUL02:def 6
{ A where A is Coset of W : verum } ;
correctness
coherence
{ A where A is Coset of W : verum } is non empty Subset-Family of V
;
proof end;
end;

:: deftheorem defines CosetSet ZMODUL02:def 6 :
for V being Z_Module
for W being Submodule of V holds CosetSet (V,W) = { A where A is Coset of W : verum } ;

definition
let V be Z_Module;
let W be Submodule of V;
func addCoset (V,W) -> BinOp of (CosetSet (V,W)) means :Def7: :: ZMODUL02:def 7
for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
it . (A,B) = (a + b) + W;
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
proof end;
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
proof end;
end;

:: deftheorem Def7 defines addCoset ZMODUL02:def 7 :
for V being Z_Module
for W being Submodule of V
for b3 being BinOp of (CosetSet (V,W)) holds
( b3 = addCoset (V,W) iff for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b3 . (A,B) = (a + b) + W );

definition
let V be Z_Module;
let W be Submodule of V;
func zeroCoset (V,W) -> Element of CosetSet (V,W) equals :: ZMODUL02:def 8
the carrier of W;
coherence
the carrier of W is Element of CosetSet (V,W)
proof end;
end;

:: deftheorem defines zeroCoset ZMODUL02:def 8 :
for V being Z_Module
for W being Submodule of V holds zeroCoset (V,W) = the carrier of W;

definition
let V be Z_Module;
let W be Submodule of V;
func lmultCoset (V,W) -> Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) means :Def9: :: ZMODUL02:def 9
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
it . (z,A) = (z * a) + W;
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
proof end;
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
proof end;
end;

:: deftheorem Def9 defines lmultCoset ZMODUL02:def 9 :
for V being Z_Module
for W being Submodule of V
for b3 being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) holds
( b3 = lmultCoset (V,W) iff 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
b3 . (z,A) = (z * a) + W );

definition
let V be Z_Module;
let W be Submodule of V;
func Z_ModuleQuot (V,W) -> strict Z_Module means :Def10: :: ZMODUL02:def 10
( the carrier of it = CosetSet (V,W) & the addF of it = addCoset (V,W) & 0. it = zeroCoset (V,W) & the lmult of it = lmultCoset (V,W) );
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) )
proof end;
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;

:: deftheorem Def10 defines Z_ModuleQuot ZMODUL02:def 10 :
for V being Z_Module
for W being Submodule of V
for b3 being strict Z_Module holds
( b3 = Z_ModuleQuot (V,W) iff ( the carrier of b3 = CosetSet (V,W) & the addF of b3 = addCoset (V,W) & 0. b3 = zeroCoset (V,W) & the lmult of b3 = lmultCoset (V,W) ) );

theorem Th1: :: ZMODUL02:1
for p being Element of INT.Ring
for V being Z_Module
for W being Submodule of V
for x being VECTOR of (Z_ModuleQuot (V,W)) st W = p (*) V holds
p * x = 0. (Z_ModuleQuot (V,W))
proof end;

theorem Th2: :: ZMODUL02:2
for p, i being Element of INT.Ring
for V being Z_Module
for W being Submodule of V
for x being VECTOR of (Z_ModuleQuot (V,W)) st p <> 0 & W = p (*) V holds
i * x = (i mod p) * x
proof end;

Lem1: for i being Integer holds i in the carrier of INT.Ring
proof end;

theorem :: ZMODUL02:3
for p, q being Element of INT.Ring
for V being Z_Module
for W being Submodule of V
for v being VECTOR of V st W = p (*) V & p > 1 & q > 1 & p,q are_coprime & q * v = 0. V holds
v + W = 0. (Z_ModuleQuot (V,W))
proof end;

registration
cluster -> integer for Element of the carrier of INT.Ring;
coherence
for b1 being Element of INT.Ring holds b1 is integer
;
end;

registration
existence
ex b1 being Element of INT.Ring st b1 is prime
proof end;
end;

registration
coherence
for b1 being integer Number st b1 is prime holds
b1 is natural
proof end;
end;

definition
let p be prime Element of INT.Ring;
let V be Z_Module;
func Mult_Mod_pV (V,p) -> Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) means :Def11: :: ZMODUL02:def 11
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
it . (a,x) = (i mod p) * x;
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
proof end;
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
proof end;
end;

:: deftheorem Def11 defines Mult_Mod_pV ZMODUL02:def 11 :
for p being prime Element of INT.Ring
for V being Z_Module
for b3 being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) holds
( b3 = Mult_Mod_pV (V,p) iff 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
b3 . (a,x) = (i mod p) * x );

definition
let p be prime Element of INT.Ring;
let V be Z_Module;
func Z_MQ_VectSp (V,p) -> non empty strict ModuleStr over GF p equals :: ZMODUL02:def 12
ModuleStr(# the carrier of (Z_ModuleQuot (V,(p (*) V))), the addF of (Z_ModuleQuot (V,(p (*) V))), the ZeroF of (Z_ModuleQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);
coherence
ModuleStr(# the carrier of (Z_ModuleQuot (V,(p (*) V))), the addF of (Z_ModuleQuot (V,(p (*) V))), the ZeroF of (Z_ModuleQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #) is non empty strict ModuleStr over GF p
;
end;

:: deftheorem defines Z_MQ_VectSp ZMODUL02:def 12 :
for p being prime Element of INT.Ring
for V being Z_Module holds Z_MQ_VectSp (V,p) = ModuleStr(# the carrier of (Z_ModuleQuot (V,(p (*) V))), the addF of (Z_ModuleQuot (V,(p (*) V))), the ZeroF of (Z_ModuleQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);

registration
let p be prime Element of INT.Ring;
let V be Z_Module;
coherence
( Z_MQ_VectSp (V,p) is scalar-distributive & Z_MQ_VectSp (V,p) is vector-distributive & Z_MQ_VectSp (V,p) is scalar-associative & Z_MQ_VectSp (V,p) is scalar-unital & Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )
proof end;
end;

definition
let p be prime Element of INT.Ring;
let V be Z_Module;
let v be VECTOR of V;
func ZMtoMQV (V,p,v) -> Vector of (Z_MQ_VectSp (V,p)) equals :: ZMODUL02:def 13
v + (p (*) V);
correctness
coherence
v + (p (*) V) is Vector of (Z_MQ_VectSp (V,p))
;
proof end;
end;

:: deftheorem defines ZMtoMQV ZMODUL02:def 13 :
for p being prime Element of INT.Ring
for V being Z_Module
for v being VECTOR of V holds ZMtoMQV (V,p,v) = v + (p (*) V);

definition
let X be Z_Module;
func Mult_INT* X -> Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X equals :: ZMODUL02:def 14
the lmult of X;
correctness
coherence
the lmult of X is Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X
;
;
end;

:: deftheorem defines Mult_INT* ZMODUL02:def 14 :
for X being Z_Module holds Mult_INT* X = the lmult of X;

definition
let X be Z_Module;
func modetrans X -> non empty strict ModuleStr over INT.Ring equals :: ZMODUL02:def 15
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);
coherence
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is non empty strict ModuleStr over INT.Ring
;
end;

:: deftheorem defines modetrans ZMODUL02:def 15 :
for X being Z_Module holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);

registration
let X be Z_Module;
coherence
proof end;
end;

definition
let X be LeftMod of INT.Ring ;
func Mult_INT* X -> Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X equals :: ZMODUL02:def 16
the lmult of X;
coherence
the lmult of X is Function of [: the carrier of INT.Ring, the carrier of X:], the carrier of X
;
end;

:: deftheorem defines Mult_INT* ZMODUL02:def 16 :
for X being LeftMod of INT.Ring holds Mult_INT* X = the lmult of X;

definition
let X be LeftMod of INT.Ring ;
func modetrans X -> non empty strict ModuleStr over INT.Ring equals :: ZMODUL02:def 17
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);
correctness
coherence
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is non empty strict ModuleStr over INT.Ring
;
;
end;

:: deftheorem defines modetrans ZMODUL02:def 17 :
for X being LeftMod of INT.Ring holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);

registration
let X be LeftMod of INT.Ring ;
coherence
proof end;
end;

theorem :: ZMODUL02:4
canceled;

theorem :: ZMODUL02:5
canceled;

theorem :: ZMODUL02:6
canceled;

theorem :: ZMODUL02:7
canceled;

definition
end;

:: deftheorem ZMODUL02:def 18 :
canceled;

:: deftheorem ZMODUL02:def 19 :
canceled;

:: deftheorem ZMODUL02:def 20 :
canceled;

:: deftheorem ZMODUL02:def 21 :
canceled;

:: deftheorem ZMODUL02:def 22 :
canceled;

:: deftheorem ZMODUL02:def 23 :
canceled;

theorem :: ZMODUL02:8
for V being Z_Module
for L being Linear_Combination of V
for v being Element of V holds
( L . v = 0. INT.Ring iff not v in Carrier L )
proof end;

theorem :: ZMODUL02:9
for V being Z_Module
for v being Element of V holds () . v = 0. INT.Ring
proof end;

theorem :: ZMODUL02:10
for V being Z_Module
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B by VECTSP_6:4;

theorem Th11: :: ZMODUL02:11
for V being Z_Module
for A being Subset of V holds ZeroLC V is Linear_Combination of A by VECTSP_6:5;

theorem :: ZMODUL02:12
for V being Z_Module
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V by VECTSP_6:6;

theorem :: ZMODUL02:13
for V being Z_Module
for v being VECTOR of V
for F being FinSequence of V
for f being Function of V,INT.Ring
for i being Element of NAT st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v by VECTSP_6:8;

theorem :: ZMODUL02:14
for V being Z_Module
for f being Function of V,INT.Ring holds f (#) (<*> the carrier of V) = <*> the carrier of V by VECTSP_6:9;

theorem :: ZMODUL02:15
for V being Z_Module
for v being VECTOR of V
for f being Function of V,INT.Ring holds f (#) <*v*> = <*((f . v) * v)*> by VECTSP_6:10;

theorem :: ZMODUL02:16
for V being Z_Module
for v1, v2 being Vector of V
for f being Function of V,INT.Ring holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> by VECTSP_6:11;

theorem :: ZMODUL02:17
for V being Z_Module
for v1, v2, v3 being Vector of V
for f being Function of V,INT.Ring holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by VECTSP_6:12;

theorem :: ZMODUL02:18
for V being Z_Module
for A being Subset of V holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proof end;

theorem :: ZMODUL02:19
for V being Z_Module holds Sum () = 0. V by VECTSP_6:15;

theorem :: ZMODUL02:20
for V being Z_Module
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V by VECTSP_6:16;

theorem :: ZMODUL02:21
for V being Z_Module
for v being VECTOR of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v by VECTSP_6:17;

theorem Th22: :: ZMODUL02:22
for V being Z_Module
for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) by VECTSP_6:18;

theorem :: ZMODUL02:23
for V being Z_Module
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V by VECTSP_6:19;

theorem Th24: :: ZMODUL02:24
for V being Z_Module
for v being VECTOR of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v by VECTSP_6:20;

theorem :: ZMODUL02:25
for V being Z_Module
for L being Linear_Combination of V
for v1, v2 being Vector of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2) by VECTSP_6:21;

definition
end;

:: deftheorem ZMODUL02:def 24 :
canceled;

:: deftheorem ZMODUL02:def 25 :
canceled;

:: deftheorem ZMODUL02:def 26 :
canceled;

theorem :: ZMODUL02:26
for V being Z_Module
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by VECTSP_6:23;

theorem Th27: :: ZMODUL02:27
for V being Z_Module
for L1, L2 being Linear_Combination of V
for A being Subset of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A by VECTSP_6:24;

theorem Th28: :: ZMODUL02:28
for V being Z_Module
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 by VECTSP_6:26;

registration
let V be Z_Module;
let L be Linear_Combination of V;
reduce L + () to L;
reducibility
L + () = L
by VECTSP_6:27;
end;

theorem :: ZMODUL02:29
for V being Z_Module
for L being Linear_Combination of V
for a being Element of INT.Ring st a <> 0. INT.Ring holds
Carrier (a * L) = Carrier L
proof end;

theorem :: ZMODUL02:30
for V being Z_Module
for L being Linear_Combination of V holds () * L = ZeroLC V by VECTSP_6:30;

theorem Th31: :: ZMODUL02:31
for V being Z_Module
for L being Linear_Combination of V
for a being Element of INT.Ring
for A being Subset of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A by VECTSP_6:31;

theorem Th32: :: ZMODUL02:32
for V being Z_Module
for L being Linear_Combination of V
for a, b being Element of INT.Ring holds (a + b) * L = (a * L) + (b * L) by VECTSP_6:32;

theorem Th33: :: ZMODUL02:33
for V being Z_Module
for L1, L2 being Linear_Combination of V
for a being Element of INT.Ring holds a * (L1 + L2) = (a * L1) + (a * L2) by VECTSP_6:33;

theorem Th34: :: ZMODUL02:34
for V being Z_Module
for L being Linear_Combination of V
for a, b being Element of INT.Ring holds a * (b * L) = (a * b) * L by VECTSP_6:34;

registration
let V be Z_Module;
let L be Linear_Combination of V;
reduce () * L to L;
reducibility
() * L = L
by VECTSP_6:35;
end;

definition
end;

:: deftheorem ZMODUL02:def 27 :
canceled;

:: deftheorem ZMODUL02:def 28 :
canceled;

theorem :: ZMODUL02:35
for V being Z_Module
for v being VECTOR of V
for L being Linear_Combination of V holds (- L) . v = - (L . v) by VECTSP_6:36;

theorem :: ZMODUL02:36
for V being Z_Module
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1 by VECTSP_6:37;

theorem :: ZMODUL02:37
for V being Z_Module
for L being Linear_Combination of V holds Carrier (- L) = Carrier L by VECTSP_6:38;

theorem :: ZMODUL02:38
for V being Z_Module
for L being Linear_Combination of V
for A being Subset of V st L is Linear_Combination of A holds
- L is Linear_Combination of A by VECTSP_6:39;

theorem :: ZMODUL02:39
for V being Z_Module
for v being VECTOR of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) by VECTSP_6:40;

theorem :: ZMODUL02:40
for V being Z_Module
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by VECTSP_6:41;

theorem :: ZMODUL02:41
for V being Z_Module
for L1, L2 being Linear_Combination of V
for A being Subset of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A by VECTSP_6:42;

theorem Th42: :: ZMODUL02:42
for V being Z_Module
for L being Linear_Combination of V holds L - L = ZeroLC V by VECTSP_6:43;

definition
let V be Z_Module;
func LinComb V -> set means :Def29: :: ZMODUL02:def 29
for x being set holds
( x in it iff x is Linear_Combination of V );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Linear_Combination of V )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Linear_Combination of V ) ) & ( for x being set holds
( x in b2 iff x is Linear_Combination of V ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines LinComb ZMODUL02:def 29 :
for V being Z_Module
for b2 being set holds
( b2 = LinComb V iff for x being set holds
( x in b2 iff x is Linear_Combination of V ) );

registration
let V be Z_Module;
cluster LinComb V -> non empty ;
coherence
not LinComb V is empty
proof end;
end;

definition
let V be Z_Module;
let e be Element of LinComb V;
func @ e -> Linear_Combination of V equals :: ZMODUL02:def 30
e;
coherence
e is Linear_Combination of V
by Def29;
end;

:: deftheorem defines @ ZMODUL02:def 30 :
for V being Z_Module
for e being Element of LinComb V holds @ e = e;

definition
let V be Z_Module;
let L be Linear_Combination of V;
func @ L -> Element of LinComb V equals :: ZMODUL02:def 31
L;
coherence
L is Element of LinComb V
by Def29;
end;

:: deftheorem defines @ ZMODUL02:def 31 :
for V being Z_Module
for L being Linear_Combination of V holds @ L = L;

definition
let V be Z_Module;
func LCAdd V -> BinOp of () means :Def32: :: ZMODUL02:def 32
for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);
existence
ex b1 being BinOp of () st
for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2)
proof end;
uniqueness
for b1, b2 being BinOp of () st ( for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def32 defines LCAdd ZMODUL02:def 32 :
for V being Z_Module
for b2 being BinOp of () holds
( b2 = LCAdd V iff for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) );

definition
let V be Z_Module;
func LCMult V -> Function of [: the carrier of INT.Ring,():],() means :Def33: :: ZMODUL02:def 33
for a being Element of INT.Ring
for e being Element of LinComb V holds it . [a,e] = a * (@ e);
existence
ex b1 being Function of [: the carrier of INT.Ring,():],() st
for a being Element of INT.Ring
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e)
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of INT.Ring,():],() st ( for a being Element of INT.Ring
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Element of INT.Ring
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def33 defines LCMult ZMODUL02:def 33 :
for V being Z_Module
for b2 being Function of [: the carrier of INT.Ring,():],() holds
( b2 = LCMult V iff for a being Element of INT.Ring
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) );

definition
let V be Z_Module;
func LC_Z_Module V -> ModuleStr over INT.Ring equals :: ZMODUL02:def 34
ModuleStr(# (),(),(@ ()),() #);
coherence
ModuleStr(# (),(),(@ ()),() #) is ModuleStr over INT.Ring
;
end;

:: deftheorem defines LC_Z_Module ZMODUL02:def 34 :
for V being Z_Module holds LC_Z_Module V = ModuleStr(# (),(),(@ ()),() #);

registration
let V be Z_Module;
coherence
( LC_Z_Module V is strict & not LC_Z_Module V is empty )
;
end;

registration
let V be Z_Module;
coherence
proof end;
end;

theorem :: ZMODUL02:43
for V being Z_Module holds the carrier of () = LinComb V ;

theorem :: ZMODUL02:44
for V being Z_Module holds 0. () = ZeroLC V ;

theorem :: ZMODUL02:45
for V being Z_Module holds the addF of () = LCAdd V ;

theorem :: ZMODUL02:46
for V being Z_Module holds the lmult of () = LCMult V ;

theorem Th47: :: ZMODUL02:47
for V being Z_Module
for L1, L2 being Linear_Combination of V holds (vector ((),L1)) + (vector ((),L2)) = L1 + L2
proof end;

theorem Th48: :: ZMODUL02:48
for V being Z_Module
for L being Linear_Combination of V
for a being Element of INT.Ring holds a * (vector ((),L)) = a * L
proof end;

theorem Th49: :: ZMODUL02:49
for V being Z_Module
for L being Linear_Combination of V holds - (vector ((),L)) = - L
proof end;

theorem :: ZMODUL02:50
for V being Z_Module
for L1, L2 being Linear_Combination of V holds (vector ((),L1)) - (vector ((),L2)) = L1 - L2
proof end;

definition
let V be Z_Module;
let A be Subset of V;
func LC_Z_Module A -> strict Submodule of LC_Z_Module V means :: ZMODUL02:def 35
the carrier of it = { l where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Submodule of LC_Z_Module V st the carrier of b1 = { l where l is Linear_Combination of A : verum }
proof end;
uniqueness
for b1, b2 being strict Submodule of LC_Z_Module V st the carrier of b1 = { l where l is Linear_Combination of A : verum } & the carrier of b2 = { l where l is Linear_Combination of A : verum } holds
b1 = b2
by ZMODUL01:45;
end;

:: deftheorem defines LC_Z_Module ZMODUL02:def 35 :
for V being Z_Module
for A being Subset of V
for b3 being strict Submodule of LC_Z_Module V holds
( b3 = LC_Z_Module A iff the carrier of b3 = { l where l is Linear_Combination of A : verum } );

theorem :: ZMODUL02:51
for V being Z_Module
for F, G being FinSequence of V
for f being Function of V,INT.Ring holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by VECTSP_6:13;

theorem :: ZMODUL02:52
for V being Z_Module
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) by VECTSP_6:44;

theorem :: ZMODUL02:53
for V being Z_Module
for a being Element of INT.Ring
for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L) by MOD_3:3;

theorem :: ZMODUL02:54
for V being Z_Module
for L being Linear_Combination of V holds Sum (- L) = - (Sum L) by VECTSP_6:46;

theorem :: ZMODUL02:55
for V being Z_Module
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) by VECTSP_6:47;

theorem :: ZMODUL02:56
for V being Z_Module
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent by VECTSP_7:1;

theorem Th57: :: ZMODUL02:57
for V being Z_Module
for A being Subset of V st A is linearly-independent holds
not 0. V in A by VECTSP_7:2;

theorem :: ZMODUL02:58
for V being Z_Module holds {} the carrier of V is linearly-independent ;

registration
let V be Z_Module;
cluster linearly-independent for Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 is linearly-independent
proof end;
end;

theorem :: ZMODUL02:59
for V being Z_Module
for v being Vector of V st V is Mult-cancelable holds
( {v} is linearly-independent iff v <> 0. V )
proof end;

registration
let V be Z_Module;
cluster {(0. V)} -> linearly-dependent for Subset of V;
coherence
for b1 being Subset of V st b1 = {(0. V)} holds
not b1 is linearly-independent
proof end;
end;

theorem Th60: :: ZMODUL02:60
for V being Z_Module
for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds
v1 <> 0. V by VECTSP_7:4;

theorem :: ZMODUL02:61
for V being Z_Module
for v being Vector of V holds {v,(0. V)} is linearly-dependent by Th60;

theorem Th62: :: ZMODUL02:62
for V being Z_Module
for v1, v2 being Vector of V st V is Mult-cancelable holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
b * v1 <> a * v2 ) ) )
proof end;

theorem :: ZMODUL02:63
for V being Z_Module
for v1, v2 being Vector of V st V is Mult-cancelable holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of INT.Ring st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
proof end;

theorem :: ZMODUL02:64
for x being set
for V being Z_Module
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) by MOD_3:4;

theorem Th65: :: ZMODUL02:65
for x being set
for V being Z_Module
for A being Subset of V st x in A holds
x in Lin A by MOD_3:5;

theorem :: ZMODUL02:66
for V being Z_Module
for x being object holds
( x in (0). V iff x = 0. V )
proof end;

theorem :: ZMODUL02:67
for V being Z_Module holds Lin ({} the carrier of V) = (0). V by MOD_3:6;

theorem :: ZMODUL02:68
for V being Z_Module
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} ) by MOD_3:7;

theorem :: ZMODUL02:69
for V being strict Z_Module
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof 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

proof end;

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

proof end;

theorem :: ZMODUL02:70
for V being Z_Module
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B by MOD_3:10;

theorem :: ZMODUL02:71
for V being strict Z_Module
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V by MOD_3:11;

theorem :: ZMODUL02:72
for V being Z_Module
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) by MOD_3:12;

theorem :: ZMODUL02:73
for V being Z_Module
for A, B being Subset of V holds Lin (A /\ B) is Submodule of (Lin A) /\ (Lin B) by MOD_3:13;

theorem :: ZMODUL02:74
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 holds
W1 /\ W2 is Submodule of W3
proof end;

theorem :: ZMODUL02:75
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 by Lm3;

theorem :: ZMODUL02:76
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 by Lm4;

theorem :: ZMODUL02:77
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 is Submodule of W2 + W3
proof end;