:: RMOD_3 semantic presentation

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 )  }
proof
reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RMOD_2:def_2;
set VS =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ;
  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  or x in the carrier of V )
assume  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ; ::_thesis: x in the carrier of V
then  ex v1, v2 being Vector of V st
( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
hence  x in the carrier of V ; ::_thesis: verum
end;
then reconsider VS =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  as Subset of V ;
A1: 0. V = (0. V) + (0. V) by RLVECT_1:def_4;
 ( 0. V in W1 & 0. V in W2 ) by RMOD_2:17;
then A2: 0. V in VS by A1;
A3: VS =  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }
proof
thus  VS c=  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }  c= VS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VS or x in  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }  )
assume  x in VS ; ::_thesis: x in  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }
then consider v, u being Vector of V such that
A4: x = v + u and
A5: ( v in W1 & u in W2 ) ;
 ( v in V1 & u in V2 ) by A5, STRUCT_0:def_5;
hence  x in  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }  or x in VS )
assume  x in  {  (v + u) where v, u is Vector of V : ( v in V1 & u in V2 )  }  ; ::_thesis: x in VS
then consider v, u being Vector of V such that
A6: x = v + u and
A7: ( v in V1 & u in V2 ) ;
 ( v in W1 & u in W2 ) by A7, STRUCT_0:def_5;
hence  x in VS by A6; ::_thesis: verum
end;
 ( V1 is linearly-closed & V2 is linearly-closed ) by RMOD_2:33;
hence  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 )  }  by A2, A3, RMOD_2:6, RMOD_2:34; ::_thesis: verum
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 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
proof
set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of V;
 0. V in W2 by RMOD_2:17;
then A1: 0. V in the carrier of W2 by STRUCT_0:def_5;
 ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RMOD_2:def_2;
then  the carrier of W1 /\ the carrier of W2 c= the carrier of V /\ the carrier of V by XBOOLE_1:27;
then reconsider V1 = the carrier of W1, V2 = the carrier of W2, V3 = the carrier of W1 /\ the carrier of W2 as Subset of V by RMOD_2:def_2;
 ( V1 is linearly-closed & V2 is linearly-closed ) by RMOD_2:33;
then A2: V3 is linearly-closed by RMOD_2:7;
 0. V in W1 by RMOD_2:17;
then  0. V in the carrier of W1 by STRUCT_0:def_5;
then  the carrier of W1 /\ the carrier of W2 <> {} by A1, XBOOLE_0:def_4;
hence  ex b1 being strict Submodule of V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 by A2, RMOD_2:34; ::_thesis: verum
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 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 ) )
proof
let R be Ring; ::_thesis: 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 ) )
let V be RightMod of R; ::_thesis: 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 ) )
let W1, W2 be Submodule of V; ::_thesis: 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 ) )
let x be set ; ::_thesis: ( x in W1 + W2 iff ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
thus  ( x in W1 + W2 implies ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) ::_thesis: ( ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) implies x in W1 + W2 )
proof
assume  x in W1 + W2 ; ::_thesis: ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 )
then  x in the carrier of (W1 + W2) by STRUCT_0:def_5;
then  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by Def1;
then consider v1, v2 being Vector of V such that
A1: ( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
take  v1 ; ::_thesis: ex v2 being Vector of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 )
take  v2 ; ::_thesis: ( v1 in W1 & v2 in W2 & x = v1 + v2 )
thus  ( v1 in W1 & v2 in W2 & x = v1 + v2 ) by A1; ::_thesis: verum
end;
given v1, v2 being Vector of V such that A2: ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ; ::_thesis: x in W1 + W2
 x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by A2;
then  x in the carrier of (W1 + W2) by Def1;
hence  x in W1 + W2 by STRUCT_0:def_5; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2 be Submodule of V; ::_thesis: for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
let v be Vector of V; ::_thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 )
assume A1: ( v in W1 or v in W2 ) ; ::_thesis: v in W1 + W2
now__::_thesis:_v_in_W1_+_W2
percases ( v in W1 or v in W2 ) by A1;
supposeA2: v in W1 ; ::_thesis: v in W1 + W2
 ( v = v + (0. V) & 0. V in W2 ) by RLVECT_1:def_4, RMOD_2:17;
hence  v in W1 + W2 by A2, Th1; ::_thesis: verum
end;
supposeA3: v in W2 ; ::_thesis: v in W1 + W2
 ( v = (0. V) + v & 0. V in W1 ) by RLVECT_1:def_4, RMOD_2:17;
hence  v in W1 + W2 by A3, Th1; ::_thesis: verum
end;
end;
end;
hence  v in W1 + W2 ; ::_thesis: verum
end;

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 ) )
proof
let R be Ring; ::_thesis: 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 ) )
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let W1, W2 be Submodule of V; ::_thesis: for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let x be set ; ::_thesis: ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
 ( x in W1 /\ W2 iff x in the carrier of (W1 /\ W2) ) by STRUCT_0:def_5;
then  ( x in W1 /\ W2 iff x in the carrier of W1 /\ the carrier of W2 ) by Def2;
then  ( x in W1 /\ W2 iff ( x in the carrier of W1 & x in the carrier of W2 ) ) by XBOOLE_0:def_4;
hence  ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) by STRUCT_0:def_5; ::_thesis: verum
end;

Lm1:  for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds W1 + W2 = W2 + W1
let W1, W2 be Submodule of V; ::_thesis: W1 + W2 = W2 + W1
set A =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ;
set B =  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  ;
A1:  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  c=  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  or x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  )
assume  x in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }
then  ex v, u being Vector of V st
( x = v + u & v in W2 & u in W1 ) ;
hence  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ; ::_thesis: verum
end;
A2: the carrier of (W1 + W2) =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by Def1;
  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  c=  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  or x in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  )
assume  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }
then  ex v, u being Vector of V st
( x = v + u & v in W1 & u in W2 ) ;
hence  x in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  ; ::_thesis: verum
end;
then   {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  =  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W1 )  }  by A1, XBOOLE_0:def_10;
hence  W1 + W2 = W2 + W1 by A2, Def1; ::_thesis: verum
end;

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)
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds the carrier of W1 c= the carrier of (W1 + W2)
let W1, W2 be Submodule of V; ::_thesis: the carrier of W1 c= the carrier of (W1 + W2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 + W2) )
set A =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ;
assume  x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 + W2)
then reconsider v = x as Element of W1 ;
reconsider v = v as Vector of V by RMOD_2:10;
A1: v = v + (0. V) by RLVECT_1:def_4;
 ( v in W1 & 0. V in W2 ) by RMOD_2:17, STRUCT_0:def_5;
then  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by A1;
hence  x in the carrier of (W1 + W2) by Def1; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1 be Submodule of V; ::_thesis: for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W2 be strict Submodule of V; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )
assume A1: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 + W2 = W2
A2: the carrier of (W1 + W2) c= the carrier of W2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 )
assume  x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of W2
then  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by Def1;
then consider v, u being Vector of V such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2 ;
 W1 is Submodule of W2 by A1, RMOD_2:27;
then  v in W2 by A4, RMOD_2:8;
then  v + u in W2 by A5, RMOD_2:20;
hence  x in the carrier of W2 by A3, STRUCT_0:def_5; ::_thesis: verum
end;
 W1 + W2 = W2 + W1 by Lm1;
then  the carrier of W2 c= the carrier of (W1 + W2) by Lm2;
then  the carrier of (W1 + W2) = the carrier of W2 by A2, XBOOLE_0:def_10;
hence  W1 + W2 = W2 by RMOD_2:29; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3
let V be RightMod of R; ::_thesis: for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Submodule of V; ::_thesis: W1 + (W2 + W3) = (W1 + W2) + W3
set A =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  ;
set B =  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W3 )  }  ;
set C =  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  ;
set D =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  ;
A1: the carrier of (W1 + (W2 + W3)) =  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  by Def1;
A2:  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  c=  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  or x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  )
assume  x in  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }
then consider v, u being Vector of V such that
A3: x = v + u and
A4: v in W1 + W2 and
A5: u in W3 ;
 v in the carrier of (W1 + W2) by A4, STRUCT_0:def_5;
then  v in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by Def1;
then consider u1, u2 being Vector of V such that
A6: v = u1 + u2 and
A7: u1 in W1 and
A8: u2 in W2 ;
 u2 + u in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W3 )  }  by A5, A8;
then  u2 + u in the carrier of (W2 + W3) by Def1;
then A9: u2 + u in W2 + W3 by STRUCT_0:def_5;
 v + u = u1 + (u2 + u) by A6, RLVECT_1:def_3;
hence  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  by A3, A7, A9; ::_thesis: verum
end;
  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  c=  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  or x in  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  )
