:: $\mathbb Z$-modules
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received September 5, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


definition
mode Z_Module is LeftMod of INT.Ring ;
end;

:: deftheorem ZMODUL01:def 1 :
canceled;

:: deftheorem ZMODUL01:def 2 :
canceled;

:: deftheorem ZMODUL01:def 3 :
canceled;

:: deftheorem ZMODUL01:def 4 :
canceled;

:: deftheorem ZMODUL01:def 5 :
canceled;

:: deftheorem ZMODUL01:def 6 :
canceled;

registration
cluster TrivialLMod INT.Ring -> trivial ;
coherence
( TrivialLMod INT.Ring is trivial & not TrivialLMod INT.Ring is empty & TrivialLMod INT.Ring is strict )
proof end;
end;

registration
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V142() V143() V144() V145() strict vector-distributive scalar-distributive scalar-associative scalar-unital for ModuleStr over INT.Ring ;
existence
ex b1 being Z_Module st b1 is strict
proof end;
end;

definition
let R be Ring;
let V be LeftMod of R;
mode VECTOR of V is Element of V;
end;

definition
let R be Ring;
let IT be LeftMod of R;
attr IT is Mult-cancelable means :: ZMODUL01:def 7
 for a being Element of R
for v being Vector of IT holds
( not a * v = 0. IT or a = 0. R or v = 0. IT );
end;

:: deftheorem defines Mult-cancelable ZMODUL01:def 7 :
for R being Ring
for IT being LeftMod of R holds
( IT is Mult-cancelable iff for a being Element of R
for v being Vector of IT holds
( not a * v = 0. IT or a = 0. R or v = 0. IT ) );

theorem Th1: :: ZMODUL01:1
for V being Z_Module
for a being Element of INT.Ring
for v being Vector of V st ( a = 0. INT.Ring or v = 0. V ) holds
a * v = 0. V
proof end;

theorem Th2: :: ZMODUL01:2
for R being Ring
for V being LeftMod of R
for v being Vector of V holds - v = (- (1. R)) * v by VECTSP_1:14;

theorem Th3: :: ZMODUL01:3
for V being Z_Module
for v being Vector of V st V is Mult-cancelable & v = - v holds
v = 0. V
proof end;

theorem :: ZMODUL01:4
for V being Z_Module
for v being Vector of V st V is Mult-cancelable & v + v = 0. V holds
v = 0. V
proof end;

theorem Th5: :: ZMODUL01:5
for V being Z_Module
for a being Element of INT.Ring
for v being Vector of V holds a * (- v) = (- a) * v
proof end;

theorem Th6: :: ZMODUL01:6
for V being Z_Module
for a being Element of INT.Ring
for v being Vector of V holds a * (- v) = - (a * v)
proof end;

theorem :: ZMODUL01:7
for V being Z_Module
for a being Element of INT.Ring
for v being Vector of V holds (- a) * (- v) = a * v
proof end;

theorem Th8: :: ZMODUL01:8
for V being Z_Module
for a being Element of INT.Ring
for v, w being Vector of V holds a * (v - w) = (a * v) - (a * w)
proof end;

theorem Th9: :: ZMODUL01:9
for V being Z_Module
for a, b being Element of INT.Ring
for v being Vector of V holds (a - b) * v = (a * v) - (b * v)
proof end;

theorem :: ZMODUL01:10
for V being Z_Module
for a being Element of INT.Ring
for v, w being Vector of V st V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w holds
v = w
proof end;

theorem :: ZMODUL01:11
for V being Z_Module
for a, b being Element of INT.Ring
for v being Vector of V st V is Mult-cancelable & v <> 0. V & a * v = b * v holds
a = b
proof end;

Lm1: for R being Ring
for V being LeftMod of R holds Sum (<*> the carrier of V) = 0. V
proof end;

Lm2: for R being Ring
for V being LeftMod of R
for F being FinSequence of V st len F = 0 holds
Sum F = 0. V
proof end;

theorem Th12: :: ZMODUL01:12
for R being Ring
for a being Element of R
for V being LeftMod of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
proof end;

