:: RMOD_3 semantic presentation

definition
let c1 be Ring;
let c2 be RightMod of c1;
let c3, c4 be Submodule of c2;
func c3 + c4 -> strict Submodule of a2 means :Def1: :: RMOD_3:def 1
the carrier of a5 = { (b1 + b2) where B is Vector of a2, B is Vector of a2 : ( b1 in a3 & b2 in a4 ) } ;
existence
ex b1 being strict Submodule of c2 st the carrier of b1 = { (b2 + b3) where B is Vector of c2, B is Vector of c2 : ( b2 in c3 & b3 in c4 ) }
proof end;
uniqueness
for b1, b2 being strict Submodule of c2 st the carrier of b1 = { (b3 + b4) where B is Vector of c2, B is Vector of c2 : ( b3 in c3 & b4 in c4 ) } & the carrier of b2 = { (b3 + b4) where B is Vector of c2, B is Vector of c2 : ( b3 in c3 & b4 in c4 ) } holds
b1 = b2 by RMOD_2:37;
end;

:: deftheorem Def1 defines + RMOD_3:def 1 :
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being strict Submodule of b2 holds
( b5 = b3 + b4 iff the carrier of b5 = { (b6 + b7) where B is Vector of b2, B is Vector of b2 : ( b6 in b3 & b7 in b4 ) } );

definition
let c1 be Ring;
let c2 be RightMod of c1;
let c3, c4 be Submodule of c2;
func c3 /\ c4 -> strict Submodule of a2 means :Def2: :: RMOD_3:def 2
the carrier of a5 = the carrier of a3 /\ the carrier of a4;
existence
ex b1 being strict Submodule of c2 st the carrier of b1 = the carrier of c3 /\ the carrier of c4
proof end;
uniqueness
for b1, b2 being strict Submodule of c2 st the carrier of b1 = the carrier of c3 /\ the carrier of c4 & the carrier of b2 = the carrier of c3 /\ the carrier of c4 holds
b1 = b2 by RMOD_2:37;
end;

:: deftheorem Def2 defines /\ RMOD_3:def 2 :
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being strict Submodule of b2 holds
( b5 = b3 /\ b4 iff the carrier of b5 = the carrier of b3 /\ the carrier of b4 );

theorem Th1: :: RMOD_3:1
canceled;

theorem Th2: :: RMOD_3:2
canceled;

theorem Th3: :: RMOD_3:3
canceled;

theorem Th4: :: RMOD_3:4
canceled;

theorem Th5: :: RMOD_3:5
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being set holds
( b5 in b3 + b4 iff ex b6, b7 being Vector of b2 st
( b6 in b3 & b7 in b4 & b5 = b6 + b7 ) )
proof end;

theorem Th6: :: RMOD_3:6
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being Vector of b2 st ( b5 in b3 or b5 in b4 ) holds
b5 in b3 + b4
proof end;

theorem Th7: :: RMOD_3:7
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being set holds
( b5 in b3 /\ b4 iff ( b5 in b3 & b5 in b4 ) )
proof end;

Lemma5: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds b3 + b4 = b4 + b3
proof end;

Lemma6: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds the carrier of b3 c= the carrier of (b3 + b4)
proof end;

Lemma7: for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2
for b4 being strict Submodule of b2 st the carrier of b3 c= the carrier of b4 holds
b3 + b4 = b4
proof end;

theorem Th8: :: RMOD_3:8
for b1 being Ring
for b2 being RightMod of b1
for b3 being strict Submodule of b2 holds b3 + b3 = b3 by Lemma7;

theorem Th9: :: RMOD_3:9
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds b3 + b4 = b4 + b3 by Lemma5;

theorem Th10: :: RMOD_3:10
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 holds b3 + (b4 + b5) = (b3 + b4) + b5
proof end;

theorem Th11: :: RMOD_3:11
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds
( b3 is Submodule of b3 + b4 & b4 is Submodule of b3 + b4 )
proof end;

theorem Th12: :: RMOD_3:12
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2
for b4 being strict Submodule of b2 holds
( b3 is Submodule of b4 iff b3 + b4 = b4 )
proof end;

theorem Th13: :: RMOD_3:13
for b1 being Ring
for b2 being RightMod of b1
for b3 being strict Submodule of b2 holds
( ((0). b2) + b3 = b3 & b3 + ((0). b2) = b3 )
proof end;