assume  x in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }
then consider v, u being Vector of V such that
A10: x = v + u and
A11: v in W1 and
A12: u in W2 + W3 ;
 u in the carrier of (W2 + W3) by A12, STRUCT_0:def_5;
then  u in  {  (v + u) where v, u is Vector of V : ( v in W2 & u in W3 )  }  by Def1;
then consider u1, u2 being Vector of V such that
A13: u = u1 + u2 and
A14: u1 in W2 and
A15: u2 in W3 ;
 v + u1 in  {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 )  }  by A11, A14;
then  v + u1 in the carrier of (W1 + W2) by Def1;
then A16: v + u1 in W1 + W2 by STRUCT_0:def_5;
 v + u = (v + u1) + u2 by A13, RLVECT_1:def_3;
hence  x in  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  by A10, A15, A16; ::_thesis: verum
end;
then   {  (v + u) where v, u is Vector of V : ( v in W1 & u in W2 + W3 )  }  =  {  (v + u) where v, u is Vector of V : ( v in W1 + W2 & u in W3 )  }  by A2, XBOOLE_0:def_10;
hence  W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds
( W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2 )
let W1, W2 be Submodule of V; ::_thesis: ( W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2 )
 the carrier of W1 c= the carrier of (W1 + W2) by Lm2;
hence  W1 is Submodule of W1 + W2 by RMOD_2:27; ::_thesis: W2 is Submodule of W1 + W2
 the carrier of W2 c= the carrier of (W2 + W1) by Lm2;
then  the carrier of W2 c= the carrier of (W1 + W2) by Lm1;
hence  W2 is Submodule of W1 + W2 by RMOD_2:27; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be RightMod of R; ::_thesis: for W1 being Submodule of V
for W2 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 + W2 = W2 )
let W1 be Submodule of V; ::_thesis: for W2 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 + W2 = W2 )
let W2 be strict Submodule of V; ::_thesis: ( W1 is Submodule of W2 iff W1 + W2 = W2 )
thus  ( W1 is Submodule of W2 implies W1 + W2 = W2 ) ::_thesis: ( W1 + W2 = W2 implies W1 is Submodule of W2 )
proof
assume  W1 is Submodule of W2 ; ::_thesis: W1 + W2 = W2
then  the carrier of W1 c= the carrier of W2 by RMOD_2:def_2;
hence  W1 + W2 = W2 by Lm3; ::_thesis: verum
end;
thus  ( W1 + W2 = W2 implies W1 is Submodule of W2 ) by Th7; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W being strict Submodule of V holds
( ((0). V) + W = W & W + ((0). V) = W )
let V be RightMod of R; ::_thesis: for W being strict Submodule of V holds
( ((0). V) + W = W & W + ((0). V) = W )
let W be strict Submodule of V; ::_thesis: ( ((0). V) + W = W & W + ((0). V) = W )
 (0). V is Submodule of W by RMOD_2:39;
then  the carrier of ((0). V) c= the carrier of W by RMOD_2:def_2;
hence  ((0). V) + W = W by Lm3; ::_thesis: W + ((0). V) = W
hence  W + ((0). V) = W by Lm1; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be RightMod of R; ::_thesis: 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 )
let W, W9, W1 be Submodule of V; ::_thesis: ( the carrier of W = the carrier of W9 implies ( W1 + W = W1 + W9 & W + W1 = W9 + W1 ) )
assume A1: the carrier of W = the carrier of W9 ; ::_thesis: ( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
A2: now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_W1_+_W_implies_v_in_W1_+_W9_)_&_(_v_in_W1_+_W9_implies_v_in_W1_+_W_)_)
let v be Vector of V; ::_thesis: ( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) )
set W1W9 =  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W9 )  }  ;
set W1W =  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W )  }  ;
thus  ( v in W1 + W implies v in W1 + W9 ) ::_thesis: ( v in W1 + W9 implies v in W1 + W )
proof
assume  v in W1 + W ; ::_thesis: v in W1 + W9
then  v in the carrier of (W1 + W) by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W )  }  by Def1;
then consider v1, v2 being Vector of V such that
A3: ( v = v1 + v2 & v1 in W1 ) and
A4: v2 in W ;
 v2 in the carrier of W9 by A1, A4, STRUCT_0:def_5;
then  v2 in W9 by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W9 )  }  by A3;
then  v in the carrier of (W1 + W9) by Def1;
hence  v in W1 + W9 by STRUCT_0:def_5; ::_thesis: verum
end;
assume  v in W1 + W9 ; ::_thesis: v in W1 + W
then  v in the carrier of (W1 + W9) by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W9 )  }  by Def1;
then consider v1, v2 being Vector of V such that
A5: ( v = v1 + v2 & v1 in W1 ) and
A6: v2 in W9 ;
 v2 in the carrier of W by A1, A6, STRUCT_0:def_5;
then  v2 in W by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W )  }  by A5;
then  v in the carrier of (W1 + W) by Def1;
hence  v in W1 + W by STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 + W = W1 + W9 by RMOD_2:30; ::_thesis: W + W1 = W9 + W1
 ( W1 + W = W + W1 & W1 + W9 = W9 + W1 ) by Lm1;
hence  W + W1 = W9 + W1 by A2, RMOD_2:30; ::_thesis: verum
end;

Lm5:  for R being Ring
for V being RightMod of R
for W being Submodule of V holds W is Submodule of (Omega). V
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W being Submodule of V holds W is Submodule of (Omega). V
let V be RightMod of R; ::_thesis: for W being Submodule of V holds W is Submodule of (Omega). V
let W be Submodule of V; ::_thesis: W is Submodule of (Omega). V
thus  the carrier of W c= the carrier of ((Omega). V) by RMOD_2:def_2; :: according to RMOD_2:def_2 ::_thesis: ( 0. W = 0. ((Omega). V) & the U7 of W = the U7 of ((Omega). V) | [: the carrier of W, the carrier of W:] & the rmult of W = the rmult of ((Omega). V) | [: the carrier of W, the carrier of R:] )
thus  0. W = 0. V by RMOD_2:def_2
.= 0. ((Omega). V) ; ::_thesis: ( the U7 of W = the U7 of ((Omega). V) | [: the carrier of W, the carrier of W:] & the rmult of W = the rmult of ((Omega). V) | [: the carrier of W, the carrier of R:] )
thus  ( the U7 of W = the U7 of ((Omega). V) | [: the carrier of W, the carrier of W:] & the rmult of W = the rmult of ((Omega). V) | [: the carrier of W, the carrier of R:] ) by RMOD_2:def_2; ::_thesis: verum
end;

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 #) )
proof
let R be Ring; ::_thesis: 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 #) )
let V be RightMod of R; ::_thesis: 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 #) )
let W be Submodule of V; ::_thesis: ( ((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 #) )
consider W9 being strict Submodule of V such that
A1: the carrier of W9 = the carrier of ((Omega). V) ;
A2: the carrier of W c= the carrier of W9 by A1, RMOD_2:def_2;
A3: W9 is Submodule of (Omega). V by Lm5;
W + ((Omega). V) = W + W9 by A1, Lm4
.= W9 by A2, Lm3
.= RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) by A1, A3, RMOD_2:31 ;
hence  ( ((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 #) ) by Lm1; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W being strict Submodule of V holds W /\ W = W
let V be RightMod of R; ::_thesis: for W being strict Submodule of V holds W /\ W = W
let W be strict Submodule of V; ::_thesis: W /\ W = W
 the carrier of W = the carrier of W /\ the carrier of W ;
hence  W /\ W = W by Def2; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds W1 /\ W2 = W2 /\ W1
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds W1 /\ W2 = W2 /\ W1
let W1, W2 be Submodule of V; ::_thesis: W1 /\ W2 = W2 /\ W1
 the carrier of (W1 /\ W2) = the carrier of W2 /\ the carrier of W1 by Def2;
hence  W1 /\ W2 = W2 /\ W1 by Def2; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let V be RightMod of R; ::_thesis: for W1, W2, W3 being Submodule of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let W1, W2, W3 be Submodule of V; ::_thesis: W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
set V1 = the carrier of W1;
set V2 = the carrier of W2;
set V3 = the carrier of W3;
the carrier of (W1 /\ (W2 /\ W3)) = the carrier of W1 /\ the carrier of (W2 /\ W3) by Def2
.= the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) by Def2
.= ( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 by XBOOLE_1:16
.= the carrier of (W1 /\ W2) /\ the carrier of W3 by Def2 ;
hence  W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by Def2; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of W1
let W1, W2 be Submodule of V; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of W1
 the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence  the carrier of (W1 /\ W2) c= the carrier of W1 by XBOOLE_1:17; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds
( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )
let W1, W2 be Submodule of V; ::_thesis: ( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )
 the carrier of (W1 /\ W2) c= the carrier of W1 by Lm6;
hence  W1 /\ W2 is Submodule of W1 by RMOD_2:27; ::_thesis: W1 /\ W2 is Submodule of W2
 the carrier of (W2 /\ W1) c= the carrier of W2 by Lm6;
then  the carrier of (W1 /\ W2) c= the carrier of W2 by Th14;
hence  W1 /\ W2 is Submodule of W2 by RMOD_2:27; ::_thesis: verum
end;

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 ) )
proof
let R be Ring; ::_thesis: 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 ) )
let V be RightMod of R; ::_thesis: 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 ) )
let W2 be Submodule of V; ::_thesis: ( ( 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 ) )
thus  for W1 being strict Submodule of V st W1 is Submodule of W2 holds
W1 /\ W2 = W1 ::_thesis: for W1 being Submodule of V st W1 /\ W2 = W1 holds
W1 is Submodule of W2
proof
let W1 be strict Submodule of V; ::_thesis: ( W1 is Submodule of W2 implies W1 /\ W2 = W1 )
assume  W1 is Submodule of W2 ; ::_thesis: W1 /\ W2 = W1
then A1: the carrier of W1 c= the carrier of W2 by RMOD_2:def_2;
 the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence  W1 /\ W2 = W1 by A1, RMOD_2:29, XBOOLE_1:28; ::_thesis: verum
