:: Operations on Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let R be Ring;
let V be RightMod of R;
let W1, W2 be Submodule of V;
funcW1 + W2 ->  strict Submodule of V means :Def1: :: RMOD_3:def 1
 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 )  }
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 & 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 RMOD_2:29;
end;

:: deftheorem Def1 defines + RMOD_3:def_1_:_
 for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for b5 being strict Submodule of V holds
( b5 = W1 + W2 iff the carrier of b5 =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  );

definition
let R be Ring;
let V be RightMod of R;
let W1, W2 be Submodule of V;
funcW1 /\ W2 ->  strict Submodule of V means :Def2: :: RMOD_3:def 2
 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 & the carrier of b2 = the carrier of W1 /\ the carrier of W2 holds
b1 = b2 by RMOD_2:29;
end;

:: deftheorem Def2 defines /\ RMOD_3:def_2_:_
 for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for b5 being strict Submodule of V holds
( b5 = W1 /\ W2 iff the carrier of b5 = the carrier of W1 /\ the carrier of W2 );

theorem Th1: :: RMOD_3:1
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
proofend;

theorem :: RMOD_3:2
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
proofend;

theorem Th3: :: RMOD_3:3
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
proofend;

Lm1:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1
proofend;

Lm2:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
proofend;

Lm3:  for R being Ring
for V being RightMod of R
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 :: RMOD_3:4
for R being Ring
for V being RightMod of R
for W being strict Submodule of V holds W + W = W by Lm3;

theorem :: RMOD_3:5
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1 by Lm1;

theorem Th6: :: RMOD_3:6
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3
proofend;

theorem Th7: :: RMOD_3:7
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2 )
proofend;

theorem Th8: :: RMOD_3:8
for R being Ring
for V being RightMod of R
for W1 being Submodule of V
for W2 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 + W2 = W2 )
proofend;

theorem Th9: :: RMOD_3:9
for R being Ring
for V being RightMod of R
for W being strict Submodule of V holds
( ((0). V) + W = W & W + ((0). V) = W )
proofend;

Lm4:  for R being Ring
for V being RightMod of R
for W, W9, W1 being Submodule of V st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
proofend;

Lm5:  for R being Ring
for V being RightMod of R
for W being Submodule of V holds W is Submodule of (Omega). V
proofend;

theorem :: RMOD_3:10
for R being Ring
for V being strict RightMod of R holds
( ((0). V) + ((Omega). V) = V & ((Omega). V) + ((0). V) = V ) by Th9;

theorem Th11: :: RMOD_3:11
for R being Ring
for V being RightMod of R
for W being Submodule of V holds
( ((Omega). V) + W = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) )
proofend;

theorem :: RMOD_3:12
for R being Ring
for V being strict RightMod of R holds ((Omega). V) + ((Omega). V) = V by Th11;

theorem :: RMOD_3:13
for R being Ring
for V being RightMod of R
for W being strict Submodule of V holds W /\ W = W
proofend;

theorem Th14: :: RMOD_3:14
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds W1 /\ W2 = W2 /\ W1
proofend;

theorem Th15: :: RMOD_3:15
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proofend;

Lm6:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1
proofend;

theorem Th16: :: RMOD_3:16
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )
proofend;

theorem Th17: :: RMOD_3:17
for R being Ring
for V being RightMod of R
for W2 being Submodule of V holds
( ( for W1 being strict Submodule of V st W1 is Submodule of W2 holds
W1 /\ W2 = W1 ) & ( for W1 being Submodule of V st W1 /\ W2 = W1 holds
W1 is Submodule of W2 ) )
proofend;

theorem :: RMOD_3:18
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 /\ W3 is Submodule of W2 /\ W3
proofend;

theorem :: RMOD_3:19
for R being Ring
for V being RightMod of R
for W1, W3, W2 being Submodule of V st W1 is Submodule of W3 holds
W1 /\ W2 is Submodule of W3
proofend;

theorem :: RMOD_3:20
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds
W1 is Submodule of W2 /\ W3
proofend;

theorem Th21: :: RMOD_3:21
for R being Ring
for V being RightMod of R
for W being Submodule of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
proofend;

theorem Th22: :: RMOD_3:22
for R being Ring
for V being RightMod of R
for W being strict Submodule of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
proofend;

theorem :: RMOD_3:23
for R being Ring
for V being strict RightMod of R holds ((Omega). V) /\ ((Omega). V) = V by Th22;

Lm7:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
proofend;

theorem :: RMOD_3:24
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds W1 /\ W2 is Submodule of W1 + W2 by Lm7, RMOD_2:27;

Lm8:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
proofend;

theorem :: RMOD_3:25
for R being Ring
for V being RightMod of R
for W1 being Submodule of V
for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2 by Lm8, RMOD_2:29;

Lm9:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
proofend;

theorem :: RMOD_3:26
for R being Ring
for V being RightMod of R
for W2 being Submodule of V
for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1 by Lm9, RMOD_2:29;

Lm10:  for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proofend;

theorem :: RMOD_3:27
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V holds (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by Lm10, RMOD_2:27;

Lm11:  for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
proofend;

theorem :: RMOD_3:28
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm11, RMOD_2:29;

Lm12:  for R being Ring
for V being RightMod of R
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 :: RMOD_3:29
for R being Ring
for V being RightMod of R
for W2, W1, W3 being Submodule of V holds W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3) by Lm12, RMOD_2:27;

