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


begin

definition
attr c1 is strict ;
struct Z_ModuleStruct -> addLoopStr ;
aggr Z_ModuleStruct(# carrier, ZeroF, addF, Mult #) -> Z_ModuleStruct ;
sel Mult c1 -> Function of [:INT, the carrier of c1:], the carrier of c1;
end;

registration
cluster non empty for Z_ModuleStruct ;
existence
not for b1 being Z_ModuleStruct holds b1 is empty
proof end;
end;

definition
let V be Z_ModuleStruct ;
mode VECTOR of V is Element of V;
end;

definition
let V be non empty Z_ModuleStruct ;
let v be VECTOR of V;
let a be integer number ;
func a * v -> Element of V equals :: ZMODUL01:def 1
the Mult of V . (a,v);
coherence
the Mult of V . (a,v) is Element of V
proof end;
end;

:: deftheorem defines * ZMODUL01:def 1 :
for V being non empty Z_ModuleStruct
for v being VECTOR of V
for a being integer number holds a * v = the Mult of V . (a,v);

registration
let ZS be non empty set ;
let O be Element of ZS;
let F be BinOp of ZS;
let G be Function of [:INT,ZS:],ZS;
cluster Z_ModuleStruct(# ZS,O,F,G #) -> non empty ;
coherence
not Z_ModuleStruct(# ZS,O,F,G #) is empty
;
end;

definition
let IT be non empty Z_ModuleStruct ;
attr IT is vector-distributive means :Def2: :: ZMODUL01:def 2
for a being integer number
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);
attr IT is scalar-distributive means :Def3: :: ZMODUL01:def 3
for a, b being integer number
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);
attr IT is scalar-associative means :Def4: :: ZMODUL01:def 4
for a, b being integer number
for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attr IT is scalar-unital means :Def5: :: ZMODUL01:def 5
for v being VECTOR of IT holds 1 * v = v;
end;

:: deftheorem Def2 defines vector-distributive ZMODUL01:def 2 :
for IT being non empty Z_ModuleStruct holds
( IT is vector-distributive iff for a being integer number
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

:: deftheorem Def3 defines scalar-distributive ZMODUL01:def 3 :
for IT being non empty Z_ModuleStruct holds
( IT is scalar-distributive iff for a, b being integer number
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

:: deftheorem Def4 defines scalar-associative ZMODUL01:def 4 :
for IT being non empty Z_ModuleStruct holds
( IT is scalar-associative iff for a, b being integer number
for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

:: deftheorem Def5 defines scalar-unital ZMODUL01:def 5 :
for IT being non empty Z_ModuleStruct holds
( IT is scalar-unital iff for v being VECTOR of IT holds 1 * v = v );

definition
func Trivial-Z_ModuleStruct -> strict Z_ModuleStruct equals :: ZMODUL01:def 6
Z_ModuleStruct(# 1,op0,op2,(pr2 (INT,1)) #);
coherence
Z_ModuleStruct(# 1,op0,op2,(pr2 (INT,1)) #) is strict Z_ModuleStruct
;
end;

:: deftheorem defines Trivial-Z_ModuleStruct ZMODUL01:def 6 :
Trivial-Z_ModuleStruct = Z_ModuleStruct(# 1,op0,op2,(pr2 (INT,1)) #);

registration
cluster Trivial-Z_ModuleStruct -> non empty trivial strict ;
coherence
( Trivial-Z_ModuleStruct is trivial & not Trivial-Z_ModuleStruct is empty )
by CARD_1:49;
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for Z_ModuleStruct ;
existence
ex b1 being non empty Z_ModuleStruct st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is scalar-distributive & b1 is vector-distributive & b1 is scalar-associative & b1 is scalar-unital )
proof end;
end;

definition
mode Z_Module is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Z_ModuleStruct ;
end;

definition
let IT be non empty Z_ModuleStruct ;
attr IT is Mult-cancelable means :Def7: :: ZMODUL01:def 7
for a being integer number
for v being VECTOR of IT holds
( not a * v = 0. IT or a = 0 or v = 0. IT );
end;

:: deftheorem Def7 defines Mult-cancelable ZMODUL01:def 7 :
for IT being non empty Z_ModuleStruct holds
( IT is Mult-cancelable iff for a being integer number
for v being VECTOR of IT holds
( not a * v = 0. IT or a = 0 or v = 0. IT ) );

theorem Th1: :: ZMODUL01:1
for a being integer number
for V being Z_Module
for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
proof end;

theorem Th2: :: ZMODUL01:2
for V being Z_Module
for v being VECTOR of V holds - v = (- 1) * v
proof end;

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 a being integer number
for V being Z_Module
for v being VECTOR of V holds a * (- v) = (- a) * v
proof end;

theorem Th6: :: ZMODUL01:6
for a being integer number
for V being Z_Module
for v being VECTOR of V holds a * (- v) = - (a * v)
proof end;

theorem :: ZMODUL01:7
for a being integer number
for V being Z_Module
for v being VECTOR of V holds (- a) * (- v) = a * v
proof end;

theorem Th8: :: ZMODUL01:8
for a being integer number
for V being Z_Module
for v, w being VECTOR of V holds a * (v - w) = (a * v) - (a * w)
proof end;

theorem Th9: :: ZMODUL01:9
for a, b being integer number
for V being Z_Module
for v being VECTOR of V holds (a - b) * v = (a * v) - (b * v)
proof end;

theorem :: ZMODUL01:10
for a being integer number
for V being Z_Module
for v, w being VECTOR of V st V is Mult-cancelable & a <> 0 & a * v = a * w holds
v = w
proof end;

theorem :: ZMODUL01:11
for a, b being integer number
for V being Z_Module
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 V being Z_Module holds Sum (<*> the carrier of V) = 0. V
proof end;

Lm2: for V being Z_Module
for F being FinSequence of V st len F = 0 holds
Sum F = 0. V

proof end;

theorem Th12: :: ZMODUL01:12
for a being integer number
for V being Z_Module
for F, G being FinSequence of V st len F = len G & ( for k being Element of 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 Integer holds a * (Sum (<*> the carrier of V)) = 0. V by Lm1, Th1;

theorem :: ZMODUL01:14
for V being Z_Module
for a being Integer
for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
proof end;

theorem :: ZMODUL01:15
for V being Z_Module
for a being Integer
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 a being integer number
for V being Z_Module
for v being VECTOR of V holds (- a) * v = - (a * v)
proof end;

theorem :: ZMODUL01:17
for a being integer number
for V being Z_Module
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proof end;

begin

definition
let V be Z_Module;
let V1 be Subset of V;
attr V1 is linearly-closed means :Def8: :: ZMODUL01:def 8
( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being integer number
for v being VECTOR of V st v in V1 holds
a * v in V1 ) );
end;

:: deftheorem Def8 defines linearly-closed ZMODUL01:def 8 :
for V being Z_Module
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being integer number
for v being VECTOR of V st v in V1 holds
a * v in V1 ) ) );

theorem Th18: :: ZMODUL01:18
for V being Z_Module
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1
proof end;

theorem Th19: :: ZMODUL01:19
for V being Z_Module
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
proof end;

theorem Th20: :: ZMODUL01:20
for V being Z_Module
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
proof end;

theorem :: ZMODUL01:21
for V being Z_Module
for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed
proof end;

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

registration
let V be Z_Module;
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
proof end;
end;

registration
let V be Z_Module;
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 V be Z_Module;
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
proof end;
end;

definition
let V be Z_Module;
mode Submodule of V -> Z_Module means :Def9: :: ZMODUL01:def 9
( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:INT, the carrier of it:] );
existence
ex b1 being Z_Module st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:INT, the carrier of b1:] )
proof end;
end;