end;
thus  for W1 being Submodule of V st W1 /\ W2 = W1 holds
W1 is Submodule of W2 by Th16; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 /\ W3 is Submodule of W2 /\ W3
let W1, W2, W3 be Submodule of V; ::_thesis: ( W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3 )
set A1 = the carrier of W1;
set A2 = the carrier of W2;
set A3 = the carrier of W3;
set A4 = the carrier of (W1 /\ W3);
assume  W1 is Submodule of W2 ; ::_thesis: W1 /\ W3 is Submodule of W2 /\ W3
then  the carrier of W1 c= the carrier of W2 by RMOD_2:def_2;
then  the carrier of W1 /\ the carrier of W3 c= the carrier of W2 /\ the carrier of W3 by XBOOLE_1:26;
then  the carrier of (W1 /\ W3) c= the carrier of W2 /\ the carrier of W3 by Def2;
then  the carrier of (W1 /\ W3) c= the carrier of (W2 /\ W3) by Def2;
hence  W1 /\ W3 is Submodule of W2 /\ W3 by RMOD_2:27; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: for W1, W3, W2 being Submodule of V st W1 is Submodule of W3 holds
W1 /\ W2 is Submodule of W3
let W1, W3, W2 be Submodule of V; ::_thesis: ( W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3 )
assume A1: W1 is Submodule of W3 ; ::_thesis: W1 /\ W2 is Submodule of W3
 W1 /\ W2 is Submodule of W1 by Th16;
hence  W1 /\ W2 is Submodule of W3 by A1, RMOD_2:26; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2, W3 be Submodule of V; ::_thesis: ( W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of W2 /\ W3 )
assume A1: ( W1 is Submodule of W2 & W1 is Submodule of W3 ) ; ::_thesis: W1 is Submodule of W2 /\ W3
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_W1_holds_
v_in_W2_/\_W3
let v be Vector of V; ::_thesis: ( v in W1 implies v in W2 /\ W3 )
assume  v in W1 ; ::_thesis: v in W2 /\ W3
then  ( v in W2 & v in W3 ) by A1, RMOD_2:8;
hence  v in W2 /\ W3 by Th3; ::_thesis: verum
end;
hence  W1 is Submodule of W2 /\ W3 by RMOD_2:28; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W being Submodule of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let V be RightMod of R; ::_thesis: for W being Submodule of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let W be Submodule of V; ::_thesis: ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
 0. V in W by RMOD_2:17;
then  0. V in the carrier of W by STRUCT_0:def_5;
then  {(0. V)} c= the carrier of W by ZFMISC_1:31;
then A1: {(0. V)} /\ the carrier of W = {(0. V)} by XBOOLE_1:28;
the carrier of (((0). V) /\ W) = the carrier of ((0). V) /\ the carrier of W by Def2
.= {(0. V)} /\ the carrier of W by RMOD_2:def_3 ;
hence  ((0). V) /\ W = (0). V by A1, RMOD_2:def_3; ::_thesis: W /\ ((0). V) = (0). V
hence  W /\ ((0). V) = (0). V by Th14; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W being strict Submodule of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
let V be RightMod of R; ::_thesis: for W being strict Submodule of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
let W be strict Submodule of V; ::_thesis: ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
 ( the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W & the carrier of W c= the carrier of V ) by Def2, RMOD_2:def_2;
hence  ((Omega). V) /\ W = W by RMOD_2:29, XBOOLE_1:28; ::_thesis: W /\ ((Omega). V) = W
hence  W /\ ((Omega). V) = W by Th14; ::_thesis: verum
end;

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)
proof
let R be Ring; ::_thesis: 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)
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
let W1, W2 be Submodule of V; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
 ( the carrier of (W1 /\ W2) c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) ) by Lm2, Lm6;
hence  the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) by XBOOLE_1:1; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let W1, W2 be Submodule of V; ::_thesis: the carrier of ((W1 /\ W2) + W2) = the carrier of W2
thus  the carrier of ((W1 /\ W2) + W2) c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + W2) or x in the carrier of W2 )
assume  x in the carrier of ((W1 /\ W2) + W2) ; ::_thesis: x in the carrier of W2
then  x in  {  (u + v) where u, v is Vector of V : ( u in W1 /\ W2 & v in W2 )  }  by Def1;
then consider u, v being Vector of V such that
A1: x = u + v and
A2: u in W1 /\ W2 and
A3: v in W2 ;
 u in W2 by A2, Th3;
then  u + v in W2 by A3, RMOD_2:20;
hence  x in the carrier of W2 by A1, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W2 or x in the carrier of ((W1 /\ W2) + W2) )
 the carrier of W2 c= the carrier of (W2 + (W1 /\ W2)) by Lm2;
then A4: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) by Lm1;
assume  x in the carrier of W2 ; ::_thesis: x in the carrier of ((W1 /\ W2) + W2)
hence  x in the carrier of ((W1 /\ W2) + W2) by A4; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Submodule of V; ::_thesis: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
thus  the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W1 c= the carrier of (W1 /\ (W1 + W2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 /\ (W1 + W2)) or x in the carrier of W1 )
assume A1: x in the carrier of (W1 /\ (W1 + W2)) ; ::_thesis: x in the carrier of W1
 the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 /\ the carrier of (W1 + W2) by Def2;
hence  x in the carrier of W1 by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) )
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 /\ (W1 + W2))
 the carrier of W1 c= the carrier of V by RMOD_2:def_2;
then reconsider x1 = x as Element of V by A2;
A3: ( x1 + (0. V) = x1 & 0. V in W2 ) by RLVECT_1:def_4, RMOD_2:17;
 x in W1 by A2, STRUCT_0:def_5;
then  x in  {  (u + v) where u, v is Vector of V : ( u in W1 & v in W2 )  }  by A3;
then  x in the carrier of (W1 + W2) by Def1;
then  x in the carrier of W1 /\ the carrier of (W1 + W2) by A2, XBOOLE_0:def_4;
hence  x in the carrier of (W1 /\ (W1 + W2)) by Def2; ::_thesis: verum
end;

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))
proof
let R be Ring; ::_thesis: 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))
let V be RightMod of R; ::_thesis: for W1, W2, W3 being Submodule of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let W1, W2, W3 be Submodule of V; ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) or x in the carrier of (W2 /\ (W1 + W3)) )
assume  x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) ; ::_thesis: x in the carrier of (W2 /\ (W1 + W3))
then  x in  {  (u + v) where u, v is Vector of V : ( u in W1 /\ W2 & v in W2 /\ W3 )  }  by Def1;
then consider u, v being Vector of V such that
A1: x = u + v and
A2: ( u in W1 /\ W2 & v in W2 /\ W3 ) ;
 ( u in W2 & v in W2 ) by A2, Th3;
then A3: x in W2 by A1, RMOD_2:20;
 ( u in W1 & v in W3 ) by A2, Th3;