theorem :: ZMODUL01:13
for V being Z_Module
for a being Element of INT.Ring holds a * (Sum (<*> the carrier of V)) = 0. V by Lm1, Th1;

theorem :: ZMODUL01:14
for R being Ring
for V being LeftMod of R
for a being Element of R
for v, u being Vector of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
proof end;

theorem :: ZMODUL01:15
for R being Ring
for V being LeftMod of R
for a being Element of R
for v, u, w being Vector of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
proof end;

theorem :: ZMODUL01:16
for V being LeftMod of INT.Ring
for a being Element of INT.Ring
for v being Vector of V holds (- a) * v = - (a * v)
proof end;

theorem :: ZMODUL01:17
for R being Ring
for a being Element of R
for V being LeftMod of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proof end;

theorem :: ZMODUL01:18
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1 by VECTSP_4:1;

theorem :: ZMODUL01:19
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 is linearly-closed holds
for v being Vector of V st v in V1 holds
- v in V1 by VECTSP_4:2;

theorem :: ZMODUL01:20
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 is linearly-closed holds
for v, u being Vector of V st v in V1 & u in V1 holds
v - u in V1 by VECTSP_4:3;

theorem :: ZMODUL01:21
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed ;

theorem :: ZMODUL01:22
for R being Ring
for V being LeftMod of R
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is Vector of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed
proof end;

registration
let R be Ring;
let V be LeftMod of R;
cluster {(0. V)} -> linearly-closed for Subset of V;
coherence
for b1 being Subset of V st b1 = {(0. V)} holds
b1 is linearly-closed by VECTSP_4:4;
end;

registration
let R be Ring;
let V be LeftMod of R;
cluster linearly-closed for Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 is linearly-closed
proof end;
end;

registration
let R be Ring;
let V be LeftMod of R;
let V1, V2 be linearly-closed Subset of V;
cluster V1 /\ V2 -> linearly-closed for Subset of V;
coherence
for b1 being Subset of V st b1 = V1 /\ V2 holds
b1 is linearly-closed by VECTSP_4:7;
end;

definition
end;

:: deftheorem ZMODUL01:def 8 :
canceled;

:: deftheorem ZMODUL01:def 9 :
canceled;

definition
let R be Ring;
let V be LeftMod of R;
mode Submodule of V is Subspace of V;
end;

theorem :: ZMODUL01:23
for R being Ring
for V being LeftMod of R
for x being set
for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds
x in W2 by VECTSP_4:8;

theorem Th24: :: ZMODUL01:24
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for x being object st x in W holds
x in V by VECTSP_4:9;

theorem Th25: :: ZMODUL01:25
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for w being Vector of W holds w is Vector of V by VECTSP_4:10;

theorem :: ZMODUL01:26
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds 0. W = 0. V by VECTSP_4:def 2;

theorem :: ZMODUL01:27
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds 0. W1 = 0. W2 by VECTSP_4:12;

theorem :: ZMODUL01:28
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V
for w1, w2 being Vector of W st w1 = v & w2 = u holds
w1 + w2 = v + u by VECTSP_4:13;

theorem :: ZMODUL01:29
for R being Ring
for V being LeftMod of R
for v being Vector of V
for a being Element of R
for W being Submodule of V
for w being Vector of W st w = v holds
a * w = a * v by VECTSP_4:14;

theorem :: ZMODUL01:30
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
- v = - w by VECTSP_4:15;

theorem :: ZMODUL01:31
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V
for w1, w2 being Vector of W st w1 = v & w2 = u holds
w1 - w2 = v - u by VECTSP_4:16;

theorem Th32: :: ZMODUL01:32
for R being Ring
for V being LeftMod of R holds V is Submodule of V by VECTSP_4:24;

theorem Th33: :: ZMODUL01:33
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds 0. V in W by VECTSP_4:17;

theorem :: ZMODUL01:34
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds 0. W1 in W2 by VECTSP_4:18;

theorem :: ZMODUL01:35
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds 0. W in V by VECTSP_4:19;

theorem Th36: :: ZMODUL01:36
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V st u in W & v in W holds
u + v in W by VECTSP_4:20;

