:: 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 b₁ being Element of INT.Ring st b₁ is prime

proof end;

end;

registration

cluster integer prime -> natural integer for object ;

coherence
for b₁ being integer Number st b₁ is prime holds
b₁ 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 b₁ 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
b₁ . (a,x) = (i mod p) * x

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (a,x) = (i mod p) * x ) holds
b₁ = b₂

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 b₃ being Function of [: the carrier of (GF p), the carrier of (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) holds
( b₃ = 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
b₃ . (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 b₁ being set st
for x being set holds
( x in b₁ iff x is Linear_Combination of V )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is Linear_Combination of V ) ) & ( for x being set holds
( x in b₂ iff x is Linear_Combination of V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def29 defines LinComb ZMODUL02:def 29 :
for R being Ring
for V being LeftMod of R
for b₃ being set holds
( b₃ = LinComb V iff for x being set holds
( x in b₃ 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 b₁ being BinOp of (LinComb V) st
for e1, e2 being Element of LinComb V holds b₁ . (e1,e2) = (@ e1) + (@ e2)

proof end;

uniqueness
for b₁, b₂ being BinOp of (LinComb V) st ( for e1, e2 being Element of LinComb V holds b₁ . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b₂ . (e1,e2) = (@ e1) + (@ e2) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def32 defines LCAdd ZMODUL02:def 32 :
for R being Ring
for V being LeftMod of R
for b₃ being BinOp of (LinComb V) holds
( b₃ = LCAdd V iff for e1, e2 being Element of LinComb V holds b₃ . (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 b₁ 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 b₁ . [a,e] = a * (@ e)

proof end;

uniqueness
for b₁, b₂ 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 b₁ . [a,e] = a * (@ e) ) & ( for a being Element of R
for e being Element of LinComb V holds b₂ . [a,e] = a * (@ e) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def33 defines LCMult ZMODUL02:def 33 :
for R being Ring
for V being LeftMod of R
for b₃ being Function of [: the carrier of R,(LinComb V):],(LinComb V) holds
( b₃ = LCMult V iff for a being Element of R
for e being Element of LinComb V holds b₃ . [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 b₁ being strict Submodule of LC_Z_Module V st the carrier of b₁ = { l where l is Linear_Combination of A : verum }

proof end;

uniqueness
for b₁, b₂ being strict Submodule of LC_Z_Module V st the carrier of b₁ = { l where l is Linear_Combination of A : verum } & the carrier of b₂ = { l where l is Linear_Combination of A : verum } holds
b₁ = b₂ 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 b₄ being strict Submodule of LC_Z_Module V holds
( b₄ = LC_Z_Module A iff the carrier of b₄ = { 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 b₁ being Subset of V st b₁ 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 b₁ being Subset of V st b₁ = {(0. V)} holds
not b₁ 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;