then  x in W1 + W3 by A1, Th1;
then  x in W2 /\ (W1 + W3) by A3, Th3;
hence  x in the carrier of (W2 /\ (W1 + W3)) by STRUCT_0:def_5; ::_thesis: verum
end;

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))
proof
let R be Ring; ::_thesis: 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))
let V be RightMod of R; ::_thesis: 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))
let W1, W2, W3 be Submodule of V; ::_thesis: ( W1 is Submodule of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume A1: W1 is Submodule of W2 ; ::_thesis: the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
thus  the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 /\ (W1 + W3)) or x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume  x in the carrier of (W2 /\ (W1 + W3)) ; ::_thesis: x in the carrier of ((W1 /\ W2) + (W2 /\ W3))
then A2: x in the carrier of W2 /\ the carrier of (W1 + W3) by Def2;
then  x in the carrier of (W1 + W3) by XBOOLE_0:def_4;
then  x in  {  (u + v) where u, v is Vector of V : ( u in W1 & v in W3 )  }  by Def1;
then consider u1, v1 being Vector of V such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3 ;
A6: u1 in W2 by A1, A4, RMOD_2:8;
 x in the carrier of W2 by A2, XBOOLE_0:def_4;
then  u1 + v1 in W2 by A3, STRUCT_0:def_5;
then  (v1 + u1) - u1 in W2 by A6, RMOD_2:23;
then  v1 + (u1 - u1) in W2 by RLVECT_1:def_3;
then  v1 + (0. V) in W2 by VECTSP_1:19;
then  v1 in W2 by RLVECT_1:def_4;
then A7: v1 in W2 /\ W3 by A5, Th3;
 u1 in W1 /\ W2 by A4, A6, Th3;
then  x in (W1 /\ W2) + (W2 /\ W3) by A3, A7, Th1;
hence  x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) by STRUCT_0:def_5; ::_thesis: verum
end;
thus  the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) by Lm10; ::_thesis: verum
end;

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))
proof
let R be Ring; ::_thesis: 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))
let V be RightMod of R; ::_thesis: for W2, W1, W3 being Submodule of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let W2, W1, W3 be Submodule of V; ::_thesis: the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 + (W1 /\ W3)) or x in the carrier of ((W1 + W2) /\ (W2 + W3)) )
assume  x in the carrier of (W2 + (W1 /\ W3)) ; ::_thesis: x in the carrier of ((W1 + W2) /\ (W2 + W3))
then  x in  {  (u + v) where u, v is Vector of V : ( u in W2 & v in W1 /\ W3 )  }  by Def1;
then consider u, v being Vector of V such that
A1: ( x = u + v & u in W2 ) and
A2: v in W1 /\ W3 ;
 v in W3 by A2, Th3;
then  x in  {  (u1 + u2) where u1, u2 is Vector of V : ( u1 in W2 & u2 in W3 )  }  by A1;
then A3: x in the carrier of (W2 + W3) by Def1;
 v in W1 by A2, Th3;
then  x in  {  (v1 + v2) where v1, v2 is Vector of V : ( v1 in W1 & v2 in W2 )  }  by A1;
then  x in the carrier of (W1 + W2) by Def1;
then  x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by A3, XBOOLE_0:def_4;
hence  x in the carrier of ((W1 + W2) /\ (W2 + W3)) by Def2; ::_thesis: verum
end;

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))
proof
let R be Ring; ::_thesis: 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))
let V be RightMod of R; ::_thesis: 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))
let W1, W2, W3 be Submodule of V; ::_thesis: ( W1 is Submodule of W2 implies the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) )
reconsider V2 = the carrier of W2 as Subset of V by RMOD_2:def_2;
A1: V2 is linearly-closed by RMOD_2:33;
assume  W1 is Submodule of W2 ; ::_thesis: the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
then A2: the carrier of W1 c= the carrier of W2 by RMOD_2:def_2;
thus  the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm12; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 + W2) /\ (W2 + W3)) c= the carrier of (W2 + (W1 /\ W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 + W2) /\ (W2 + W3)) or x in the carrier of (W2 + (W1 /\ W3)) )
assume  x in the carrier of ((W1 + W2) /\ (W2 + W3)) ; ::_thesis: x in the carrier of (W2 + (W1 /\ W3))
then  x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by Def2;
then  x in the carrier of (W1 + W2) by XBOOLE_0:def_4;
then  x in  {  (u1 + u2) where u1, u2 is Vector of V : ( u1 in W1 & u2 in W2 )  }  by Def1;
then consider u1, u2 being Vector of V such that
A3: x = u1 + u2 and
A4: ( u1 in W1 & u2 in W2 ) ;
 ( u1 in the carrier of W1 & u2 in the carrier of W2 ) by A4, STRUCT_0:def_5;
then  u1 + u2 in V2 by A2, A1, RMOD_2:def_1;
then A5: u1 + u2 in W2 by STRUCT_0:def_5;
 ( 0. V in W1 /\ W3 & (u1 + u2) + (0. V) = u1 + u2 ) by RLVECT_1:def_4, RMOD_2:17;
then  x in  {  (u + v) where u, v is Vector of V : ( u in W2 & v in W1 /\ W3 )  }  by A3, A5;
hence  x in the carrier of (W2 + (W1 /\ W3)) by Def1; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W3, W2 be Submodule of V; ::_thesis: for W1 being strict Submodule of V st W1 is Submodule of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let W1 be strict Submodule of V; ::_thesis: ( W1 is Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3 )
assume A1: W1 is Submodule of W3 ; ::_thesis: W1 + (W2 /\ W3) = (W1 + W2) /\ W3
thus (W1 + W2) /\ W3 = W3 /\ (W1 + W2) by Th14
.= (W1 /\ W3) + (W3 /\ W2) by A1, Lm11, RMOD_2:29
.= W1 + (W3 /\ W2) by A1, Th17
.= W1 + (W2 /\ W3) by Th14 ; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for W1, W2 being strict Submodule of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let V be RightMod of R; ::_thesis: for W1, W2 being strict Submodule of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let W1, W2 be strict Submodule of V; ::_thesis: ( W1 + W2 = W2 iff W1 /\ W2 = W1 )
 ( W1 + W2 = W2 iff W1 is Submodule of W2 ) by Th8;
hence  ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) by Th17; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1 be Submodule of V; ::_thesis: for W2, W3 being strict Submodule of V st W1 is Submodule of W2 holds
W1 + W3 is Submodule of W2 + W3
let W2, W3 be strict Submodule of V; ::_thesis: ( W1 is Submodule of W2 implies W1 + W3 is Submodule of W2 + W3 )
assume A1: W1 is Submodule of W2 ; ::_thesis: W1 + W3 is Submodule of W2 + W3
(W1 + W3) + (W2 + W3) = (W1 + W3) + (W3 + W2) by Lm1
.= ((W1 + W3) + W3) + W2 by Th6
.= (W1 + (W3 + W3)) + W2 by Th6
.= (W1 + W3) + W2 by Lm3
.= W1 + (W3 + W2) by Th6
.= W1 + (W2 + W3) by Lm1
.= (W1 + W2) + W3 by Th6
.= W2 + W3 by A1, Th8 ;
hence  W1 + W3 is Submodule of W2 + W3 by Th8; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 is Submodule of W2 + W3
let W1, W2, W3 be Submodule of V; ::_thesis: ( W1 is Submodule of W2 implies W1 is Submodule of W2 + W3 )
assume A1: W1 is Submodule of W2 ; ::_thesis: W1 is Submodule of W2 + W3
 W2 is Submodule of W2 + W3 by Th7;
hence  W1 is Submodule of W2 + W3 by A1, RMOD_2:26; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W3, W2 be Submodule of V; ::_thesis: ( W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is Submodule of W3 )
assume A1: ( W1 is Submodule of W3 & W2 is Submodule of W3 ) ; ::_thesis: W1 + W2 is Submodule of W3
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_W1_+_W2_holds_
v_in_W3
let v be Vector of V; ::_thesis: ( v in W1 + W2 implies v in W3 )
assume  v in W1 + W2 ; ::_thesis: v in W3
then consider v1, v2 being Vector of V such that
A2: ( v1 in W1 & v2 in W2 ) and
A3: v = v1 + v2 by Th1;
 ( v1 in W3 & v2 in W3 ) by A1, A2, RMOD_2:8;