:: deftheorem Def9 defines Submodule ZMODUL01:def 9 :
for V, b2 being Z_Module holds
( b2 is Submodule of V iff ( the carrier of b2 c= the carrier of V & 0. b2 = 0. V & the addF of b2 = the addF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:INT, the carrier of b2:] ) );

theorem Th23: :: ZMODUL01:23
for V being Z_Module
for x being set
for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds
x in W2
proof end;

theorem Th24: :: ZMODUL01:24
for V being Z_Module
for x being set
for W being Submodule of V st x in W holds
x in V
proof end;

theorem Th25: :: ZMODUL01:25
for V being Z_Module
for W being Submodule of V
for w being VECTOR of W holds w is VECTOR of V
proof end;

theorem :: ZMODUL01:26
for V being Z_Module
for W being Submodule of V holds 0. W = 0. V by Def9;

theorem :: ZMODUL01:27
for V being Z_Module
for W1, W2 being Submodule of V holds 0. W1 = 0. W2
proof end;

theorem Th28: :: ZMODUL01:28
for V being Z_Module
for v, u 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
proof end;

theorem Th29: :: ZMODUL01:29
for V being Z_Module
for v being VECTOR of V
for a being integer number
for W being Submodule of V
for w being VECTOR of W st w = v holds
a * w = a * v
proof end;