theorem :: ZMODUL01:37
for R being Ring
for V being LeftMod of R
for v being Vector of V
for a being Element of R
for W being Submodule of V st v in W holds
a * v in W by VECTSP_4:21;

theorem :: ZMODUL01:38
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W being Submodule of V st v in W holds
- v in W by VECTSP_4:22;

theorem Th39: :: ZMODUL01:39
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V st u in W & v in W holds
u - v in W by VECTSP_4:23;

theorem Th40: :: ZMODUL01:40
for R being Ring
for V being LeftMod of R
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [: the carrier of R,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the lmult of V | [: the carrier of R,V1:] holds
ModuleStr(# D,A,d1,M #) is Submodule of V
proof end;

theorem :: ZMODUL01:41
for R being Ring
for V, X being strict LeftMod of R st V is Submodule of X & X is Submodule of V holds
V = X by VECTSP_4:25;

theorem Th42: :: ZMODUL01:42
for R being Ring
for V, X, Y being LeftMod of R st V is Submodule of X & X is Submodule of Y holds
V is Submodule of Y by VECTSP_4:26;

theorem Th43: :: ZMODUL01:43
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 is Submodule of W2 by VECTSP_4:27;

theorem :: ZMODUL01:44
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds
v in W2 ) holds
W1 is Submodule of W2 by VECTSP_4:28;

registration
let R be Ring;
let V be LeftMod of R;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V142() V143() V144() V145() strict vector-distributive scalar-distributive scalar-associative scalar-unital for Subspace of V;
existence
ex b1 being Submodule of V st b1 is strict
proof end;
end;

theorem Th45: :: ZMODUL01:45
for R being Ring
for V being LeftMod of R
for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds
W1 = W2 by VECTSP_4:29;

theorem Th46: :: ZMODUL01:46
for R being Ring
for V being LeftMod of R
for W1, W2 being strict Submodule of V st ( for v being Vector of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2 by VECTSP_4:30;

theorem :: ZMODUL01:47
for R being Ring
for V being strict LeftMod of R
for W being strict Submodule of V st the carrier of W = the carrier of V holds
W = V by VECTSP_4:31;

theorem :: ZMODUL01:48
for R being Ring
for V being strict LeftMod of R
for W being strict Submodule of V st ( for v being Vector of V holds
( v in W iff v in V ) ) holds
W = V
proof end;

theorem :: ZMODUL01:49
for R being Ring
for V being LeftMod of R
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed by VECTSP_4:33;

theorem :: ZMODUL01:50
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W by VECTSP_4:34;

theorem :: ZMODUL01:51
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0). W = (0). V by VECTSP_4:36;

theorem :: ZMODUL01:52
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds (0). W1 = (0). W2 by VECTSP_4:37;

theorem :: ZMODUL01:53
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0). W is Submodule of V by Th42;

theorem Th54: :: ZMODUL01:54
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0). V is Submodule of W by VECTSP_4:39;

theorem :: ZMODUL01:55
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2 by VECTSP_4:40;

theorem :: ZMODUL01:56
for R being Ring
for V being LeftMod of R holds V is Submodule of (Omega). V by VECTSP_4:41;

definition
end;

:: deftheorem ZMODUL01:def 10 :
canceled;

:: deftheorem ZMODUL01:def 11 :
canceled;

:: deftheorem ZMODUL01:def 12 :
canceled;

:: deftheorem ZMODUL01:def 13 :
canceled;

theorem :: ZMODUL01:57
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W being Submodule of V holds
( 0. V in v + W iff v in W ) by VECTSP_4:43;

theorem Th58: :: ZMODUL01:58
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W being Submodule of V holds v in v + W by VECTSP_4:44;

theorem :: ZMODUL01:59
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0. V) + W = the carrier of W by VECTSP_4:45;

theorem :: ZMODUL01:60
for R being Ring
for V being LeftMod of R
for v being Vector of V holds v + ((0). V) = {v} by VECTSP_4:46;

theorem :: ZMODUL01:61
for R being Ring
for V being LeftMod of R
for v being Vector of V holds v + ((Omega). V) = the carrier of V by VECTSP_4:47;

