:: $\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 b₁ being Z_Module st b₁ 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 b₁ being Subset of V st b₁ = {(0. V)} holds
b₁ 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 b₁ being Subset of V st b₁ 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 b₁ being Subset of V st b₁ = V1 /\ V2 holds
b₁ 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 b₁ being Submodule of V st b₁ 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 b₁ being Submodule of V st b₁ 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 b₁ being Submodule of V st V is_the_direct_sum_of b₁,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 b₄ being Submodule of V holds
( b₄ is Linear_Compl of W iff V is_the_direct_sum_of b₄,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 b₁ 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 b₁ . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b₁ . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b₁ . (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 b₂ . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b₂ . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) holds
b₁ = b₂

proof end;

end;

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