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