theorem :: ZMODUL01:62
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W being Submodule of V holds
( 0. V in v + W iff v + W = the carrier of W ) by VECTSP_4:48;

theorem :: ZMODUL01:63
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W ) by VECTSP_4:49;

theorem :: ZMODUL01:64
for R being Ring
for V being LeftMod of R
for v being Vector of V
for a being Element of R
for W being Submodule of V st v in W holds
(a * v) + W = the carrier of W by VECTSP_4:50;

theorem :: ZMODUL01:65
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in W iff v + W = (v + u) + W ) by VECTSP_4:53;

theorem :: ZMODUL01:66
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in W iff v + W = (v - u) + W ) by VECTSP_4:54;

theorem :: ZMODUL01:67
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( v in u + W iff u + W = v + W ) by VECTSP_4:55;

theorem :: ZMODUL01:68
for R being Ring
for V being LeftMod of R
for u, v1, v2 being Vector of V
for W being Submodule of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W by VECTSP_4:56;

theorem :: ZMODUL01:69
for R being Ring
for V being LeftMod of R
for v being Vector of V
for a being Element of R
for W being Submodule of V st v in W holds
a * v in v + W by VECTSP_4:58;

theorem :: ZMODUL01:70
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u + v in v + W iff u in W ) by VECTSP_4:60;

theorem :: ZMODUL01:71
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( v - u in v + W iff u in W ) by VECTSP_4:61;

theorem :: ZMODUL01:72
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in v + W iff ex v1 being Vector of V st
( v1 in W & u = v + v1 ) )
proof end;

theorem :: ZMODUL01:73
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V holds
( u in v + W iff ex v1 being Vector of V st
( v1 in W & u = v - v1 ) ) by VECTSP_4:62;

theorem :: ZMODUL01:74
for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V
for W being Submodule of V holds
( ex v being Vector of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) by VECTSP_4:63;

theorem :: ZMODUL01:75
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V st v + W = u + W holds
ex v1 being Vector of V st
( v1 in W & v + v1 = u ) by VECTSP_4:64;

theorem :: ZMODUL01:76
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V st v + W = u + W holds
ex v1 being Vector of V st
( v1 in W & v - v1 = u ) by VECTSP_4:65;

theorem :: ZMODUL01:77
for R being Ring
for V being LeftMod of R
for v being Vector of V
for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds
W1 = W2 by VECTSP_4:66;

theorem :: ZMODUL01:78
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds
W1 = W2 by VECTSP_4:67;

theorem :: ZMODUL01:79
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W ) by VECTSP_4:69;

theorem :: ZMODUL01:80
for R being Ring
for V being LeftMod of R
for W1, W2 being strict Submodule of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2 by VECTSP_4:70;

theorem :: ZMODUL01:81
for R being Ring
for V being LeftMod of R
for v being Vector of V holds {v} is Coset of (0). V by VECTSP_4:71;

theorem :: ZMODUL01:82
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being Vector of V st V1 = {v} by VECTSP_4:72;

theorem :: ZMODUL01:83
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds the carrier of W is Coset of W by VECTSP_4:73;

theorem :: ZMODUL01:84
for R being Ring
for V being LeftMod of R holds the carrier of V is Coset of (Omega). V by VECTSP_4:74;

theorem :: ZMODUL01:85
for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V by VECTSP_4:75;

theorem :: ZMODUL01:86
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W ) by VECTSP_4:76;

theorem :: ZMODUL01:87
for R being Ring
for V being LeftMod of R
for u being Vector of V
for W being Submodule of V
for C being Coset of W holds
( u in C iff C = u + W ) by VECTSP_4:77;

theorem :: ZMODUL01:88
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V
for C being Coset of W st u in C & v in C holds
ex v1 being Vector of V st
( v1 in W & u + v1 = v ) by VECTSP_4:78;

theorem :: ZMODUL01:89
for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V
for C being Coset of W st u in C & v in C holds
ex v1 being Vector of V st
( v1 in W & u - v1 = v ) by VECTSP_4:79;

theorem :: ZMODUL01:90
for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V
for W being Submodule of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W ) by VECTSP_4:80;

