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


definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
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 R being Ring
for V being LeftMod of R
for a being Element of R holds a * V = { (a * v) where v is Element of V : verum } ;

definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
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 R being Ring
for V being LeftMod of R
for a being Element of R holds Zero_ (a,V) = 0. V;

definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
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 R being Ring
for V being LeftMod of R
for a being Element of R holds Add_ (a,V) = the addF of V | [:(a * V),(a * V):];

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

:: deftheorem defines Mult_ ZMODUL02:def 4 :
for R being commutative Ring
for V being VectSp of R
for a being Element of R holds Mult_ (a,V) = the lmult of V | [: the carrier of R,(a * V):];

definition
let R be commutative Ring;
let V be LeftMod of R;
let a be Element of R;
func a (*) V -> Subspace 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 Subspace of V
proof end;
end;

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

definition
end;

:: deftheorem ZMODUL02:def 6 :
canceled;

:: deftheorem ZMODUL02:def 7 :
canceled;

:: deftheorem ZMODUL02:def 8 :
canceled;

:: deftheorem ZMODUL02:def 9 :
canceled;

:: deftheorem ZMODUL02:def 10 :
canceled;

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 (VectQuot (V,W)) st W = p (*) V holds
p * x = 0. (VectQuot (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 (VectQuot (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
by INT_1:def 2;

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. (VectQuot (V,W))
proof end;

registration
cluster ext-real complex right_complementable V102() integer V115() prime for Element of the carrier of INT.Ring;
existence
ex b1 being Element of INT.Ring st b1 is prime
proof end;
end;

registration
cluster integer prime -> natural integer for object ;
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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (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 (VectQuot (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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) st
for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (VectQuot (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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) st ( for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (VectQuot (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 (VectQuot (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 (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (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 (VectQuot (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 (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);
coherence
ModuleStr(# the carrier of (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (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 (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);

registration
let p be prime Element of INT.Ring;
let V be Z_Module;
cluster Z_MQ_VectSp (V,p) -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
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 R be Ring;
let X be LeftMod of R;
func Mult_INT* X -> Function of [: the carrier of R, 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 R, the carrier of X:], the carrier of X
;
;
end;

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

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

:: deftheorem defines modetrans ZMODUL02:def 15 :
for R being Ring
for X being LeftMod of R holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);

registration
let R be Ring;
let X be LeftMod of R;
cluster modetrans X -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is vector-distributive & modetrans X is scalar-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital )
proof end;
end;

definition
end;

:: deftheorem ZMODUL02:def 16 :
canceled;

:: deftheorem ZMODUL02:def 17 :
canceled;

:: 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;

:: deftheorem ZMODUL02:def 24 :
canceled;

:: deftheorem ZMODUL02:def 25 :
canceled;

:: deftheorem ZMODUL02:def 26 :
canceled;

:: deftheorem ZMODUL02:def 27 :
canceled;

:: deftheorem ZMODUL02:def 28 :
canceled;

::$CD 13
theorem :: ZMODUL02:4
canceled;

::$CD 13
theorem :: ZMODUL02:5
canceled;

::$CD 13
theorem :: ZMODUL02:6
canceled;

::$CD 13
theorem :: ZMODUL02:7
canceled;

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

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

theorem :: ZMODUL02:10
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for A being Subset of V holds ZeroLC V is Linear_Combination of A by VECTSP_6:5;

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

theorem :: ZMODUL02:13
for R being Ring
for V being LeftMod of R
for v being VECTOR of V
for F being FinSequence of V
for f being Function of V,R
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 R being Ring
for V being LeftMod of R
for f being Function of V,R holds f (#) (<*> the carrier of V) = <*> the carrier of V by VECTSP_6:9;

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

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

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

theorem :: ZMODUL02:18
for R being Ring
for V being LeftMod of R
for A being Subset of V st not R is degenerated holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) by VECTSP_6:14;

theorem :: ZMODUL02:19
for R being Ring
for V being LeftMod of R holds Sum (ZeroLC V) = 0. V by VECTSP_6:15;

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

theorem :: ZMODUL02:21
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V by VECTSP_6:19;

theorem Th24: :: ZMODUL02:24
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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;

theorem :: ZMODUL02:26
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 by VECTSP_6:26;

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

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

theorem :: ZMODUL02:30
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V holds (0. R) * L = ZeroLC V by VECTSP_6:30;

theorem Th31: :: ZMODUL02:31
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a being Element of R
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 R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a, b being Element of R holds (a + b) * L = (a * L) + (b * L) by VECTSP_6:32;

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

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

registration
let R be Ring;
let V be LeftMod of R;
let L be Linear_Combination of V;
reduce (1. R) * L to L;
reducibility
(1. R) * L = L
by VECTSP_6:35;
end;

theorem :: ZMODUL02:35
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1 by VECTSP_6:37;

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

theorem :: ZMODUL02:38
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for L being Linear_Combination of V holds L - L = ZeroLC V by VECTSP_6:43;

definition
let R be Ring;
let V be LeftMod of R;
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 R being Ring
for V being LeftMod of R
for b3 being set holds
( b3 = LinComb V iff for x being set holds
( x in b3 iff x is Linear_Combination of V ) );

registration
let R be Ring;
let V be LeftMod of R;
cluster LinComb V -> non empty ;
coherence
not LinComb V is empty
proof end;
end;

definition
let R be Ring;
let V be LeftMod of R;
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 R being Ring
for V being LeftMod of R
for e being Element of LinComb V holds @ e = e;

definition
let R be Ring;
let V be LeftMod of R;
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 R being Ring
for V being LeftMod of R
for L being Linear_Combination of V holds @ L = L;

definition
let R be Ring;
let V be LeftMod of R;
func LCAdd V -> BinOp of (LinComb V) 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 (LinComb V) st
for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2)
proof end;
uniqueness
for b1, b2 being BinOp of (LinComb V) 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 R being Ring
for V being LeftMod of R
for b3 being BinOp of (LinComb V) holds
( b3 = LCAdd V iff for e1, e2 being Element of LinComb V holds b3 . (e1,e2) = (@ e1) + (@ e2) );

definition
let R be Ring;
let V be LeftMod of R;
func LCMult V -> Function of [: the carrier of R,(LinComb V):],(LinComb V) means :Def33: :: ZMODUL02:def 33
for a being Element of R
for e being Element of LinComb V holds it . [a,e] = a * (@ e);
existence
ex b1 being Function of [: the carrier of R,(LinComb V):],(LinComb V) st
for a being Element of R
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 R,(LinComb V):],(LinComb V) st ( for a being Element of R
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Element of R
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 R being Ring
for V being LeftMod of R
for b3 being Function of [: the carrier of R,(LinComb V):],(LinComb V) holds
( b3 = LCMult V iff for a being Element of R
for e being Element of LinComb V holds b3 . [a,e] = a * (@ e) );

definition
let R be Ring;
let V be LeftMod of R;
func LC_Z_Module V -> ModuleStr over R equals :: ZMODUL02:def 34
ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);
coherence
ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #) is ModuleStr over R
;
end;

:: deftheorem defines LC_Z_Module ZMODUL02:def 34 :
for R being Ring
for V being LeftMod of R holds LC_Z_Module V = ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);

registration
let R be Ring;
let V be LeftMod of R;
cluster LC_Z_Module V -> non empty strict ;
coherence
( LC_Z_Module V is strict & not LC_Z_Module V is empty )
;
end;

registration
let R be Ring;
let V be LeftMod of R;
cluster LC_Z_Module V -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( LC_Z_Module V is Abelian & LC_Z_Module V is add-associative & LC_Z_Module V is right_zeroed & LC_Z_Module V is right_complementable & LC_Z_Module V is vector-distributive & LC_Z_Module V is scalar-distributive & LC_Z_Module V is scalar-associative & LC_Z_Module V is scalar-unital )
proof end;
end;

theorem :: ZMODUL02:43
for R being Ring
for V being LeftMod of R holds the carrier of (LC_Z_Module V) = LinComb V ;

theorem :: ZMODUL02:44
for R being Ring
for V being LeftMod of R holds 0. (LC_Z_Module V) = ZeroLC V ;

theorem :: ZMODUL02:45
for R being Ring
for V being LeftMod of R holds the addF of (LC_Z_Module V) = LCAdd V ;

theorem :: ZMODUL02:46
for R being Ring
for V being LeftMod of R holds the lmult of (LC_Z_Module V) = LCMult V ;

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

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

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

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

definition
let R be Ring;
let V be LeftMod of R;
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 R being Ring
for V being LeftMod of R
for A being Subset of V
for b4 being strict Submodule of LC_Z_Module V holds
( b4 = LC_Z_Module A iff the carrier of b4 = { l where l is Linear_Combination of A : verum } );

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

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

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

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

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

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

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

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

registration
let R be Ring;
let V be LeftMod of R;
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 R being Ring
for V being LeftMod of R
for v being Vector of V st not R is degenerated & V is Mult-cancelable holds
( {v} is linearly-independent iff v <> 0. V )
proof end;

registration
let R be non degenerated Ring;
let V be LeftMod of R;
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 R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V st R is commutative & not R is degenerated & {v1,v2} is linearly-independent holds
v1 <> 0. V by VECTSP_7:4;

theorem :: ZMODUL02:61
for R being Ring
for V being LeftMod of R
for v being Vector of V st R is commutative & not R is degenerated holds
{v,(0. V)} is linearly-dependent by Th60;

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

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

theorem :: ZMODUL02:64
for x being set
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A by MOD_3:5;

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

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

theorem :: ZMODUL02:68
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being strict LeftMod of R
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof end;

Lm3: for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) by MOD_3:12;

theorem :: ZMODUL02:73
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 is Submodule of W2 + W3
proof end;