theorem Th30: :: ZMODUL01:30
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V
for w being VECTOR of W st w = v holds
- v = - w
proof end;

theorem Th31: :: ZMODUL01:31
for V being Z_Module
for v, u 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
proof end;

Lm3: for V being Z_Module
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed

proof end;

theorem Th32: :: ZMODUL01:32
for V being Z_Module holds V is Submodule of V
proof end;

theorem Th33: :: ZMODUL01:33
for V being Z_Module
for W being Submodule of V holds 0. V in W
proof end;

theorem :: ZMODUL01:34
for V being Z_Module
for W1, W2 being Submodule of V holds 0. W1 in W2
proof end;

theorem :: ZMODUL01:35
for V being Z_Module
for W being Submodule of V holds 0. W in V by Th24, RLVECT_1:1;

theorem Th36: :: ZMODUL01:36
for V being Z_Module
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
proof end;

theorem Th37: :: ZMODUL01:37
for V being Z_Module
for v being VECTOR of V
for a being integer number
for W being Submodule of V st v in W holds
a * v in W
proof end;

theorem Th38: :: ZMODUL01:38
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V st v in W holds
- v in W
proof end;

theorem Th39: :: ZMODUL01:39
for V being Z_Module
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
proof end;

theorem Th40: :: ZMODUL01:40
for V being Z_Module
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 [:INT,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
proof end;

theorem Th41: :: ZMODUL01:41
for V, X being strict Z_Module st V is Submodule of X & X is Submodule of V holds
V = X
proof end;

theorem Th42: :: ZMODUL01:42
for V, X, Y being Z_Module st V is Submodule of X & X is Submodule of Y holds
V is Submodule of Y
proof end;

theorem Th43: :: ZMODUL01:43
for V being Z_Module
for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 is Submodule of W2
proof end;

theorem :: ZMODUL01:44
for V being Z_Module
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
proof end;

registration
let V be Z_Module;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() strict vector-distributive scalar-distributive scalar-associative scalar-unital for Submodule of V;
existence
ex b1 being Submodule of V st b1 is strict
proof end;
end;

theorem Th45: :: ZMODUL01:45
for V being Z_Module
for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proof end;

theorem Th46: :: ZMODUL01:46
for V being Z_Module
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
proof end;

theorem :: ZMODUL01:47
for V being strict Z_Module
for W being strict Submodule of V st the carrier of W = the carrier of V holds
W = V
proof end;

theorem :: ZMODUL01:48
for V being strict Z_Module
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 V being Z_Module
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm3;

theorem Th50: :: ZMODUL01:50
for V being Z_Module
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
proof end;

definition
let V be Z_Module;
func (0). V -> strict Submodule of V means :Def10: :: ZMODUL01:def 10
the carrier of it = {(0. V)};
correctness
existence
ex b1 being strict Submodule of V st the carrier of b1 = {(0. V)}
;
uniqueness
for b1, b2 being strict Submodule of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds
b1 = b2
;
by Th45, Th50;
end;

:: deftheorem Def10 defines (0). ZMODUL01:def 10 :
for V being Z_Module
for b2 being strict Submodule of V holds
( b2 = (0). V iff the carrier of b2 = {(0. V)} );

definition
let V be Z_Module;
func (Omega). V -> strict Submodule of V equals :: ZMODUL01:def 11
Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
coherence
Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Submodule of V
proof end;
end;

:: deftheorem defines (Omega). ZMODUL01:def 11 :
for V being Z_Module holds (Omega). V = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

theorem Th51: :: ZMODUL01:51
for V being Z_Module
for W being Submodule of V holds (0). W = (0). V
proof end;

theorem Th52: :: ZMODUL01:52
for V being Z_Module
for W1, W2 being Submodule of V holds (0). W1 = (0). W2
proof end;

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

theorem Th54: :: ZMODUL01:54
for V being Z_Module
for W being Submodule of V holds (0). V is Submodule of W
proof end;

theorem :: ZMODUL01:55
for V being Z_Module
for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2
proof end;

theorem :: ZMODUL01:56
for V being strict Z_Module holds V is Submodule of (Omega). V ;

definition
let V be Z_Module;
let v be VECTOR of V;
let W be Submodule of V;
func v + W -> Subset of V equals :: ZMODUL01:def 12
{ (v + u) where u is VECTOR of V : u in W } ;
coherence
{ (v + u) where u is VECTOR of V : u in W } is Subset of V
proof end;
end;

:: deftheorem defines + ZMODUL01:def 12 :
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;

Lm4: for V being Z_Module
for W being Submodule of V holds (0. V) + W = the carrier of W

proof end;

definition
let V be Z_Module;
let W be Submodule of V;
mode Coset of W -> Subset of V means :Def13: :: ZMODUL01:def 13
ex v being VECTOR of V st it = v + W;
existence
ex b1 being Subset of V ex v being VECTOR of V st b1 = v + W
proof end;
end;

:: deftheorem Def13 defines Coset ZMODUL01:def 13 :
for V being Z_Module
for W being Submodule of V
for b3 being Subset of V holds
( b3 is Coset of W iff ex v being VECTOR of V st b3 = v + W );

theorem Th57: :: ZMODUL01:57
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V holds
( 0. V in v + W iff v in W )
proof end;

theorem Th58: :: ZMODUL01:58
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V holds v in v + W
proof end;

theorem :: ZMODUL01:59
for V being Z_Module
for W being Submodule of V holds (0. V) + W = the carrier of W by Lm4;

theorem Th60: :: ZMODUL01:60
for V being Z_Module
for v being VECTOR of V holds v + ((0). V) = {v}
proof end;

Lm5: for V being Z_Module
for v being VECTOR of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W )