theorem :: ZMODUL01:91
for R being Ring
for V being LeftMod of R
for u being Vector of V
for W being Submodule of V
for B, C being Coset of W st u in B & u in C holds
B = C by VECTSP_4:81;

definition
let GF be Ring;
let M be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over GF;
let W1, W2 be Subspace of M;
:: original: +
redefine func W1 + W2 -> Subspace of M;
commutativity
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1 by VECTSP_5:5;
end;

theorem Th92: :: ZMODUL01:92
for R being Ring
for x being set
for V being LeftMod of R
for W1, W2 being Submodule of V holds
( x in W1 + W2 iff ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) by VECTSP_5:1;

theorem :: ZMODUL01:93
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2 by VECTSP_5:2;

theorem Th94: :: ZMODUL01:94
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for x being object holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) by VECTSP_5:3;

Lm6: for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
proof end;

theorem :: ZMODUL01:95
for R being Ring
for V being LeftMod of R
for W being strict Submodule of V holds W + W = W by VECTSP_5:4;

theorem :: ZMODUL01:96
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3 by VECTSP_5:6;

theorem :: ZMODUL01:97
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds W1 is Submodule of W1 + W2 by VECTSP_5:7;

theorem Th98: :: ZMODUL01:98
for R being Ring
for V being LeftMod of R
for W1 being Submodule of V
for W2 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 + W2 = W2 ) by VECTSP_5:8;

theorem Th99: :: ZMODUL01:99
for R being Ring
for V being LeftMod of R
for W being strict Submodule of V holds ((0). V) + W = W by VECTSP_5:9;

theorem :: ZMODUL01:100
for R being Ring
for V being LeftMod of R holds ((0). V) + ((Omega). V) = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_5:10;

theorem Th101: :: ZMODUL01:101
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds ((Omega). V) + W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_5:11;

theorem :: ZMODUL01:102
for R being Ring
for V being strict LeftMod of R holds ((Omega). V) + ((Omega). V) = V by Th101;

theorem :: ZMODUL01:103
for R being Ring
for V being LeftMod of R
for W being strict Submodule of V holds W /\ W = W by VECTSP_5:13;

theorem :: ZMODUL01:104
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by VECTSP_5:14;

Lm8: for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1
proof end;

theorem :: ZMODUL01:105
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1 by VECTSP_5:15;

theorem Th106: :: ZMODUL01:106
for R being Ring
for V being LeftMod of R
for W2 being Submodule of V
for W1 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 /\ W2 = W1 ) by VECTSP_5:16;

theorem Th107: :: ZMODUL01:107
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds ((0). V) /\ W = (0). V by VECTSP_5:20;

theorem :: ZMODUL01:108
for R being Ring
for V being LeftMod of R holds ((0). V) /\ ((Omega). V) = (0). V by Th107;

theorem Th109: :: ZMODUL01:109
for R being Ring
for V being LeftMod of R
for W being strict Submodule of V holds ((Omega). V) /\ W = W by VECTSP_5:21;

theorem :: ZMODUL01:110
for R being Ring
for V being strict LeftMod of R holds ((Omega). V) /\ ((Omega). V) = V by Th109;

Lm9: for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
proof end;

theorem :: ZMODUL01:111
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1 + W2 by Lm9, Th43;

Lm10: for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
proof end;

theorem :: ZMODUL01:112
for R being Ring
for V being LeftMod of R
for W1 being Submodule of V
for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2 by Lm10, Th45;

Lm11: for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
proof end;

theorem :: ZMODUL01:113
for R being Ring
for V being LeftMod of R
for W2 being Submodule of V
for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1 by Lm11, Th45;

Lm12: for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof end;

theorem :: ZMODUL01:114
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V holds (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by Lm12, Th43;

Lm13: 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
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
by VECTSP_5:27;

theorem :: ZMODUL01:115
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
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm13, Th45;

Lm14: for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
proof end;

theorem :: ZMODUL01:116
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V holds W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3) by Lm14, Th43;

Lm15: 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
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
proof end;

theorem :: ZMODUL01:117
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
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm15, Th45;