hence  v in W3 by A3, RMOD_2:20; ::_thesis: verum
end;
hence  W1 + W2 is Submodule of W3 by RMOD_2:28; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be RightMod of R; ::_thesis: 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 )
let W1, W2 be Submodule of V; ::_thesis: ( ( 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 )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
thus  ( for W being Submodule of V holds not the carrier of W = the carrier of W1 \/ the carrier of W2 or W1 is Submodule of W2 or W2 is Submodule of W1 ) ::_thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proof
given W being Submodule of V such that A1: the carrier of W = the carrier of W1 \/ the carrier of W2 ; ::_thesis: ( W1 is Submodule of W2 or W2 is Submodule of W1 )
set VW = the carrier of W;
assume that
A2: W1 is not Submodule of W2 and
A3: W2 is not Submodule of W1 ; ::_thesis: contradiction
 not the carrier of W2 c= the carrier of W1 by A3, RMOD_2:27;
then consider y being set  such that
A4: y in the carrier of W2 and
A5: not y in the carrier of W1 by TARSKI:def_3;
reconsider y = y as Element of the carrier of W2 by A4;
reconsider y = y as Vector of V by RMOD_2:10;
reconsider A1 = the carrier of W as Subset of V by RMOD_2:def_2;
A6: A1 is linearly-closed by RMOD_2:33;
 not the carrier of W1 c= the carrier of W2 by A2, RMOD_2:27;
then consider x being set  such that
A7: x in the carrier of W1 and
A8: not x in the carrier of W2 by TARSKI:def_3;
reconsider x = x as Element of the carrier of W1 by A7;
reconsider x = x as Vector of V by RMOD_2:10;
A9: now__::_thesis:_not_x_+_y_in_the_carrier_of_W2
reconsider A2 = the carrier of W2 as Subset of V by RMOD_2:def_2;
A10: A2 is linearly-closed by RMOD_2:33;
assume  x + y in the carrier of W2 ; ::_thesis: contradiction
then  (x + y) - y in the carrier of W2 by A10, RMOD_2:3;
then  x + (y - y) in the carrier of W2 by RLVECT_1:def_3;
then  x + (0. V) in the carrier of W2 by VECTSP_1:19;
hence  contradiction by A8, RLVECT_1:def_4; ::_thesis: verum
end;
A11: now__::_thesis:_not_x_+_y_in_the_carrier_of_W1
reconsider A2 = the carrier of W1 as Subset of V by RMOD_2:def_2;
A12: A2 is linearly-closed by RMOD_2:33;
assume  x + y in the carrier of W1 ; ::_thesis: contradiction
then  (y + x) - x in the carrier of W1 by A12, RMOD_2:3;
then  y + (x - x) in the carrier of W1 by RLVECT_1:def_3;
then  y + (0. V) in the carrier of W1 by VECTSP_1:19;
hence  contradiction by A5, RLVECT_1:def_4; ::_thesis: verum
end;
 ( x in the carrier of W & y in the carrier of W ) by A1, XBOOLE_0:def_3;
then  x + y in the carrier of W by A6, RMOD_2:def_1;
hence  contradiction by A1, A11, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
A13: now__::_thesis:_(_W1_is_Submodule_of_W2_&_(_W1_is_Submodule_of_W2_or_W2_is_Submodule_of_W1_)_implies_ex_W_being_Submodule_of_V_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_)
assume  W1 is Submodule of W2 ; ::_thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then  the carrier of W1 c= the carrier of W2 by RMOD_2:def_2;
then  the carrier of W1 \/ the carrier of W2 = the carrier of W2 by XBOOLE_1:12;
hence  ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum
end;
A14: now__::_thesis:_(_W2_is_Submodule_of_W1_&_(_W1_is_Submodule_of_W2_or_W2_is_Submodule_of_W1_)_implies_ex_W_being_Submodule_of_V_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_)
assume  W2 is Submodule of W1 ; ::_thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then  the carrier of W2 c= the carrier of W1 by RMOD_2:def_2;
then  the carrier of W1 \/ the carrier of W2 = the carrier of W1 by XBOOLE_1:12;
hence  ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum
end;
assume  ( W1 is Submodule of W2 or W2 is Submodule of W1 ) ; ::_thesis: ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2
hence  ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 by A13, A14; ::_thesis: verum
end;

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 )
proof
defpred S1[ set , set ] means  ex W being strict Submodule of V st
( $2 = W & $1 = the carrier of W );
defpred S2[ set ] means  ex W being strict Submodule of V st $1 = the carrier of W;
consider B being set  such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of V & S2[x] ) ) from XBOOLE_0:sch_1();
A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by RMOD_2:29;
consider f being Function such that
A3: for x, y being set holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2);
 for x being set holds
( x in B iff ex y being set st [x,y] in f )
proof
let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f )
thus  ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B )
proof
assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f
then consider W being strict Submodule of V such that
A5: x = the carrier of W by A1;
take  W ; ::_thesis: [x,W] in f
thus  [x,W] in f by A3, A4, A5; ::_thesis: verum
end;
given y being set  such that A6: [x,y] in f ; ::_thesis: x in B
thus  x in B by A3, A6; ::_thesis: verum
end;
then A7: B = dom f by XTUPLE_0:def_12;
 for y being set holds
( y in rng f iff ex W being strict Submodule of V st y = W )
proof
let y be set ; ::_thesis: ( y in rng f iff ex W being strict Submodule of V st y = W )
thus  ( y in rng f implies ex W being strict Submodule of V st y = W ) ::_thesis: ( ex W being strict Submodule of V st y = W implies y in rng f )
proof
assume  y in rng f ; ::_thesis: ex W being strict Submodule of V st y = W
then consider x being set  such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
 [x,y] in f by A8, FUNCT_1:def_2;
then  ex W being strict Submodule of V st
( y = W & x = the carrier of W ) by A3;
hence  ex W being strict Submodule of V st y = W ; ::_thesis: verum
end;
given W being strict Submodule of V such that A9: y = W ; ::_thesis: y in rng f
reconsider W = y as Submodule of V by A9;
reconsider x = the carrier of W as set ;
 the carrier of W c= the carrier of V by RMOD_2:def_2;
then A10: x in dom f by A1, A7, A9;
then  [x,y] in f by A3, A7, A9;
then  y = f . x by A10, FUNCT_1:def_2;
hence  y in rng f by A10, FUNCT_1:def_3; ::_thesis: verum
end;
hence  ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Submodule of V st W = x ) ; ::_thesis: verum
end;
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
proof
defpred S1[ set ] means  ex W being strict Submodule of V st W = $1;
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  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 ; ::_thesis: verum
end;
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
proof
set W = the strict Submodule of V;
 the strict Submodule of V in Submodules V by Def3;
hence  not Submodules V is empty ; ::_thesis: verum
end;
end;

theorem :: RMOD_3:37
for R being Ring
for V being strict RightMod of R holds V in Submodules V
proof
let R be Ring; ::_thesis: for V being strict RightMod of R holds V in Submodules V
let V be strict RightMod of R; ::_thesis: V in Submodules V
 ex W9 being strict Submodule of V st the carrier of ((Omega). V) = the carrier of W9 ;
hence  V in Submodules V by Def3; ::_thesis: verum
end;

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 ) )
proof
let R be Ring; ::_thesis: 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 ) )
let V be RightMod of R; ::_thesis: 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 ) )
let W1, W2 be Submodule of V; ::_thesis: ( 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 ) )
thus  ( W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) implies for v being Vector of V ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) ::_thesis: ( ( for v being Vector of V ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) implies W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) )
proof
assume A1: W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) ; ::_thesis: for v being Vector of V ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
let v be Vector of V; ::_thesis: ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
 v in (Omega). V by RLVECT_1:1;
hence  ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) by A1, Th1; ::_thesis: verum
end;
assume A2: for v being Vector of V ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ; ::_thesis: W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #)
now__::_thesis:_(_W1_+_W2_is_Submodule_of_(Omega)._V_&_(_for_u_being_Vector_of_V_holds_u_in_W1_+_W2_)_)
thus  W1 + W2 is Submodule of (Omega). V by Lm5; ::_thesis: for u being Vector of V holds u in W1 + W2
let u be Vector of V; ::_thesis: u in W1 + W2
 ex v1, v2 being Vector of V st