proof end;

theorem Th61: :: ZMODUL01:61
for V being Z_Module
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
proof end;

theorem Th62: :: ZMODUL01:62
for V being Z_Module
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 )
proof end;

theorem :: ZMODUL01:63
for V being Z_Module
for v being VECTOR of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W ) by Lm5;

theorem :: ZMODUL01:64
for V being Z_Module
for v being VECTOR of V
for a being integer number
for W being Submodule of V st v in W holds
(a * v) + W = the carrier of W
proof end;

theorem Th65: :: ZMODUL01:65
for V being Z_Module
for u, v being VECTOR of V
for W being Submodule of V holds
( u in W iff v + W = (v + u) + W )
proof end;

theorem :: ZMODUL01:66
for V being Z_Module
for u, v being VECTOR of V
for W being Submodule of V holds
( u in W iff v + W = (v - u) + W )
proof end;

theorem Th67: :: ZMODUL01:67
for V being Z_Module
for v, u being VECTOR of V
for W being Submodule of V holds
( v in u + W iff u + W = v + W )
proof end;

theorem Th68: :: ZMODUL01:68
for V being Z_Module
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
proof end;

theorem :: ZMODUL01:69
for V being Z_Module
for v being VECTOR of V
for a being integer number
for W being Submodule of V st v in W holds
a * v in v + W
proof end;

theorem Th70: :: ZMODUL01:70
for V being Z_Module
for u, v being VECTOR of V
for W being Submodule of V holds
( u + v in v + W iff u in W )
proof end;

theorem :: ZMODUL01:71
for V being Z_Module
for v, u being VECTOR of V
for W being Submodule of V holds
( v - u in v + W iff u in W )
proof end;

theorem Th72: :: ZMODUL01:72
for V being Z_Module
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 Th73: :: ZMODUL01:73
for V being Z_Module
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 Th74: :: ZMODUL01:74
for V being Z_Module
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 )
proof end;

theorem Th75: :: ZMODUL01:75
for V being Z_Module
for v, u 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 )
proof end;

theorem Th76: :: ZMODUL01:76
for V being Z_Module
for v, u 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 )
proof end;