theorem :: ZMODUL01:118
for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Submodule of V st W1 is strict Submodule of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3 by VECTSP_5:30;

theorem :: ZMODUL01:119
for R being Ring
for V being LeftMod of R
for W1, W2 being strict Submodule of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
proof end;

theorem :: ZMODUL01:120
for R being Ring
for V being LeftMod of R
for W1 being Submodule of V
for W2, W3 being strict Submodule of V st W1 is Submodule of W2 holds
W1 + W3 is Submodule of W2 + W3 by VECTSP_5:32;

theorem :: ZMODUL01:121
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds
( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) by VECTSP_5:35;

notation
let GF be Ring;
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over GF;
synonym Submodules V for Subspaces V;
end;

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

theorem :: ZMODUL01:122
for R being Ring
for V being strict LeftMod of R holds V in Submodules V
proof end;

Lm16: for R being Ring
for V being LeftMod of R
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 #)
proof end;

Lm17: for R being Ring
for V being LeftMod of R
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 ) )
proof end;

definition
let R be Ring;
let V be LeftMod of R;
let W be Submodule of V;
attr W is with_Linear_Compl means :: ZMODUL01:def 17
 ex C being Submodule of V st V is_the_direct_sum_of C,W;
end;

:: deftheorem ZMODUL01:def 14 :
canceled;

:: deftheorem ZMODUL01:def 15 :
canceled;

:: deftheorem ZMODUL01:def 16 :
canceled;

:: deftheorem defines with_Linear_Compl ZMODUL01:def 17 :
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds
( W is with_Linear_Compl iff ex C being Submodule of V st V is_the_direct_sum_of C,W );

registration
let R be Ring;
let V be LeftMod of R;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V142() V143() V144() V145() vector-distributive scalar-distributive scalar-associative scalar-unital with_Linear_Compl for Subspace of V;
correctness
existence
ex b1 being Submodule of V st b1 is with_Linear_Compl ;
proof end;
end;

definition
let R be Ring;
let V be LeftMod of R;
let W be Submodule of V;
assume A1: W is with_Linear_Compl ;
mode Linear_Compl of W -> Submodule of V means :Def19: :: ZMODUL01:def 18
V is_the_direct_sum_of it,W;
existence
ex b1 being Submodule of V st V is_the_direct_sum_of b1,W by A1;
end;

:: deftheorem Def19 defines Linear_Compl ZMODUL01:def 18 :
for R being Ring
for V being LeftMod of R
for W being Submodule of V st W is with_Linear_Compl holds
for b4 being Submodule of V holds
( b4 is Linear_Compl of W iff V is_the_direct_sum_of b4,W );

theorem :: ZMODUL01:123
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1
proof end;

theorem Th124: :: ZMODUL01:124
for R being Ring
for V being LeftMod of R
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
proof end;

theorem :: ZMODUL01:125
for R being Ring
for V being LeftMod of R
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
proof end;

theorem :: ZMODUL01:126
for R being Ring
for V being LeftMod of R
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds W /\ L = (0). V
proof end;

theorem :: ZMODUL01:127
for R being Ring
for V being LeftMod of R
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 by VECTSP_5:41;

theorem :: ZMODUL01:128
for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds W is Linear_Compl of L
proof end;

theorem Th129: :: ZMODUL01:129
for V being Z_Module holds
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
proof end;

theorem :: ZMODUL01:130
for V being Z_Module holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
proof end;

theorem :: ZMODUL01:131
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2 by VECTSP_5:45;

Lm18: for R being Ring
for V being LeftMod of R
for W being Submodule of V
for v being Vector of V ex C being Coset of W st v in C
proof end;

theorem :: ZMODUL01:132
for V being Z_Module
for W1, W2 being Submodule of V holds
( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} ) by VECTSP_5:46;

theorem :: ZMODUL01:133
for R being Ring
for V being LeftMod of R
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 ) ) by Lm17;

theorem :: ZMODUL01:134
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for u1, u2, v1, v2 being Vector of V st V is_the_direct_sum_of W1,W2 & v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) by VECTSP_5:48;