Lm13:  for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
proofend;

theorem :: RMOD_3:30
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm13, RMOD_2:29;

theorem Th31: :: RMOD_3:31
for R being Ring
for V being RightMod of R
for W3, W2 being Submodule of V
for W1 being strict Submodule of V st W1 is Submodule of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proofend;

theorem :: RMOD_3:32
for R being Ring
for V being RightMod of R
for W1, W2 being strict Submodule of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
proofend;

theorem :: RMOD_3:33
for R being Ring
for V being RightMod of R
for W1 being Submodule of V
for W2, W3 being strict Submodule of V st W1 is Submodule of W2 holds
W1 + W3 is Submodule of W2 + W3
proofend;

theorem :: RMOD_3:34
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 is Submodule of W2 + W3
proofend;

theorem :: RMOD_3:35
for R being Ring
for V being RightMod of R
for W1, W3, W2 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds
W1 + W2 is Submodule of W3
proofend;

theorem :: RMOD_3:36
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proofend;

definition
let R be Ring;
let V be RightMod of R;
func Submodules V ->  set  means :Def3: :: RMOD_3:def 3
 for x being set holds
( x in it iff ex W being strict Submodule of V st W = x );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Submodule of V st W = x )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Submodule of V st W = x ) ) & ( for x being set holds
( x in b2 iff ex W being strict Submodule of V st W = x ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Submodules RMOD_3:def_3_:_
 for R being Ring
for V being RightMod of R
for b3 being set holds
( b3 = Submodules V iff for x being set holds
( x in b3 iff ex W being strict Submodule of V st W = x ) );

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

theorem :: RMOD_3:37
for R being Ring
for V being strict RightMod of R holds V in Submodules V
proofend;

definition
let R be Ring;
let V be RightMod of R;
let W1, W2 be Submodule of V;
predV is_the_direct_sum_of W1,W2 means :Def4: :: RMOD_3:def 4
( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V );
end;

:: deftheorem Def4 defines is_the_direct_sum_of RMOD_3:def_4_:_
 for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( V is_the_direct_sum_of W1,W2 iff ( RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );

Lm14:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds
( W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult 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 ) )
proofend;

Lm15:  for R being Ring
for V being RightMod of R
for v, v1, v2 being Vector of V holds
( v = v1 + v2 iff v1 = v - v2 )
proofend;

theorem Th38: :: RMOD_3:38
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1
proofend;

theorem :: RMOD_3:39
for R being Ring
for V being strict RightMod of R holds
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
proofend;

theorem Th40: :: RMOD_3:40
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
proofend;

theorem Th41: :: RMOD_3:41
for R being Ring
for V being RightMod of R
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 :: RMOD_3:42
for R being Ring
for V being strict RightMod of R
for W1, W2 being Submodule of V holds
( W1 + W2 = 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 Lm14;

theorem Th43: :: RMOD_3:43
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for v, v1, v2, u1, u2 being Vector of V st V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
proofend;

theorem :: RMOD_3:44
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V st V = W1 + W2 & ex v being Vector of V st
for v1, v2, u1, u2 being Vector of V st v = v1 + v2 & v = 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
proofend;

definition
let R be Ring;
let V be RightMod of R;
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 :Def5: :: RMOD_3:def 5
( 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 )
proofend;
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
proofend;
end;

:: deftheorem Def5 defines |-- RMOD_3:def_5_:_
 for R being Ring
for V being RightMod of R
for v being Vector of V
for W1, W2 being Submodule of V st V is_the_direct_sum_of W1,W2 holds
for b6 being Element of [: the carrier of V, the carrier of V:] holds
( b6 = v |-- (W1,W2) iff ( v = (b6 `1) + (b6 `2) & b6 `1 in W1 & b6 `2 in W2 ) );

theorem :: RMOD_3:45
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for v being Vector of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
proofend;

theorem :: RMOD_3:46
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for v being Vector of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
proofend;

definition
let R be Ring;
let V be RightMod of R;
func SubJoin V ->  BinOp of (Submodules V) means :Def6: :: RMOD_3:def 6
 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
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 & 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
proofend;
end;

:: deftheorem Def6 defines SubJoin RMOD_3:def_6_:_
 for R being Ring
for V being RightMod of R
for b3 being BinOp of (Submodules V) holds
( b3 = SubJoin V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 + W2 );

definition
let R be Ring;
let V be RightMod of R;
func SubMeet V ->  BinOp of (Submodules V) means :Def7: :: RMOD_3:def 7
 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
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 & 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
proofend;
end;

:: deftheorem Def7 defines SubMeet RMOD_3:def_7_:_
 for R being Ring
for V being RightMod of R
for b3 being BinOp of (Submodules V) holds
( b3 = SubMeet V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 /\ W2 );

theorem Th47: :: RMOD_3:47
for R being Ring
for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
proofend;

theorem Th48: :: RMOD_3:48
for R being Ring
for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
proofend;

theorem Th49: :: RMOD_3:49
for R being Ring
for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
proofend;

theorem :: RMOD_3:50
for R being Ring
for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice
proofend;

theorem :: RMOD_3:51
for R being Ring
for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice
proofend;