( v1 in W1 & v2 in W2 & u = v1 + v2 ) by A2;
hence  u in W1 + W2 by Th1; ::_thesis: verum
end;
hence  W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) by RMOD_2:32; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: for V being RightMod of R
for v, v1, v2 being Vector of V holds
( v = v1 + v2 iff v1 = v - v2 )
let V be RightMod of R; ::_thesis: for v, v1, v2 being Vector of V holds
( v = v1 + v2 iff v1 = v - v2 )
let v, v1, v2 be Vector of V; ::_thesis: ( v = v1 + v2 iff v1 = v - v2 )
thus  ( v = v1 + v2 implies v1 = v - v2 ) ::_thesis: ( v1 = v - v2 implies v = v1 + v2 )
proof
assume A1: v = v1 + v2 ; ::_thesis: v1 = v - v2
thus v1 = (0. V) + v1 by RLVECT_1:def_4
.= (v + (- (v2 + v1))) + v1 by A1, VECTSP_1:19
.= (v + ((- v2) + (- v1))) + v1 by RLVECT_1:31
.= ((v + (- v2)) + (- v1)) + v1 by RLVECT_1:def_3
.= (v + (- v2)) + ((- v1) + v1) by RLVECT_1:def_3
.= (v + (- v2)) + (0. V) by RLVECT_1:5
.= v - v2 by RLVECT_1:def_4 ; ::_thesis: verum
end;
assume A2: v1 = v - v2 ; ::_thesis: v = v1 + v2
thus v = v + (0. V) by RLVECT_1:def_4
.= v + (v1 + (- v1)) by RLVECT_1:5
.= (v + v1) + (- (v - v2)) by A2, RLVECT_1:def_3
.= (v + v1) + ((- v) + v2) by RLVECT_1:33
.= ((v + v1) + (- v)) + v2 by RLVECT_1:def_3
.= ((v + (- v)) + v1) + v2 by RLVECT_1:def_3
.= ((0. V) + v1) + v2 by RLVECT_1:5
.= v1 + v2 by RLVECT_1:def_4 ; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2 be Submodule of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1 )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: V is_the_direct_sum_of W2,W1
then  W1 /\ W2 = (0). V by Def4;
then A2: W2 /\ W1 = (0). V by Th14;
 RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 by A1, Def4;
then  RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W2 + W1 by Lm1;
hence  V is_the_direct_sum_of W2,W1 by A2, Def4; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be strict RightMod of R; ::_thesis: ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
 ( ((0). V) + ((Omega). V) = V & (0). V = ((0). V) /\ ((Omega). V) ) by Th9, Th21;
hence  V is_the_direct_sum_of (0). V, (Omega). V by Def4; ::_thesis: V is_the_direct_sum_of (Omega). V, (0). V
hence  V is_the_direct_sum_of (Omega). V, (0). V by Th38; ::_thesis: verum
end;


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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2 be Submodule of V; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C2 be Coset of W2; ::_thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 )
set v = the Element of C1 /\ C2;
set C = C1 /\ C2;
assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: C1 /\ C2 is Coset of W1 /\ W2
then reconsider v = the Element of C1 /\ C2 as Element of V by TARSKI:def_3;
 v in C2 by A1, XBOOLE_0:def_4;
then A2: C2 = v + W2 by RMOD_2:74;
 v in C1 by A1, XBOOLE_0:def_4;
then A3: C1 = v + W1 by RMOD_2:74;
 C1 /\ C2 is Coset of W1 /\ W2
proof
take  v ; :: according to RMOD_2:def_6 ::_thesis: C1 /\ C2 = v + (W1 /\ W2)
thus  C1 /\ C2 c= v + (W1 /\ W2) :: according to XBOOLE_0:def_10 ::_thesis: v + (W1 /\ W2) c= C1 /\ C2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) )
assume A4: x in C1 /\ C2 ; ::_thesis: x in v + (W1 /\ W2)
then  x in C1 by XBOOLE_0:def_4;
then consider u1 being Vector of V such that
A5: u1 in W1 and
A6: x = v + u1 by A3, RMOD_2:42;
 x in C2 by A4, XBOOLE_0:def_4;
then consider u2 being Vector of V such that
A7: u2 in W2 and
A8: x = v + u2 by A2, RMOD_2:42;
 u1 = u2 by A6, A8, RLVECT_1:8;
then  u1 in W1 /\ W2 by A5, A7, Th3;
hence  x in v + (W1 /\ W2) by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + (W1 /\ W2) or x in C1 /\ C2 )
assume  x in v + (W1 /\ W2) ; ::_thesis: x in C1 /\ C2
then consider u being Vector of V such that
A9: u in W1 /\ W2 and
A10: x = v + u by RMOD_2:42;
 u in W2 by A9, Th3;
then A11: x in C2 by A2, A10;
 u in W1 by A9, Th3;
then  x in C1 by A3, A10;
hence  x in C1 /\ C2 by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  C1 /\ C2 is Coset of W1 /\ W2 ; ::_thesis: verum
end;

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} )
proof
let R be Ring; ::_thesis: 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} )
let V be RightMod of R; ::_thesis: 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} )
let W1, W2 be Submodule of V; ::_thesis: ( 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} )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
A1: W1 + W2 is Submodule of (Omega). V by Lm5;
thus  ( V is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} ) ::_thesis: ( ( for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} ) implies V is_the_direct_sum_of W1,W2 )
proof
assume A2: V is_the_direct_sum_of W1,W2 ; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v}
then A3: RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 by Def4;
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v}
let C2 be Coset of W2; ::_thesis: ex v being Vector of V st C1 /\ C2 = {v}
consider v1 being Vector of V such that
A4: C1 = v1 + W1 by RMOD_2:def_6;
 v1 in (Omega). V by RLVECT_1:1;
then consider v11, v12 being Vector of V such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3, Th1;
consider v2 being Vector of V such that
A8: C2 = v2 + W2 by RMOD_2:def_6;
 v2 in (Omega). V by RLVECT_1:1;
then consider v21, v22 being Vector of V such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A3, Th1;
take v = v12 + v21; ::_thesis: C1 /\ C2 = {v}
 {v} = C1 /\ C2
proof
thus A12: {v} c= C1 /\ C2 :: according to XBOOLE_0:def_10 ::_thesis: C1 /\ C2 c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in C1 /\ C2 )
assume  x in {v} ; ::_thesis: x in C1 /\ C2
then A13: x = v by TARSKI:def_1;
 v21 = v2 - v22 by A11, Lm15;
then  v21 in C2 by A8, A10, RMOD_2:59;
then  C2 = v21 + W2 by RMOD_2:74;
then A14: x in C2 by A6, A13;
 v12 = v1 - v11 by A7, Lm15;
then  v12 in C1 by A4, A5, RMOD_2:59;
then  C1 = v12 + W1 by RMOD_2:74;
then  x in C1 by A9, A13;
hence  x in C1 /\ C2 by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in {v} )
assume A15: x in C1 /\ C2 ; ::_thesis: x in {v}
then  C1 meets C2 by XBOOLE_0:4;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th40;
A16: v in {v} by TARSKI:def_1;
 W1 /\ W2 = (0). V by A2, Def4;
then  ex u being Vector of V st C = {u} by RMOD_2:69;
hence  x in {v} by A12, A15, A16, TARSKI:def_1; ::_thesis: verum
end;
hence  C1 /\ C2 = {v} ; ::_thesis: verum
end;
assume A17: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v} ; ::_thesis: V is_the_direct_sum_of W1,W2
A18: the carrier of W2 is Coset of W2 by RMOD_2:70;
A19: the carrier of V c= the carrier of (W1 + W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of V or x in the carrier of (W1 + W2) )
assume  x in the carrier of V ; ::_thesis: x in the carrier of (W1 + W2)
then reconsider u = x as Vector of V ;
consider C1 being Coset of W1 such that
A20: u in C1 by RMOD_2:65;
consider v being Vector of V such that
A21: C1 /\ the carrier of W2 = {v} by A18, A17;
A22: v in {v} by TARSKI:def_1;
then  v in C1 by A21, XBOOLE_0:def_4;
then consider v1 being Vector of V such that
A23: v1 in W1 and
A24: u - v1 = v by A20, RMOD_2:76;
 v in the carrier of W2 by A21, A22, XBOOLE_0:def_4;
then A25: v in W2 by STRUCT_0:def_5;
 u = v1 + v by A24, Lm15;
then  x in W1 + W2 by A25, A23, Th1;
hence  x in the carrier of (W1 + W2) by STRUCT_0:def_5; ::_thesis: verum
end;
 the carrier of W1 is Coset of W1 by RMOD_2:70;
then consider v being Vector of V such that
A26: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;
 the carrier of (W1 + W2) c= the carrier of V by RMOD_2:def_2;
then  the carrier of V = the carrier of (W1 + W2) by A19, XBOOLE_0:def_10;
hence  RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) = W1 + W2 by A1, RMOD_2:31; :: according to RMOD_3:def_4 ::_thesis: W1 /\ W2 = (0). V
 0. V in W2 by RMOD_2:17;
then A27: 0. V in the carrier of W2 by STRUCT_0:def_5;
 0. V in W1 by RMOD_2:17;