Lemma12: for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st the carrier of b3 = the carrier of b4 holds
( b5 + b3 = b5 + b4 & b3 + b5 = b4 + b5 )
proof end;

Lemma13: for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2 holds b3 is Submodule of (Omega). b2
proof end;

theorem Th14: :: RMOD_3:14
for b1 being Ring
for b2 being strict RightMod of b1 holds
( ((0). b2) + ((Omega). b2) = b2 & ((Omega). b2) + ((0). b2) = b2 ) by Th13;

theorem Th15: :: RMOD_3:15
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2 holds
( ((Omega). b2) + b3 = RightModStr(# the carrier of b2,the add of b2,the Zero of b2,the rmult of b2 #) & b3 + ((Omega). b2) = RightModStr(# the carrier of b2,the add of b2,the Zero of b2,the rmult of b2 #) )
proof end;

theorem Th16: :: RMOD_3:16
for b1 being Ring
for b2 being strict RightMod of b1 holds ((Omega). b2) + ((Omega). b2) = b2 by Th15;

theorem Th17: :: RMOD_3:17
for b1 being Ring
for b2 being RightMod of b1
for b3 being strict Submodule of b2 holds b3 /\ b3 = b3
proof end;

theorem Th18: :: RMOD_3:18
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds b3 /\ b4 = b4 /\ b3
proof end;

theorem Th19: :: RMOD_3:19
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 holds b3 /\ (b4 /\ b5) = (b3 /\ b4) /\ b5
proof end;

Lemma18: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds the carrier of (b3 /\ b4) c= the carrier of b3
proof end;

theorem Th20: :: RMOD_3:20
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds
( b3 /\ b4 is Submodule of b3 & b3 /\ b4 is Submodule of b4 )
proof end;

theorem Th21: :: RMOD_3:21
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2 holds
( ( for b4 being strict Submodule of b2 st b4 is Submodule of b3 holds
b4 /\ b3 = b4 ) & ( for b4 being Submodule of b2 st b4 /\ b3 = b4 holds
b4 is Submodule of b3 ) )
proof end;

theorem Th22: :: RMOD_3:22
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
b3 /\ b5 is Submodule of b4 /\ b5
proof end;

theorem Th23: :: RMOD_3:23
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
b3 /\ b5 is Submodule of b4
proof end;

theorem Th24: :: RMOD_3:24
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 & b3 is Submodule of b5 holds
b3 is Submodule of b4 /\ b5
proof end;

theorem Th25: :: RMOD_3:25
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2 holds
( ((0). b2) /\ b3 = (0). b2 & b3 /\ ((0). b2) = (0). b2 )
proof end;

theorem Th26: :: RMOD_3:26
canceled;

theorem Th27: :: RMOD_3:27
for b1 being Ring
for b2 being RightMod of b1
for b3 being strict Submodule of b2 holds
( ((Omega). b2) /\ b3 = b3 & b3 /\ ((Omega). b2) = b3 )
proof end;

theorem Th28: :: RMOD_3:28
for b1 being Ring
for b2 being strict RightMod of b1 holds ((Omega). b2) /\ ((Omega). b2) = b2 by Th27;

Lemma23: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds the carrier of (b3 /\ b4) c= the carrier of (b3 + b4)
proof end;

theorem Th29: :: RMOD_3:29
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds b3 /\ b4 is Submodule of b3 + b4
proof end;

Lemma24: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds the carrier of ((b3 /\ b4) + b4) = the carrier of b4
proof end;

theorem Th30: :: RMOD_3:30
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2
for b4 being strict Submodule of b2 holds (b3 /\ b4) + b4 = b4
proof end;

Lemma26: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds the carrier of (b3 /\ (b3 + b4)) = the carrier of b3
proof end;

theorem Th31: :: RMOD_3:31
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2
for b4 being strict Submodule of b2 holds b4 /\ (b4 + b3) = b4
proof end;

Lemma28: for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 holds the carrier of ((b3 /\ b4) + (b4 /\ b5)) c= the carrier of (b4 /\ (b3 + b5))
proof end;

theorem Th32: :: RMOD_3:32
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 holds (b3 /\ b4) + (b4 /\ b5) is Submodule of b4 /\ (b3 + b5)
proof end;

Lemma29: for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
the carrier of (b4 /\ (b3 + b5)) = the carrier of ((b3 /\ b4) + (b4 /\ b5))
proof end;

theorem Th33: :: RMOD_3:33
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
b4 /\ (b3 + b5) = (b3 /\ b4) + (b4 /\ b5)
proof end;

Lemma31: for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 holds the carrier of (b3 + (b4 /\ b5)) c= the carrier of ((b4 + b3) /\ (b3 + b5))
proof end;

theorem Th34: :: RMOD_3:34
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 holds b3 + (b4 /\ b5) is Submodule of (b4 + b3) /\ (b3 + b5)
proof end;

Lemma32: for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
the carrier of (b4 + (b3 /\ b5)) = the carrier of ((b3 + b4) /\ (b4 + b5))
proof end;

theorem Th35: :: RMOD_3:35
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
b4 + (b3 /\ b5) = (b3 + b4) /\ (b4 + b5)
proof end;

theorem Th36: :: RMOD_3:36
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being strict Submodule of b2 st b5 is Submodule of b3 holds
b5 + (b4 /\ b3) = (b5 + b4) /\ b3
proof end;

theorem Th37: :: RMOD_3:37
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being strict Submodule of b2 holds
( b3 + b4 = b4 iff b3 /\ b4 = b3 )
proof end;

theorem Th38: :: RMOD_3:38
for b1 being Ring
for b2 being RightMod of b1
for b3 being Submodule of b2
for b4, b5 being strict Submodule of b2 st b3 is Submodule of b4 holds
b3 + b5 is Submodule of b4 + b5
proof end;

theorem Th39: :: RMOD_3:39
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 holds
b3 is Submodule of b4 + b5
proof end;

theorem Th40: :: RMOD_3:40
for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Submodule of b2 st b3 is Submodule of b4 & b5 is Submodule of b4 holds
b3 + b5 is Submodule of b4
proof end;

theorem Th41: :: RMOD_3:41
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds
( ( b3 is Submodule of b4 or b4 is Submodule of b3 ) iff ex b5 being Submodule of b2 st the carrier of b5 = the carrier of b3 \/ the carrier of b4 )
proof end;

definition
let c1 be Ring;
let c2 be RightMod of c1;
func Submodules c2 -> set means :Def3: :: RMOD_3:def 3
for b1 being set holds
( b1 in a3 iff ex b2 being strict Submodule of a2 st b2 = b1 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being strict Submodule of c2 st b3 = b2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being strict Submodule of c2 st b4 = b3 ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being strict Submodule of c2 st b4 = b3 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Submodules RMOD_3:def 3 :
for b1 being Ring
for b2 being RightMod of b1
for b3 being set holds
( b3 = Submodules b2 iff for b4 being set holds
( b4 in b3 iff ex b5 being strict Submodule of b2 st b5 = b4 ) );

registration
let c1 be Ring;
let c2 be RightMod of c1;
cluster Submodules a2 -> non empty ;
coherence
not Submodules c2 is empty
proof end;
end;

theorem Th42: :: RMOD_3:42
canceled;

theorem Th43: :: RMOD_3:43
canceled;

theorem Th44: :: RMOD_3:44
for b1 being Ring
for b2 being strict RightMod of b1 holds b2 in Submodules b2
proof end;

definition
let c1 be Ring;
let c2 be RightMod of c1;
let c3, c4 be Submodule of c2;
pred c2 is_the_direct_sum_of c3,c4 means :Def4: :: RMOD_3:def 4
( RightModStr(# the carrier of a2,the add of a2,the Zero of a2,the rmult of a2 #) = a3 + a4 & a3 /\ a4 = (0). a2 );
end;

:: deftheorem Def4 defines is_the_direct_sum_of RMOD_3:def 4 :
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds
( b2 is_the_direct_sum_of b3,b4 iff ( RightModStr(# the carrier of b2,the add of b2,the Zero of b2,the rmult of b2 #) = b3 + b4 & b3 /\ b4 = (0). b2 ) );

Lemma36: for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds
( b3 + b4 = RightModStr(# the carrier of b2,the add of b2,the Zero of b2,the rmult of b2 #) iff for b5 being Vector of b2 ex b6, b7 being Vector of b2 st
( b6 in b3 & b7 in b4 & b5 = b6 + b7 ) )
proof end;

Lemma37: for b1 being Ring
for b2 being RightMod of b1
for b3, b4, b5 being Vector of b2 holds
( b3 = b4 + b5 iff b4 = b3 - b5 )
proof end;

theorem Th45: :: RMOD_3:45
canceled;

theorem Th46: :: RMOD_3:46
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 st b2 is_the_direct_sum_of b3,b4 holds
b2 is_the_direct_sum_of b4,b3
proof end;

theorem Th47: :: RMOD_3:47
for b1 being Ring
for b2 being strict RightMod of b1 holds
( b2 is_the_direct_sum_of (0). b2, (Omega). b2 & b2 is_the_direct_sum_of (Omega). b2, (0). b2 )
proof end;

theorem Th48: :: RMOD_3:48
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being Coset of b3
for b6 being Coset of b4 st b5 meets b6 holds
b5 /\ b6 is Coset of b3 /\ b4
proof end;

theorem Th49: :: RMOD_3:49
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 holds
( b2 is_the_direct_sum_of b3,b4 iff for b5 being Coset of b3
for b6 being Coset of b4 ex b7 being Vector of b2 st b5 /\ b6 = {b7} )
proof end;

theorem Th50: :: RMOD_3:50
for b1 being Ring
for b2 being strict RightMod of b1
for b3, b4 being Submodule of b2 holds
( b3 + b4 = b2 iff for b5 being Vector of b2 ex b6, b7 being Vector of b2 st
( b6 in b3 & b7 in b4 & b5 = b6 + b7 ) ) by Lemma36;

theorem Th51: :: RMOD_3:51
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5, b6, b7, b8, b9 being Vector of b2 st b2 is_the_direct_sum_of b3,b4 & b5 = b6 + b7 & b5 = b8 + b9 & b6 in b3 & b8 in b3 & b7 in b4 & b9 in b4 holds
( b6 = b8 & b7 = b9 )
proof end;

theorem Th52: :: RMOD_3:52
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2 st b2 = b3 + b4 & ex b5 being Vector of b2 st
for b6, b7, b8, b9 being Vector of b2 st b5 = b6 + b7 & b5 = b8 + b9 & b6 in b3 & b8 in b3 & b7 in b4 & b9 in b4 holds
( b6 = b8 & b7 = b9 ) holds
b2 is_the_direct_sum_of b3,b4
proof end;

definition
let c1 be Ring;
let c2 be RightMod of c1;
let c3 be Vector of c2;
let c4, c5 be Submodule of c2;
assume E42: c2 is_the_direct_sum_of c4,c5 ;
func c3 |-- c4,c5 -> Element of [:the carrier of a2,the carrier of a2:] means :Def5: :: RMOD_3:def 5
( a3 = (a6 `1 ) + (a6 `2 ) & a6 `1 in a4 & a6 `2 in a5 );
existence
ex b1 being Element of [:the carrier of c2,the carrier of c2:] st
( c3 = (b1 `1 ) + (b1 `2 ) & b1 `1 in c4 & b1 `2 in c5 )
proof end;
uniqueness
for b1, b2 being Element of [:the carrier of c2,the carrier of c2:] st c3 = (b1 `1 ) + (b1 `2 ) & b1 `1 in c4 & b1 `2 in c5 & c3 = (b2 `1 ) + (b2 `2 ) & b2 `1 in c4 & b2 `2 in c5 holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines |-- RMOD_3:def 5 :
for b1 being Ring
for b2 being RightMod of b1
for b3 being Vector of b2
for b4, b5 being Submodule of b2 st b2 is_the_direct_sum_of b4,b5 holds
for b6 being Element of [:the carrier of b2,the carrier of b2:] holds
( b6 = b3 |-- b4,b5 iff ( b3 = (b6 `1 ) + (b6 `2 ) & b6 `1 in b4 & b6 `2 in b5 ) );

theorem Th53: :: RMOD_3:53
canceled;

theorem Th54: :: RMOD_3:54
canceled;

theorem Th55: :: RMOD_3:55
canceled;

theorem Th56: :: RMOD_3:56
canceled;

theorem Th57: :: RMOD_3:57
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being Vector of b2 st b2 is_the_direct_sum_of b3,b4 holds
(b5 |-- b3,b4) `1 = (b5 |-- b4,b3) `2
proof end;

theorem Th58: :: RMOD_3:58
for b1 being Ring
for b2 being RightMod of b1
for b3, b4 being Submodule of b2
for b5 being Vector of b2 st b2 is_the_direct_sum_of b3,b4 holds
(b5 |-- b3,b4) `2 = (b5 |-- b4,b3) `1
proof end;

definition
let c1 be Ring;
let c2 be RightMod of c1;
func SubJoin c2 -> BinOp of Submodules a2 means :Def6: :: RMOD_3:def 6
for b1, b2 being Element of Submodules a2
for b3, b4 being Submodule of a2 st b1 = b3 & b2 = b4 holds
a3 . b1,b2 = b3 + b4;
existence
ex b1 being BinOp of Submodules c2 st
for b2, b3 being Element of Submodules c2
for b4, b5 being Submodule of c2 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 + b5
proof end;
uniqueness
for b1, b2 being BinOp of Submodules c2 st ( for b3, b4 being Element of Submodules c2
for b5, b6 being Submodule of c2 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 + b6 ) & ( for b3, b4 being Element of Submodules c2
for b5, b6 being Submodule of c2 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 + b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines SubJoin RMOD_3:def 6 :
for b1 being Ring
for b2 being RightMod of b1
for b3 being BinOp of Submodules b2 holds
( b3 = SubJoin b2 iff for b4, b5 being Element of Submodules b2
for b6, b7 being Submodule of b2 st b4 = b6 & b5 = b7 holds
b3 . b4,b5 = b6 + b7 );

definition
let c1 be Ring;
let c2 be RightMod of c1;
func SubMeet c2 -> BinOp of Submodules a2 means :Def7: :: RMOD_3:def 7
for b1, b2 being Element of Submodules a2
for b3, b4 being Submodule of a2 st b1 = b3 & b2 = b4 holds
a3 . b1,b2 = b3 /\ b4;
existence
ex b1 being BinOp of Submodules c2 st
for b2, b3 being Element of Submodules c2
for b4, b5 being Submodule of c2 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 /\ b5
proof end;
uniqueness
for b1, b2 being BinOp of Submodules c2 st ( for b3, b4 being Element of Submodules c2
for b5, b6 being Submodule of c2 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 /\ b6 ) & ( for b3, b4 being Element of Submodules c2
for b5, b6 being Submodule of c2 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 /\ b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines SubMeet RMOD_3:def 7 :
for b1 being Ring
for b2 being RightMod of b1
for b3 being BinOp of Submodules b2 holds
( b3 = SubMeet b2 iff for b4, b5 being Element of Submodules b2
for b6, b7 being Submodule of b2 st b4 = b6 & b5 = b7 holds
b3 . b4,b5 = b6 /\ b7 );

theorem Th59: :: RMOD_3:59
canceled;

theorem Th60: :: RMOD_3:60
canceled;

theorem Th61: :: RMOD_3:61
canceled;

theorem Th62: :: RMOD_3:62
canceled;

theorem Th63: :: RMOD_3:63
for b1 being Ring
for b2 being RightMod of b1 holds LattStr(# (Submodules b2),(SubJoin b2),(SubMeet b2) #) is Lattice
proof end;

theorem Th64: :: RMOD_3:64
for b1 being Ring
for b2 being RightMod of b1 holds LattStr(# (Submodules b2),(SubJoin b2),(SubMeet b2) #) is 0_Lattice
proof end;

theorem Th65: :: RMOD_3:65
for b1 being Ring
for b2 being RightMod of b1 holds LattStr(# (Submodules b2),(SubJoin b2),(SubMeet b2) #) is 1_Lattice
proof end;

theorem Th66: :: RMOD_3:66
for b1 being Ring
for b2 being RightMod of b1 holds LattStr(# (Submodules b2),(SubJoin b2),(SubMeet b2) #) is 01_Lattice
proof end;

theorem Th67: :: RMOD_3:67
for b1 being Ring
for b2 being RightMod of b1 holds LattStr(# (Submodules b2),(SubJoin b2),(SubMeet b2) #) is M_Lattice
proof end;