:: $\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
attrc1 is strict ;
struct Z_ModuleStruct  ->  addLoopStr ;
aggrZ_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
proofend;
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 ;
funca * 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
proofend;
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 ;
attrIT 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);
attrIT 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);
attrIT 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);
attrIT 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 )
proofend;
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 ;
attrIT 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
proofend;

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

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

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

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

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

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

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

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

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 &amp; a <> 0 &amp; a * v = a * w holds
v = w
proofend;

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 &amp; v <> 0. V &amp; a * v = b * v holds
a = b
proofend;

Lm1:  for V being Z_Module holds Sum (<*> the carrier of V) = 0. V
proofend;

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

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 &amp; ( for k being Element of NAT
for v being VECTOR of V st k in dom F &amp; v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
proofend;

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

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

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

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 &amp; ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proofend;

begin

definition
let V be Z_Module;
let V1 be Subset of V;
attrV1 is linearly-closed  means :Def8: :: ZMODUL01:def 8
( ( for v, u being VECTOR of V st v in V1 &amp; u in V1 holds
v + u in V1 ) &amp; ( 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 &amp; u in V1 holds
v + u in V1 ) &amp; ( 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 <> {} &amp; V1 is linearly-closed holds
0. V in V1
proofend;

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

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 &amp; u in V1 holds
v - u in V1
proofend;

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

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

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

registration
let V be Z_Module;
let V1, V2 be linearly-closed Subset of V;
clusterV1 /\ V2 ->  linearly-closed for Subset of V;
coherence
 for b1 being Subset of V st b1 = V1 /\ V2 holds
b1 is linearly-closed
proofend;
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 &amp; 0. it = 0. V &amp; the addF of it = the addF of V || the carrier of it &amp; 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 &amp; 0. b1 = 0. V &amp; the addF of b1 = the addF of V || the carrier of b1 &amp; the Mult of b1 = the Mult of V | [:INT, the carrier of b1:] )
proofend;
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 &amp; 0. b2 = 0. V &amp; the addF of b2 = the addF of V || the carrier of b2 &amp; 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 &amp; W1 is Submodule of W2 holds
x in W2
proofend;

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

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

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

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 &amp; w2 = u holds
w1 + w2 = v + u
proofend;

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

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

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 &amp; w2 = u holds
w1 - w2 = v - u
proofend;

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

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

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

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

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 &amp; v in W holds
u + v in W
proofend;

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

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

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 &amp; v in W holds
u - v in W
proofend;

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 &amp; d1 = 0. V &amp; A = the addF of V || V1 &amp; M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
proofend;

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

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

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

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

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

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

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

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

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 <> {} &amp; V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W
proofend;

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)} &amp; 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
proofend;
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
proofend;

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

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

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

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;
funcv + 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
proofend;
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
proofend;

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

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

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

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

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

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

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

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

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

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

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 &amp; u in v2 + W holds
v1 + W = v2 + W
proofend;

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

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

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

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 &amp; u = v + v1 ) )
proofend;

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 &amp; u = v - v1 ) )
proofend;

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 &amp; v2 in v + W ) iff v1 - v2 in W )
proofend;

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 &amp; v + v1 = u )
proofend;

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 &amp; v - v1 = u )
proofend;

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

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

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

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

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

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

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

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

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

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

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

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 &amp; v in C holds
ex v1 being VECTOR of V st
( v1 in W &amp; u + v1 = v )
proofend;

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 &amp; v in C holds
ex v1 being VECTOR of V st
( v1 in W &amp; u - v1 = v )
proofend;

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 &amp; v2 in C ) iff v1 - v2 in W )
proofend;

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 &amp; u in C holds
B = C
proofend;

begin

definition
let V be Z_Module;
let W1, W2 be Submodule of V;
funcW1 + 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 &amp; 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 &amp; u in W2 )  }
proofend;
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 &amp; u in W2 )  }  &amp; the carrier of b2 =  {  (v + u) where v, u is VECTOR of V : ( v in W1 &amp; 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 &amp; u in W2 )  }  holds
the carrier of b1 =  {  (v + u) where v, u is VECTOR of V : ( v in W2 &amp; u in W1 )  }
proofend;
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 &amp; u in W2 )  }  );