then  0. V in the carrier of W1 by STRUCT_0:def_5;
then A28: 0. V in {v} by A26, A27, XBOOLE_0:def_4;
the carrier of ((0). V) = {(0. V)} by RMOD_2:def_3
.= the carrier of W1 /\ the carrier of W2 by A26, A28, TARSKI:def_1
.= the carrier of (W1 /\ W2) by Def2 ;
hence  W1 /\ W2 = (0). V by RMOD_2:29; ::_thesis: verum
end;

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 )
proof
let R be Ring; ::_thesis: 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 )
let V be RightMod of R; ::_thesis: 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 )
let W1, W2 be Submodule of V; ::_thesis: 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 )
let v, v1, v2, u1, u2 be Vector of V; ::_thesis: ( 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 implies ( v1 = u1 & v2 = u2 ) )
reconsider C2 = v1 + W2 as Coset of W2 by RMOD_2:def_6;
reconsider C1 = the carrier of W1 as Coset of W1 by RMOD_2:70;
A1: v1 in C2 by RMOD_2:44;
assume  V is_the_direct_sum_of W1,W2 ; ::_thesis: ( not v = v1 + v2 or not v = u1 + u2 or not v1 in W1 or not u1 in W1 or not v2 in W2 or not u2 in W2 or ( v1 = u1 & v2 = u2 ) )
then consider u being Vector of V such that
A2: C1 /\ C2 = {u} by Th41;
assume that
A3: ( v = v1 + v2 & v = u1 + u2 ) and
A4: v1 in W1 and
A5: u1 in W1 and
A6: ( v2 in W2 & u2 in W2 ) ; ::_thesis: ( v1 = u1 & v2 = u2 )
A7: v2 - u2 in W2 by A6, RMOD_2:23;
 v1 in C1 by A4, STRUCT_0:def_5;
then  v1 in C1 /\ C2 by A1, XBOOLE_0:def_4;
then A8: v1 = u by A2, TARSKI:def_1;
u1 = (v1 + v2) - u2 by A3, Lm15
.= v1 + (v2 - u2) by RLVECT_1:def_3 ;
then A9: u1 in C2 by A7;
 u1 in C1 by A5, STRUCT_0:def_5;
then A10: u1 in C1 /\ C2 by A9, XBOOLE_0:def_4;
hence  v1 = u1 by A2, A8, TARSKI:def_1; ::_thesis: v2 = u2
 u1 = u by A10, A2, TARSKI:def_1;
hence  v2 = u2 by A3, A8, RLVECT_1:8; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2 be Submodule of V; ::_thesis: ( 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 ) implies V is_the_direct_sum_of W1,W2 )
assume A1: V = W1 + W2 ; ::_thesis: ( for v being Vector of V ex 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 & not ( v1 = u1 & v2 = u2 ) ) or V is_the_direct_sum_of W1,W2 )
 ( the carrier of ((0). V) = {(0. V)} & (0). V is Submodule of W1 /\ W2 ) by RMOD_2:39, RMOD_2:def_3;
then A2: {(0. V)} c= the carrier of (W1 /\ W2) by RMOD_2:def_2;
given v being Vector of V such that A3: 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 ) ; ::_thesis: V is_the_direct_sum_of W1,W2
assume  not V is_the_direct_sum_of W1,W2 ; ::_thesis: contradiction
then  W1 /\ W2 <> (0). V by A1, Def4;
then  the carrier of (W1 /\ W2) <> {(0. V)} by RMOD_2:def_3;
then  {(0. V)} c< the carrier of (W1 /\ W2) by A2, XBOOLE_0:def_8;
then consider x being set  such that
A4: x in the carrier of (W1 /\ W2) and
A5: not x in {(0. V)} by XBOOLE_0:6;
A6: x in W1 /\ W2 by A4, STRUCT_0:def_5;
then  x in V by RMOD_2:9;
then reconsider u = x as Vector of V by STRUCT_0:def_5;
consider v1, v2 being Vector of V such that
A7: v1 in W1 and
A8: v2 in W2 and
A9: v = v1 + v2 by A1, Lm14;
A10: v = (v1 + v2) + (0. V) by A9, RLVECT_1:def_4
.= (v1 + v2) + (u - u) by VECTSP_1:19
.= ((v1 + v2) + u) - u by RLVECT_1:def_3
.= ((v1 + u) + v2) - u by RLVECT_1:def_3
.= (v1 + u) + (v2 - u) by RLVECT_1:def_3 ;
 x in W2 by A6, Th3;
then A11: v2 - u in W2 by A8, RMOD_2:23;
 x in W1 by A6, Th3;
then  v1 + u in W1 by A7, RMOD_2:20;
then v2 + (- u) = v2 by A3, A7, A8, A9, A10, A11
.= v2 + (0. V) by RLVECT_1:def_4 ;
then  - u = 0. V by RLVECT_1:8;
then A12: u = - (0. V) by RLVECT_1:17;
 x <> 0. V by A5, TARSKI:def_1;
hence  contradiction by A12, RLVECT_1:12; ::_thesis: verum
end;

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 )
proof
 W1 + W2 = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) by A1, Def4;