theorem Th77: :: ZMODUL01:77
for V being Z_Module
for v being VECTOR of V
for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds
W1 = W2
proof end;

theorem Th78: :: ZMODUL01:78
for V being Z_Module
for v, u being VECTOR of V
for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds
W1 = W2
proof end;

theorem :: ZMODUL01:79
for V being Z_Module
for W being Submodule of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
proof end;

theorem :: ZMODUL01:80
for V being Z_Module
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
proof end;

theorem :: ZMODUL01:81
for V being Z_Module
for v being VECTOR of V holds {v} is Coset of (0). V
proof end;

theorem Th82: :: ZMODUL01:82
for V being Z_Module
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
proof end;

theorem Th83: :: ZMODUL01:83
for V being Z_Module
for W being Submodule of V holds the carrier of W is Coset of W
proof end;

theorem :: ZMODUL01:84
for V being Z_Module holds the carrier of V is Coset of (Omega). V
proof end;

theorem :: ZMODUL01:85
for V being Z_Module
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proof end;

theorem :: ZMODUL01:86
for V being Z_Module
for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proof end;

theorem Th87: :: ZMODUL01:87
for V being Z_Module
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 )
proof end;

theorem :: ZMODUL01:88
for V being Z_Module
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 )
proof end;

theorem Th89: :: ZMODUL01:89
for V being Z_Module
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 )
proof end;

theorem :: ZMODUL01:90
for V being Z_Module
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 )
proof end;

theorem :: ZMODUL01:91
for V being Z_Module
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
proof end;

begin

definition
let V be Z_Module;
let W1, W2 be Submodule of V;
func W1 + W2 -> strict Submodule of V means :Def14: :: ZMODUL01:def 14
the carrier of it = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
existence
ex b1 being strict Submodule of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) }
proof end;
uniqueness
for b1, b2 being strict Submodule of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } & the carrier of b2 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } holds
b1 = b2
by Th45;
commutativity
for b1 being strict Submodule of V
for W1, W2 being Submodule of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } holds
the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) }
proof end;
end;

:: deftheorem Def14 defines + ZMODUL01:def 14 :
for V being Z_Module
for W1, W2 being Submodule of V
for b4 being strict Submodule of V holds
( b4 = W1 + W2 iff the carrier of b4 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } );

definition
let V be Z_Module;
let W1, W2 be Submodule of V;
func W1 /\ W2 -> strict Submodule of V means :Def15: :: ZMODUL01:def 15
the carrier of it = the carrier of W1 /\ the carrier of W2;
existence
ex b1 being strict Submodule of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2
proof end;
uniqueness
for b1, b2 being strict Submodule of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 & the carrier of b2 = the carrier of W1 /\ the carrier of W2 holds
b1 = b2
by Th45;
commutativity
for b1 being strict Submodule of V
for W1, W2 being Submodule of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 holds
the carrier of b1 = the carrier of W2 /\ the carrier of W1
;
end;

:: deftheorem Def15 defines /\ ZMODUL01:def 15 :
for V being Z_Module
for W1, W2 being Submodule of V
for b4 being strict Submodule of V holds
( b4 = W1 /\ W2 iff the carrier of b4 = the carrier of W1 /\ the carrier of W2 );

theorem Th92: :: ZMODUL01:92
for x being set
for V being Z_Module
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 ) )
proof end;

theorem :: ZMODUL01:93
for V being Z_Module
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
proof end;

theorem Th94: :: ZMODUL01:94
for x being set
for V being Z_Module
for W1, W2 being Submodule of V holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
proof end;

Lm6: for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)

proof end;

Lm7: for V being Z_Module
for W1 being Submodule of V
for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2

proof end;

theorem :: ZMODUL01:95
for V being Z_Module
for W being strict Submodule of V holds W + W = W by Lm7;

theorem Th96: :: ZMODUL01:96
for V being Z_Module
for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3
proof end;

theorem Th97: :: ZMODUL01:97
for V being Z_Module
for W1, W2 being Submodule of V holds W1 is Submodule of W1 + W2
proof end;

theorem Th98: :: ZMODUL01:98
for V being Z_Module
for W1 being Submodule of V
for W2 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 + W2 = W2 )
proof end;

theorem Th99: :: ZMODUL01:99
for V being Z_Module
for W being strict Submodule of V holds ((0). V) + W = W
proof end;