definition
let V be Z_Module;
let W1, W2 be Submodule of V;
funcW1 /\ 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
proofend;
uniqueness
 for b1, b2 being strict Submodule of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 &amp; 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 &amp; v2 in W2 &amp; x = v1 + v2 ) )
proofend;

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

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 &amp; x in W2 ) )
proofend;

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

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

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

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

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

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

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 #)
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Submodule of V ) ) &amp; ( for x being set holds
( x in b2 iff x is strict Submodule of V ) ) holds
b1 = b2
proofend;
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
proofend;
end;

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

definition
let V be Z_Module;
let W1, W2 be Submodule of V;
predV 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 &amp; 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 &amp; 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 #)
proofend;

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 &amp; v2 in W2 &amp; v = v1 + v2 ) )
proofend;

definition
let V be Z_Module;
let W be Submodule of V;
attrW 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 ;
proofend;
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
proofend;

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

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 &amp; V is_the_direct_sum_of W,L )
proofend;

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 #)
proofend;

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

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

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

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

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

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

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} )
proofend;

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 &amp; v2 in W2 &amp; 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 &amp; v1 + v2 = u1 + u2 &amp; v1 in W1 &amp; u1 in W1 &amp; v2 in W2 &amp; u2 in W2 holds
( v1 = u1 &amp; v2 = u2 )
proofend;

theorem :: ZMODUL01:135
for V being Z_Module
for W1, W2 being Submodule of V st V = W1 + W2 &amp; ex v being VECTOR of V st
for v1, v2, u1, u2 being VECTOR of V st v1 + v2 = u1 + u2 &amp; v1 in W1 &amp; u1 in W1 &amp; v2 in W2 &amp; u2 in W2 holds
( v1 = u1 &amp; v2 = u2 ) holds
V is_the_direct_sum_of W1,W2
proofend;

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 ;
funcv |-- (W1,W2) ->  Element of [: the carrier of V, the carrier of V:] means :Def20: :: ZMODUL01:def 20
( v = (it `1) + (it `2) &amp; it `1 in W1 &amp; it `2 in W2 );
existence
 ex b1 being Element of [: the carrier of V, the carrier of V:] st
( v = (b1 `1) + (b1 `2) &amp; b1 `1 in W1 &amp; b1 `2 in W2 )
proofend;
uniqueness
 for b1, b2 being Element of [: the carrier of V, the carrier of V:] st v = (b1 `1) + (b1 `2) &amp; b1 `1 in W1 &amp; b1 `2 in W2 &amp; v = (b2 `1) + (b2 `2) &amp; b2 `1 in W1 &amp; b2 `2 in W2 holds
b1 = b2
proofend;
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) &amp; b5 `1 in W1 &amp; 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
proofend;

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

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 &amp; t `1 in W &amp; t `2 in L holds
t = v |-- (W,L)
proofend;

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

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 &amp; (v |-- (W,L)) `2 in L )
proofend;

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

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

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 &amp; 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 &amp; A2 = W2 holds
b1 . (A1,A2) = W1 + W2
proofend;
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 &amp; A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) &amp; ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 &amp; A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
proofend;
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 &amp; 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 &amp; 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 &amp; A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
proofend;
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 &amp; A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) &amp; ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 &amp; A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
proofend;
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 &amp; 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
proofend;

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

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

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

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

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

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) ) &amp; ( 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) ) &amp; ( i < 0 implies b1 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) )
proofend;
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) ) &amp; ( i < 0 implies b1 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) &amp; ( 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) ) &amp; ( i < 0 implies b2 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) holds
b1 = b2
proofend;
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) ) &amp; ( 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
proofend;

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

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

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

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 &amp; k = j - i holds
(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))
proofend;

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

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 &amp; not j in NAT holds
(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
proofend;

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

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

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

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

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 &amp; j <> 0 holds
(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))
proofend;

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

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

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