then consider v1, v2 being Vector of V such that
A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm14;
take  [v1,v2] ; ::_thesis: ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 )
 [v1,v2] `1 = v1 by MCART_1:7;
hence  ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 ) by A2, MCART_1:7; ::_thesis: verum
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
let t1, t2 be Element of [: the carrier of V, the carrier of V:]; ::_thesis: ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 implies t1 = t2 )
assume  ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 ) ; ::_thesis: t1 = t2
then A3: ( t1 `1 = t2 `1 & t1 `2 = t2 `2 ) by A1, Th43;
 t1 = [(t1 `1),(t1 `2)] by MCART_1:21;
hence  t1 = t2 by A3, MCART_1:21; ::_thesis: verum
end;
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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2 be Submodule of V; ::_thesis: for v being Vector of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let v be Vector of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
then A2: (v |-- (W1,W2)) `2 in W2 by Def5;
A3: V is_the_direct_sum_of W2,W1 by A1, Th38;
then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def5;
A5: (v |-- (W2,W1)) `2 in W1 by A3, Def5;
 ( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def5;
hence  (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by A1, A2, A4, A5, Th43; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: 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
let V be RightMod of R; ::_thesis: 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
let W1, W2 be Submodule of V; ::_thesis: for v being Vector of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let v be Vector of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
then A2: (v |-- (W1,W2)) `2 in W2 by Def5;
A3: V is_the_direct_sum_of W2,W1 by A1, Th38;
then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def5;
A5: (v |-- (W2,W1)) `2 in W1 by A3, Def5;
 ( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def5;
hence  (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by A1, A2, A4, A5, Th43; ::_thesis: verum
end;


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
proof
defpred S1[ Element of Submodules V, Element of Submodules V, Element of Submodules V] means  for W1, W2 being Submodule of V st $1 = W1 & $2 = W2 holds
$3 = W1 + W2;
A1: for A1, A2 being Element of Submodules V ex B being Element of Submodules V st S1[A1,A2,B]
proof
let A1, A2 be Element of Submodules V; ::_thesis: ex B being Element of Submodules V st S1[A1,A2,B]
consider W1 being strict Submodule of V such that
A2: W1 = A1 by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = A2 by Def3;
reconsider C = W1 + W2 as Element of Submodules V by Def3;
take  C ; ::_thesis: S1[A1,A2,C]
thus  S1[A1,A2,C] by A2, A3; ::_thesis: verum
end;
 ex o being BinOp of (Submodules V) st
for a, b being Element of Submodules V holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
hence  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 ; ::_thesis: verum
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
let o1, o2 be BinOp of (Submodules V); ::_thesis: ( ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o1 . (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
o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 + W2 ; ::_thesis: ( ex A1, A2 being Element of Submodules V ex W1, W2 being Submodule of V st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 + W2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Submodules_V_&_y_in_Submodules_V_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Submodules V & y in Submodules V implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Submodules V and
A7: y in Submodules V ; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Submodules V by A6, A7;
consider W1 being strict Submodule of V such that
A8: W1 = x by A6, Def3;
consider W2 being strict Submodule of V such that
A9: W2 = y by A7, Def3;
 o1 . (A,B) = W1 + W2 by A4, A8, A9;
hence  o1 . (x,y) = o2 . (x,y) by A5, A8, A9; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
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
proof
defpred S1[ Element of Submodules V, Element of Submodules V, Element of Submodules V] means  for W1, W2 being Submodule of V st $1 = W1 & $2 = W2 holds
$3 = W1 /\ W2;
A1: for A1, A2 being Element of Submodules V ex B being Element of Submodules V st S1[A1,A2,B]
proof
let A1, A2 be Element of Submodules V; ::_thesis: ex B being Element of Submodules V st S1[A1,A2,B]
consider W1 being strict Submodule of V such that
A2: W1 = A1 by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = A2 by Def3;
reconsider C = W1 /\ W2 as Element of Submodules V by Def3;
take  C ; ::_thesis: S1[A1,A2,C]
thus  S1[A1,A2,C] by A2, A3; ::_thesis: verum
end;
 ex o being BinOp of (Submodules V) st
for a, b being Element of Submodules V holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
hence  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 ; ::_thesis: verum
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
let o1, o2 be BinOp of (Submodules V); ::_thesis: ( ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o1 . (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
o2 . (A1,A2) = W1 /\ W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ; ::_thesis: ( ex A1, A2 being Element of Submodules V ex W1, W2 being Submodule of V st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 /\ W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Submodules_V_&_y_in_Submodules_V_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Submodules V & y in Submodules V implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Submodules V and
A7: y in Submodules V ; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Submodules V by A6, A7;
consider W1 being strict Submodule of V such that
A8: W1 = x by A6, Def3;
consider W2 being strict Submodule of V such that
A9: W2 = y by A7, Def3;
 o1 . (A,B) = W1 /\ W2 by A4, A8, A9;
hence  o1 . (x,y) = o2 . (x,y) by A5, A8, A9; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
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
proof
let R be Ring; ::_thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
let V be RightMod of R; ::_thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
A1: for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "/\" B = B "/\" A
proof
let A, B be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" B = B "/\" A
consider W1 being strict Submodule of V such that
A2: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = B by Def3;
thus A "/\" B = (SubMeet V) . (A,B) by LATTICES:def_2
.= W1 /\ W2 by A2, A3, Def7
.= W2 /\ W1 by Th14
.= (SubMeet V) . (B,A) by A2, A3, Def7
.= B "/\" A by LATTICES:def_2 ; ::_thesis: verum
end;
A4: for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B
proof
let A, B be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: (A "/\" B) "\/" B = B
consider W1 being strict Submodule of V such that
A5: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A6: W2 = B by Def3;
reconsider AB = W1 /\ W2 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
thus (A "/\" B) "\/" B = (SubJoin V) . ((A "/\" B),B) by LATTICES:def_1
.= (SubJoin V) . (((SubMeet V) . (A,B)),B) by LATTICES:def_2
.= (SubJoin V) . (AB,B) by A5, A6, Def7
.= (W1 /\ W2) + W2 by A6, Def6
.= B by A6, Lm8, RMOD_2:29 ; ::_thesis: verum
end;
A7: for A, B, C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C
consider W1 being strict Submodule of V such that
A8: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A9: W2 = B by Def3;
consider W3 being strict Submodule of V such that
A10: W3 = C by Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "/\" (B "/\" C) = (SubMeet V) . (A,(B "/\" C)) by LATTICES:def_2
.= (SubMeet V) . (A,((SubMeet V) . (B,C))) by LATTICES:def_2
.= (SubMeet V) . (A,BC) by A9, A10, Def7
.= W1 /\ (W2 /\ W3) by A8, Def7
.= (W1 /\ W2) /\ W3 by Th15
.= (SubMeet V) . (AB,C) by A10, Def7
.= (SubMeet V) . (((SubMeet V) . (A,B)),C) by A8, A9, Def7
.= (SubMeet V) . ((A "/\" B),C) by LATTICES:def_2
.= (A "/\" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
A11: for A, B, C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A, B, C be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C
consider W1 being strict Submodule of V such that
A12: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A13: W2 = B by Def3;
consider W3 being strict Submodule of V such that
A14: W3 = C by Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "\/" (B "\/" C) = (SubJoin V) . (A,(B "\/" C)) by LATTICES:def_1
.= (SubJoin V) . (A,((SubJoin V) . (B,C))) by LATTICES:def_1
.= (SubJoin V) . (A,BC) by A13, A14, Def6
.= W1 + (W2 + W3) by A12, Def6
.= (W1 + W2) + W3 by Th6
.= (SubJoin V) . (AB,C) by A14, Def6
.= (SubJoin V) . (((SubJoin V) . (A,B)),C) by A12, A13, Def6
.= (SubJoin V) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "\/" C by LATTICES:def_1 ; ::_thesis: verum
end;
A15: for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A
proof
let A, B be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" (A "\/" B) = A
consider W1 being strict Submodule of V such that
A16: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A17: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "/\" (A "\/" B) = (SubMeet V) . (A,(A "\/" B)) by LATTICES:def_2
.= (SubMeet V) . (A,((SubJoin V) . (A,B))) by LATTICES:def_1
.= (SubMeet V) . (A,AB) by A16, A17, Def6
.= W1 /\ (W1 + W2) by A16, Def7
.= A by A16, Lm9, RMOD_2:29 ; ::_thesis: verum
end;
 for A, B being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A
proof
let A, B be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: A "\/" B = B "\/" A
consider W1 being strict Submodule of V such that
A18: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A19: W2 = B by Def3;
thus A "\/" B = (SubJoin V) . (A,B) by LATTICES:def_1
.= W1 + W2 by A18, A19, Def6
.= W2 + W1 by Lm1
.= (SubJoin V) . (B,A) by A18, A19, Def6
.= B "\/" A by LATTICES:def_1 ; ::_thesis: verum
end;
then  ( LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is join-commutative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is join-associative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is meet-absorbing & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is meet-commutative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is meet-associative & LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is join-absorbing ) by A11, A4, A1, A7, A15, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice ; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
let V be RightMod of R; ::_thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
 ex C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "/\" A = C & A "/\" C = C )
proof
reconsider C = (0). V as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
take  C ; ::_thesis: for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "/\" A = C & A "/\" C = C )
let A be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: ( C "/\" A = C & A "/\" C = C )
consider W being strict Submodule of V such that
A1: W = A by Def3;
thus C "/\" A = (SubMeet V) . (C,A) by LATTICES:def_2
.= ((0). V) /\ W by A1, Def7
.= C by Th21 ; ::_thesis: A "/\" C = C
thus A "/\" C = (SubMeet V) . (A,C) by LATTICES:def_2
.= W /\ ((0). V) by A1, Def7
.= C by Th21 ; ::_thesis: verum
end;
hence  LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice by Th47, LATTICES:def_13; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
let V be RightMod of R; ::_thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
 ex C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
proof
consider W9 being strict Submodule of V such that
A1: the carrier of W9 = the carrier of ((Omega). V) ;
reconsider C = W9 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
take  C ; ::_thesis: for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
let A be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: ( C "\/" A = C & A "\/" C = C )
consider W being strict Submodule of V such that
A2: W = A by Def3;
A3: C is Submodule of (Omega). V by Lm5;
thus C "\/" A = (SubJoin V) . (C,A) by LATTICES:def_1
.= W9 + W by A2, Def6
.= ((Omega). V) + W by A1, Lm4
.= RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) by Th11
.= C by A1, A3, RMOD_2:31 ; ::_thesis: A "\/" C = C
thus A "\/" C = (SubJoin V) . (A,C) by LATTICES:def_1
.= W + W9 by A2, Def6
.= W + ((Omega). V) by A1, Lm4
.= RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) by Th11
.= C by A1, A3, RMOD_2:31 ; ::_thesis: verum
end;
hence  LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice by Th47, LATTICES:def_14; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice
let V be RightMod of R; ::_thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice
 LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded upper-bounded Lattice by Th48, Th49;
hence  LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; ::_thesis: verum
end;

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
proof
let R be Ring; ::_thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice
let V be RightMod of R; ::_thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
 for A, B, C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); ::_thesis: ( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
assume A1: A [= C ; ::_thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C
consider W1 being strict Submodule of V such that
A2: W1 = A by Def3;
consider W3 being strict Submodule of V such that
A3: W3 = C by Def3;
W1 + W3 = (SubJoin V) . (A,C) by A2, A3, Def6
.= A "\/" C by LATTICES:def_1
.= W3 by A1, A3, LATTICES:def_3 ;
then A4: W1 is Submodule of W3 by Th8;
consider W2 being strict Submodule of V such that
A5: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
reconsider BC = W2 /\ W3 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "\/" (B "/\" C) = (SubJoin V) . (A,(B "/\" C)) by LATTICES:def_1
.= (SubJoin V) . (A,((SubMeet V) . (B,C))) by LATTICES:def_2
.= (SubJoin V) . (A,BC) by A5, A3, Def7
.= W1 + (W2 /\ W3) by A2, Def6
.= (W1 + W2) /\ W3 by A4, Th31
.= (SubMeet V) . (AB,C) by A3, Def7
.= (SubMeet V) . (((SubJoin V) . (A,B)),C) by A2, A5, Def6
.= (SubMeet V) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
hence  LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is M_Lattice by Th47, LATTICES:def_12; ::_thesis: verum
end;