theorem :: ZMODUL01:100
for V being Z_Module holds ((0). V) + ((Omega). V) = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Th99;

theorem Th101: :: ZMODUL01:101
for V being Z_Module
for W being Submodule of V holds ((Omega). V) + W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
proof end;

theorem :: ZMODUL01:102
for V being strict Z_Module holds ((Omega). V) + ((Omega). V) = V by Th101;

theorem :: ZMODUL01:103
for V being Z_Module
for W being strict Submodule of V holds W /\ W = W
proof end;

theorem Th104: :: ZMODUL01:104
for V being Z_Module
for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proof end;

Lm8: for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1

proof end;

theorem Th105: :: ZMODUL01:105
for V being Z_Module
for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1
proof end;

theorem Th106: :: ZMODUL01:106
for V being Z_Module
for W2 being Submodule of V
for W1 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 /\ W2 = W1 )
proof end;

theorem Th107: :: ZMODUL01:107
for V being Z_Module
for W being Submodule of V holds ((0). V) /\ W = (0). V
proof end;

theorem :: ZMODUL01:108
for V being Z_Module holds ((0). V) /\ ((Omega). V) = (0). V by Th107;

theorem Th109: :: ZMODUL01:109
for V being Z_Module
for W being strict Submodule of V holds ((Omega). V) /\ W = W
proof end;

theorem :: ZMODUL01:110
for V being strict Z_Module holds ((Omega). V) /\ ((Omega). V) = V by Th109;

Lm9: for V being Z_Module
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 V being Z_Module
for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1 + W2 by Lm9, Th43;

Lm10: for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2

proof end;

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

Lm11: for V being Z_Module
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

proof end;

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

Lm12: for V being Z_Module
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 V being Z_Module
for W1, W2, W3 being Submodule of V holds (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by Lm12, Th43;

Lm13: for V being Z_Module
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:115
for V being Z_Module
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 V being Z_Module
for W2, W1, 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 V being Z_Module
for W2, W1, W3 being Submodule of V holds W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3) by Lm14, Th43;

Lm15: for V being Z_Module
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 V being Z_Module
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 Th118: :: ZMODUL01:118
for V being Z_Module
for W1, W3, W2 being Submodule of V st W1 is strict Submodule of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof end;

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

theorem :: ZMODUL01:120
for V being Z_Module
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
proof end;

theorem :: ZMODUL01:121
for V being Z_Module
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 )
proof end;