theorem :: ZMODUL01:135
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st
for v1, v2, u1, u2 being Vector of V st v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
V is_the_direct_sum_of W1,W2
proof end;

definition
end;

:: deftheorem ZMODUL01:def 19 :
canceled;

theorem Th136: :: ZMODUL01:136
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for v being Vector of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by VECTSP_5:50;

theorem Th137: :: ZMODUL01:137
for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for v being Vector of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by VECTSP_5:51;

theorem :: ZMODUL01:138
for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W
for v being Vector of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
proof end;

theorem :: ZMODUL01:139
for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W
for v being Vector of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
proof end;

theorem :: ZMODUL01:140
for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W
for v being Vector of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
proof end;

theorem :: ZMODUL01:141
for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W
for v being Vector of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 by Th124, Th136;

theorem :: ZMODUL01:142
for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W
for v being Vector of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 by Th124, Th137;

theorem Th143: :: ZMODUL01:143
for R being Ring
for V being LeftMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice by VECTSP_5:57;

registration
let R be Ring;
let V be LeftMod of R;
cluster LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) -> Lattice-like ;
coherence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th143;
end;

theorem Th144: :: ZMODUL01:144
for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded by VECTSP_5:58;

theorem Th145: :: ZMODUL01:145
for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is upper-bounded by VECTSP_5:59;

theorem :: ZMODUL01:146
for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice
proof end;

theorem :: ZMODUL01:147
for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is modular by VECTSP_5:61;

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

theorem :: ZMODUL01:149
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 #) by Lm16;

theorem :: ZMODUL01:150
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for v being Vector of V ex C being Coset of W st v in C by Lm18;

definition
let AG be non empty addLoopStr ;
func Int-mult-left AG -> Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG means :Def23: :: ZMODUL01:def 20
 for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies it . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies it . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) );
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)) ) )
proof end;
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
proof end;
end;

:: deftheorem Def23 defines Int-mult-left ZMODUL01:def 20 :
for AG being non empty addLoopStr
for b2 being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG holds
( b2 = Int-mult-left AG iff 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)) ) ) );

theorem :: ZMODUL01:151
for R being non empty addLoopStr
for a being Element of R
for i being Element of INT.Ring
for i1 being Element of NAT st i = i1 holds
(Int-mult-left R) . (i,a) = i1 * a by Def23;

theorem Th152: :: ZMODUL01:152
for R being non empty addLoopStr
for a being Element of R
for i being Integer st i = 0 holds
(Int-mult-left R) . (i,a) = 0. R
proof end;

theorem Th153: :: ZMODUL01:153
for R being non empty right_complementable add-associative right_zeroed addLoopStr
for i being Element of NAT holds (Nat-mult-left R) . (i,(0. R)) = 0. R
proof end;

theorem Th154: :: ZMODUL01:154
for R being non empty right_complementable add-associative right_zeroed addLoopStr
for i being Element of INT.Ring holds (Int-mult-left R) . (i,(0. R)) = 0. R
proof end;

theorem Th155: :: ZMODUL01:155
for R being non empty right_zeroed addLoopStr
for a being Element of R
for i being Integer st i = 1 holds
(Int-mult-left R) . (i,a) = a
proof end;

theorem Th156: :: ZMODUL01:156
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i, j, k being Element of NAT st i <= j & k = j - i holds
(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))
proof end;

theorem Th157: :: ZMODUL01:157
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i being Element of NAT holds - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))
proof end;

theorem Th158: :: ZMODUL01:158
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 in NAT & not j in NAT holds
(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
proof end;

theorem Th159: :: ZMODUL01:159
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 holds (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
proof end;

theorem Th160: :: ZMODUL01:160
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a, b being Element of R
for i being Element of NAT holds (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b))
proof end;

theorem Th161: :: ZMODUL01:161
for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a, b being Element of R
for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
proof end;

theorem Th162: :: ZMODUL01:162
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 NAT holds (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))
proof 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)))
proof 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.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)))
proof end;

theorem Th163: :: ZMODUL01:163
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 holds (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))
proof end;

theorem :: ZMODUL01:164
for AG being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module
proof end;