definition
let V be Z_Module;
func Submodules V -> set means :Def16: :: ZMODUL01:def 16
for x being set holds
( x in it iff x is strict Submodule of V );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict Submodule of V )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Submodule of V ) ) & ( for x being set holds
( x in b2 iff x is strict Submodule of V ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines Submodules ZMODUL01:def 16 :
for V being Z_Module
for b2 being set holds
( b2 = Submodules V iff for x being set holds
( x in b2 iff x is strict Submodule of V ) );

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

theorem :: ZMODUL01:122
for V being strict Z_Module holds V in Submodules V
proof end;

definition
let V be Z_Module;
let W1, W2 be Submodule of V;
pred V is_the_direct_sum_of W1,W2 means :Def17: :: ZMODUL01:def 17
( Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V );
end;

:: deftheorem Def17 defines is_the_direct_sum_of ZMODUL01:def 17 :
for V being Z_Module
for W1, W2 being Submodule of V holds
( V is_the_direct_sum_of W1,W2 iff ( Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );

Lm16: 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 = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)

proof end;

Lm17: for V being Z_Module
for W1, W2 being Submodule of V holds
( W1 + W2 = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 V be Z_Module;
let W be Submodule of V;
attr W is with_Linear_Compl means :Def18: :: ZMODUL01:def 18
ex C being Submodule of V st V is_the_direct_sum_of C,W;
end;

:: deftheorem Def18 defines with_Linear_Compl ZMODUL01:def 18 :
for V being Z_Module
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 V be Z_Module;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() vector-distributive scalar-distributive scalar-associative scalar-unital with_Linear_Compl for Submodule of V;
correctness
existence
ex b1 being Submodule of V st b1 is with_Linear_Compl
;
proof end;
end;

definition
let V be Z_Module;
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 19
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, Def18;
end;

:: deftheorem Def19 defines Linear_Compl ZMODUL01:def 19 :
for V being Z_Module
for W being Submodule of V st W is with_Linear_Compl holds
for b3 being Submodule of V holds
( b3 is Linear_Compl of W iff V is_the_direct_sum_of b3,W );

Lm18: for V being Z_Module
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

proof end;

theorem :: ZMODUL01:123
for V being Z_Module
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 V being Z_Module
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 V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds W + L = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
proof end;

theorem :: ZMODUL01:126
for V being Z_Module
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 V being Z_Module
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 Lm18;

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 Th131: :: ZMODUL01:131
for V being Z_Module
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
proof end;

Lm19: for V being Z_Module
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 Th132: :: 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} )
proof end;

theorem :: ZMODUL01:133
for V being Z_Module
for W1, W2 being Submodule of V holds
( W1 + W2 = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 Th134: :: ZMODUL01:134
for V being Z_Module
for W1, W2 being Submodule of V
for v1, v2, u1, u2 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 )
proof end;

theorem :: ZMODUL01:135
for V being Z_Module
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
let V be Z_Module;
let v be VECTOR of V;
let W1, W2 be Submodule of V;
assume A1: V is_the_direct_sum_of W1,W2 ;
func v |-- (W1,W2) -> Element of [: the carrier of V, the carrier of V:] means :Def20: :: ZMODUL01:def 20
( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );
existence
ex b1 being Element of [: the carrier of V, the carrier of V:] st
( v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 )
proof end;
uniqueness
for b1, b2 being Element of [: the carrier of V, the carrier of V:] st v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 & v = (b2 `1) + (b2 `2) & b2 `1 in W1 & b2 `2 in W2 holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines |-- ZMODUL01:def 20 :
for V being Z_Module
for v being VECTOR of V
for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds
for b5 being Element of [: the carrier of V, the carrier of V:] holds
( b5 = v |-- (W1,W2) iff ( v = (b5 `1) + (b5 `2) & b5 `1 in W1 & b5 `2 in W2 ) );

theorem Th136: :: ZMODUL01:136
for V being Z_Module
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
proof end;

theorem Th137: :: ZMODUL01:137
for V being Z_Module
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
proof end;

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
proof end;

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
proof end;

definition
let V be Z_Module;
func SubJoin V -> BinOp of (Submodules V) means :Def21: :: ZMODUL01:def 21
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 + W2;
existence
ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2
proof end;
uniqueness
for b1, b2 being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines SubJoin ZMODUL01:def 21 :
for V being Z_Module
for b2 being BinOp of (Submodules V) holds
( b2 = SubJoin V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 );

definition
let V be Z_Module;
func SubMeet V -> BinOp of (Submodules V) means :Def22: :: ZMODUL01:def 22
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 /\ W2;
existence
ex b1 being BinOp of (Submodules V) st
for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
proof end;
uniqueness
for b1, b2 being BinOp of (Submodules V) st ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines SubMeet ZMODUL01:def 22 :
for V being Z_Module
for b2 being BinOp of (Submodules V) holds
( b2 = SubMeet V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 );

theorem Th143: :: ZMODUL01:143
for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
proof end;

registration
let V be Z_Module;
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
proof end;

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

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
proof end;

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 = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm16;

theorem :: ZMODUL01:150
for V being Z_Module
for W being Submodule of V
for v being VECTOR of V ex C being Coset of W st v in C by Lm19;

begin

definition
let AG be non empty addLoopStr ;
func Int-mult-left AG -> Function of [:INT, the carrier of AG:], the carrier of AG means :Def23: :: ZMODUL01:def 23
for i being Element of INT
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 [:INT, the carrier of AG:], the carrier of AG st
for i being Element of INT
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 [:INT, the carrier of AG:], the carrier of AG st ( for i being Element of INT
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
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 23 :
for AG being non empty addLoopStr
for b2 being Function of [:INT, the carrier of AG:], the carrier of AG holds
( b2 = Int-mult-left AG iff for i being Element of INT
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
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 Element of INT 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 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 Element of INT 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 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 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 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;

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

Lm21: 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 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 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 Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF of AG,(Int-mult-left AG) #) is Z_Module
proof end;