:: RMOD_2 semantic presentation begin definition let R be Ring; let V be RightMod of R; let V1 be Subset of V; attrV1 is linearly-closed means :Def1: :: RMOD_2:def 1 ( ( for v, u being Vector of V st v in V1 & u in V1 holds v + u in V1 ) & ( for a being Scalar of R for v being Vector of V st v in V1 holds v * a in V1 ) ); end; :: deftheorem Def1 defines linearly-closed RMOD_2:def_1_:_ for R being Ring for V being RightMod of R for V1 being Subset of V holds ( V1 is linearly-closed iff ( ( for v, u being Vector of V st v in V1 & u in V1 holds v + u in V1 ) & ( for a being Scalar of R for v being Vector of V st v in V1 holds v * a in V1 ) ) ); theorem Th1: :: RMOD_2:1 for R being Ring for V being RightMod of R for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds 0. V in V1 proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds 0. V in V1 let V be RightMod of R; ::_thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds 0. V in V1 let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies 0. V in V1 ) assume that A1: V1 <> {} and A2: V1 is linearly-closed ; ::_thesis: 0. V in V1 set x = the Element of V1; reconsider x = the Element of V1 as Element of V by A1, TARSKI:def_3; x * (0. R) in V1 by A1, A2, Def1; hence 0. V in V1 by VECTSP_2:32; ::_thesis: verum end; theorem Th2: :: RMOD_2:2 for R being Ring for V being RightMod of R for V1 being Subset of V st V1 is linearly-closed holds for v being Vector of V st v in V1 holds - v in V1 proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st V1 is linearly-closed holds for v being Vector of V st v in V1 holds - v in V1 let V be RightMod of R; ::_thesis: for V1 being Subset of V st V1 is linearly-closed holds for v being Vector of V st v in V1 holds - v in V1 let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed implies for v being Vector of V st v in V1 holds - v in V1 ) assume A1: V1 is linearly-closed ; ::_thesis: for v being Vector of V st v in V1 holds - v in V1 let v be Vector of V; ::_thesis: ( v in V1 implies - v in V1 ) assume v in V1 ; ::_thesis: - v in V1 then v * (- (1_ R)) in V1 by A1, Def1; hence - v in V1 by VECTSP_2:32; ::_thesis: verum end; theorem :: RMOD_2:3 for R being Ring for V being RightMod of R for V1 being Subset of V st V1 is linearly-closed holds for v, u being Vector of V st v in V1 & u in V1 holds v - u in V1 proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st V1 is linearly-closed holds for v, u being Vector of V st v in V1 & u in V1 holds v - u in V1 let V be RightMod of R; ::_thesis: for V1 being Subset of V st V1 is linearly-closed holds for v, u being Vector of V st v in V1 & u in V1 holds v - u in V1 let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed implies for v, u being Vector of V st v in V1 & u in V1 holds v - u in V1 ) assume A1: V1 is linearly-closed ; ::_thesis: for v, u being Vector of V st v in V1 & u in V1 holds v - u in V1 let v, u be Vector of V; ::_thesis: ( v in V1 & u in V1 implies v - u in V1 ) assume that A2: v in V1 and A3: u in V1 ; ::_thesis: v - u in V1 - u in V1 by A1, A3, Th2; hence v - u in V1 by A1, A2, Def1; ::_thesis: verum end; theorem Th4: :: RMOD_2:4 for R being Ring for V being RightMod of R holds {(0. V)} is linearly-closed proof let R be Ring; ::_thesis: for V being RightMod of R holds {(0. V)} is linearly-closed let V be RightMod of R; ::_thesis: {(0. V)} is linearly-closed thus for v, u being Vector of V st v in {(0. V)} & u in {(0. V)} holds v + u in {(0. V)} :: according to RMOD_2:def_1 ::_thesis: for a being Scalar of R for v being Vector of V st v in {(0. V)} holds v * a in {(0. V)} proof let v, u be Vector of V; ::_thesis: ( v in {(0. V)} & u in {(0. V)} implies v + u in {(0. V)} ) assume ( v in {(0. V)} & u in {(0. V)} ) ; ::_thesis: v + u in {(0. V)} then ( v = 0. V & u = 0. V ) by TARSKI:def_1; then v + u = 0. V by RLVECT_1:def_4; hence v + u in {(0. V)} by TARSKI:def_1; ::_thesis: verum end; let a be Scalar of R; ::_thesis: for v being Vector of V st v in {(0. V)} holds v * a in {(0. V)} let v be Vector of V; ::_thesis: ( v in {(0. V)} implies v * a in {(0. V)} ) assume A1: v in {(0. V)} ; ::_thesis: v * a in {(0. V)} then v = 0. V by TARSKI:def_1; hence v * a in {(0. V)} by A1, VECTSP_2:32; ::_thesis: verum end; theorem :: RMOD_2:5 for R being Ring for V being RightMod of R for V1 being Subset of V st the carrier of V = V1 holds V1 is linearly-closed proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st the carrier of V = V1 holds V1 is linearly-closed let V be RightMod of R; ::_thesis: for V1 being Subset of V st the carrier of V = V1 holds V1 is linearly-closed let V1 be Subset of V; ::_thesis: ( the carrier of V = V1 implies V1 is linearly-closed ) assume A1: the carrier of V = V1 ; ::_thesis: V1 is linearly-closed hence for v, u being Vector of V st v in V1 & u in V1 holds v + u in V1 ; :: according to RMOD_2:def_1 ::_thesis: for a being Scalar of R for v being Vector of V st v in V1 holds v * a in V1 let a be Scalar of R; ::_thesis: for v being Vector of V st v in V1 holds v * a in V1 let v be Vector of V; ::_thesis: ( v in V1 implies v * a in V1 ) assume v in V1 ; ::_thesis: v * a in V1 thus v * a in V1 by A1; ::_thesis: verum end; theorem :: RMOD_2:6 for R being Ring for V being RightMod of R for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } holds V3 is linearly-closed proof let R be Ring; ::_thesis: for V being RightMod of R for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } holds V3 is linearly-closed let V be RightMod of R; ::_thesis: for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } holds V3 is linearly-closed let V1, V2, V3 be Subset of V; ::_thesis: ( V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } implies V3 is linearly-closed ) assume that A1: ( V1 is linearly-closed & V2 is linearly-closed ) and A2: V3 = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } ; ::_thesis: V3 is linearly-closed thus for v, u being Vector of V st v in V3 & u in V3 holds v + u in V3 :: according to RMOD_2:def_1 ::_thesis: for a being Scalar of R for v being Vector of V st v in V3 holds v * a in V3 proof let v, u be Vector of V; ::_thesis: ( v in V3 & u in V3 implies v + u in V3 ) assume that A3: v in V3 and A4: u in V3 ; ::_thesis: v + u in V3 consider v1, v2 being Vector of V such that A5: v = v1 + v2 and A6: ( v1 in V1 & v2 in V2 ) by A2, A3; consider u1, u2 being Vector of V such that A7: u = u1 + u2 and A8: ( u1 in V1 & u2 in V2 ) by A2, A4; A9: v + u = ((v1 + v2) + u1) + u2 by A5, A7, RLVECT_1:def_3 .= ((v1 + u1) + v2) + u2 by RLVECT_1:def_3 .= (v1 + u1) + (v2 + u2) by RLVECT_1:def_3 ; ( v1 + u1 in V1 & v2 + u2 in V2 ) by A1, A6, A8, Def1; hence v + u in V3 by A2, A9; ::_thesis: verum end; let a be Scalar of R; ::_thesis: for v being Vector of V st v in V3 holds v * a in V3 let v be Vector of V; ::_thesis: ( v in V3 implies v * a in V3 ) assume v in V3 ; ::_thesis: v * a in V3 then consider v1, v2 being Vector of V such that A10: v = v1 + v2 and A11: ( v1 in V1 & v2 in V2 ) by A2; A12: v * a = (v1 * a) + (v2 * a) by A10, VECTSP_2:def_9; ( v1 * a in V1 & v2 * a in V2 ) by A1, A11, Def1; hence v * a in V3 by A2, A12; ::_thesis: verum end; theorem :: RMOD_2:7 for R being Ring for V being RightMod of R for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds V1 /\ V2 is linearly-closed proof let R be Ring; ::_thesis: for V being RightMod of R for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds V1 /\ V2 is linearly-closed let V be RightMod of R; ::_thesis: for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds V1 /\ V2 is linearly-closed let V1, V2 be Subset of V; ::_thesis: ( V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is linearly-closed ) assume that A1: V1 is linearly-closed and A2: V2 is linearly-closed ; ::_thesis: V1 /\ V2 is linearly-closed thus for v, u being Vector of V st v in V1 /\ V2 & u in V1 /\ V2 holds v + u in V1 /\ V2 :: according to RMOD_2:def_1 ::_thesis: for a being Scalar of R for v being Vector of V st v in V1 /\ V2 holds v * a in V1 /\ V2 proof let v, u be Vector of V; ::_thesis: ( v in V1 /\ V2 & u in V1 /\ V2 implies v + u in V1 /\ V2 ) assume A3: ( v in V1 /\ V2 & u in V1 /\ V2 ) ; ::_thesis: v + u in V1 /\ V2 then ( v in V2 & u in V2 ) by XBOOLE_0:def_4; then A4: v + u in V2 by A2, Def1; ( v in V1 & u in V1 ) by A3, XBOOLE_0:def_4; then v + u in V1 by A1, Def1; hence v + u in V1 /\ V2 by A4, XBOOLE_0:def_4; ::_thesis: verum end; let a be Scalar of R; ::_thesis: for v being Vector of V st v in V1 /\ V2 holds v * a in V1 /\ V2 let v be Vector of V; ::_thesis: ( v in V1 /\ V2 implies v * a in V1 /\ V2 ) assume A5: v in V1 /\ V2 ; ::_thesis: v * a in V1 /\ V2 then v in V2 by XBOOLE_0:def_4; then A6: v * a in V2 by A2, Def1; v in V1 by A5, XBOOLE_0:def_4; then v * a in V1 by A1, Def1; hence v * a in V1 /\ V2 by A6, XBOOLE_0:def_4; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; mode Submodule of V -> RightMod of R means :Def2: :: RMOD_2:def 2 ( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V | [: the carrier of it, the carrier of it:] & the rmult of it = the rmult of V | [: the carrier of it, the carrier of R:] ); existence ex b1 being RightMod of R st ( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V | [: the carrier of b1, the carrier of b1:] & the rmult of b1 = the rmult of V | [: the carrier of b1, the carrier of R:] ) proof take V ; ::_thesis: ( the carrier of V c= the carrier of V & 0. V = 0. V & the addF of V = the addF of V | [: the carrier of V, the carrier of V:] & the rmult of V = the rmult of V | [: the carrier of V, the carrier of R:] ) thus ( the carrier of V c= the carrier of V & 0. V = 0. V ) ; ::_thesis: ( the addF of V = the addF of V | [: the carrier of V, the carrier of V:] & the rmult of V = the rmult of V | [: the carrier of V, the carrier of R:] ) thus ( the addF of V = the addF of V | [: the carrier of V, the carrier of V:] & the rmult of V = the rmult of V | [: the carrier of V, the carrier of R:] ) by RELSET_1:19; ::_thesis: verum end; end; :: deftheorem Def2 defines Submodule RMOD_2:def_2_:_ for R being Ring for V, b3 being RightMod of R holds ( b3 is Submodule of V iff ( the carrier of b3 c= the carrier of V & 0. b3 = 0. V & the addF of b3 = the addF of V | [: the carrier of b3, the carrier of b3:] & the rmult of b3 = the rmult of V | [: the carrier of b3, the carrier of R:] ) ); theorem :: RMOD_2:8 for x being set for R being Ring for V being RightMod of R for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds x in W2 proof let x be set ; ::_thesis: for R being Ring for V being RightMod of R for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds x in W2 let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds x in W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds x in W2 let W1, W2 be Submodule of V; ::_thesis: ( x in W1 & W1 is Submodule of W2 implies x in W2 ) assume ( x in W1 & W1 is Submodule of W2 ) ; ::_thesis: x in W2 then ( x in the carrier of W1 & the carrier of W1 c= the carrier of W2 ) by Def2, STRUCT_0:def_5; hence x in W2 by STRUCT_0:def_5; ::_thesis: verum end; theorem Th9: :: RMOD_2:9 for x being set for R being Ring for V being RightMod of R for W being Submodule of V st x in W holds x in V proof let x be set ; ::_thesis: for R being Ring for V being RightMod of R for W being Submodule of V st x in W holds x in V let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V st x in W holds x in V let V be RightMod of R; ::_thesis: for W being Submodule of V st x in W holds x in V let W be Submodule of V; ::_thesis: ( x in W implies x in V ) assume x in W ; ::_thesis: x in V then A1: x in the carrier of W by STRUCT_0:def_5; the carrier of W c= the carrier of V by Def2; hence x in V by A1, STRUCT_0:def_5; ::_thesis: verum end; theorem Th10: :: RMOD_2:10 for R being Ring for V being RightMod of R for W being Submodule of V for w being Vector of W holds w is Vector of V proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V for w being Vector of W holds w is Vector of V let V be RightMod of R; ::_thesis: for W being Submodule of V for w being Vector of W holds w is Vector of V let W be Submodule of V; ::_thesis: for w being Vector of W holds w is Vector of V let w be Vector of W; ::_thesis: w is Vector of V w in V by Th9, RLVECT_1:1; hence w is Vector of V by STRUCT_0:def_5; ::_thesis: verum end; theorem :: RMOD_2:11 for R being Ring for V being RightMod of R for W being Submodule of V holds 0. W = 0. V by Def2; theorem :: RMOD_2:12 for R being Ring for V being RightMod of R for W1, W2 being Submodule of V holds 0. W1 = 0. W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V holds 0. W1 = 0. W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds 0. W1 = 0. W2 let W1, W2 be Submodule of V; ::_thesis: 0. W1 = 0. W2 thus 0. W1 = 0. V by Def2 .= 0. W2 by Def2 ; ::_thesis: verum end; theorem Th13: :: RMOD_2:13 for R being Ring for V being RightMod of R for v, u being Vector of V for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 + w2 = v + u proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 + w2 = v + u let V be RightMod of R; ::_thesis: for v, u being Vector of V for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 + w2 = v + u let v, u be Vector of V; ::_thesis: for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 + w2 = v + u let W be Submodule of V; ::_thesis: for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 + w2 = v + u let w1, w2 be Vector of W; ::_thesis: ( w1 = v & w2 = u implies w1 + w2 = v + u ) assume A1: ( v = w1 & u = w2 ) ; ::_thesis: w1 + w2 = v + u set IW = [: the carrier of W, the carrier of W:]; w1 + w2 = ( the addF of V | [: the carrier of W, the carrier of W:]) . [w1,w2] by Def2; hence w1 + w2 = v + u by A1, FUNCT_1:49; ::_thesis: verum end; theorem Th14: :: RMOD_2:14 for R being Ring for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds w * a = v * a proof let R be Ring; ::_thesis: for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds w * a = v * a let a be Scalar of R; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds w * a = v * a let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds w * a = v * a let v be Vector of V; ::_thesis: for W being Submodule of V for w being Vector of W st w = v holds w * a = v * a let W be Submodule of V; ::_thesis: for w being Vector of W st w = v holds w * a = v * a let w be Vector of W; ::_thesis: ( w = v implies w * a = v * a ) assume A1: w = v ; ::_thesis: w * a = v * a w * a = ( the rmult of V | [: the carrier of W, the carrier of R:]) . [w,a] by Def2; hence w * a = v * a by A1, FUNCT_1:49; ::_thesis: verum end; theorem Th15: :: RMOD_2:15 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds - v = - w proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds - v = - w let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V for w being Vector of W st w = v holds - v = - w let v be Vector of V; ::_thesis: for W being Submodule of V for w being Vector of W st w = v holds - v = - w let W be Submodule of V; ::_thesis: for w being Vector of W st w = v holds - v = - w let w be Vector of W; ::_thesis: ( w = v implies - v = - w ) A1: ( - v = v * (- (1_ R)) & - w = w * (- (1_ R)) ) by VECTSP_2:32; assume w = v ; ::_thesis: - v = - w hence - v = - w by A1, Th14; ::_thesis: verum end; theorem Th16: :: RMOD_2:16 for R being Ring for V being RightMod of R for v, u being Vector of V for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 - w2 = v - u proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 - w2 = v - u let V be RightMod of R; ::_thesis: for v, u being Vector of V for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 - w2 = v - u let v, u be Vector of V; ::_thesis: for W being Submodule of V for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 - w2 = v - u let W be Submodule of V; ::_thesis: for w1, w2 being Vector of W st w1 = v & w2 = u holds w1 - w2 = v - u let w1, w2 be Vector of W; ::_thesis: ( w1 = v & w2 = u implies w1 - w2 = v - u ) assume that A1: w1 = v and A2: w2 = u ; ::_thesis: w1 - w2 = v - u - w2 = - u by A2, Th15; hence w1 - w2 = v - u by A1, Th13; ::_thesis: verum end; Lm1: for R being Ring for V being RightMod of R for V1 being Subset of V for W being Submodule of V st the carrier of W = V1 holds V1 is linearly-closed proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V for W being Submodule of V st the carrier of W = V1 holds V1 is linearly-closed let V be RightMod of R; ::_thesis: for V1 being Subset of V for W being Submodule of V st the carrier of W = V1 holds V1 is linearly-closed let V1 be Subset of V; ::_thesis: for W being Submodule of V st the carrier of W = V1 holds V1 is linearly-closed let W be Submodule of V; ::_thesis: ( the carrier of W = V1 implies V1 is linearly-closed ) set VW = the carrier of W; reconsider WW = W as RightMod of R ; assume A1: the carrier of W = V1 ; ::_thesis: V1 is linearly-closed thus for v, u being Vector of V st v in V1 & u in V1 holds v + u in V1 :: according to RMOD_2:def_1 ::_thesis: for a being Scalar of R for v being Vector of V st v in V1 holds v * a in V1 proof let v, u be Vector of V; ::_thesis: ( v in V1 & u in V1 implies v + u in V1 ) assume ( v in V1 & u in V1 ) ; ::_thesis: v + u in V1 then reconsider vv = v, uu = u as Vector of WW by A1; reconsider vw = vv + uu as Element of the carrier of W ; vw in V1 by A1; hence v + u in V1 by Th13; ::_thesis: verum end; let a be Scalar of R; ::_thesis: for v being Vector of V st v in V1 holds v * a in V1 let v be Vector of V; ::_thesis: ( v in V1 implies v * a in V1 ) assume v in V1 ; ::_thesis: v * a in V1 then reconsider vv = v as Vector of WW by A1; reconsider vw = vv * a as Element of the carrier of W ; vw in V1 by A1; hence v * a in V1 by Th14; ::_thesis: verum end; theorem Th17: :: RMOD_2:17 for R being Ring for V being RightMod of R for W being Submodule of V holds 0. V in W proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V holds 0. V in W let V be RightMod of R; ::_thesis: for W being Submodule of V holds 0. V in W let W be Submodule of V; ::_thesis: 0. V in W 0. W in W by RLVECT_1:1; hence 0. V in W by Def2; ::_thesis: verum end; theorem :: RMOD_2:18 for R being Ring for V being RightMod of R for W1, W2 being Submodule of V holds 0. W1 in W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V holds 0. W1 in W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds 0. W1 in W2 let W1, W2 be Submodule of V; ::_thesis: 0. W1 in W2 0. W1 = 0. V by Def2; hence 0. W1 in W2 by Th17; ::_thesis: verum end; theorem :: RMOD_2:19 for R being Ring for V being RightMod of R for W being Submodule of V holds 0. W in V by Th9, RLVECT_1:1; theorem Th20: :: RMOD_2:20 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V st u in W & v in W holds u + v in W proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V st u in W & v in W holds u + v in W let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V st u in W & v in W holds u + v in W let u, v be Vector of V; ::_thesis: for W being Submodule of V st u in W & v in W holds u + v in W let W be Submodule of V; ::_thesis: ( u in W & v in W implies u + v in W ) reconsider VW = the carrier of W as Subset of V by Def2; assume ( u in W & v in W ) ; ::_thesis: u + v in W then A1: ( u in the carrier of W & v in the carrier of W ) by STRUCT_0:def_5; VW is linearly-closed by Lm1; then u + v in the carrier of W by A1, Def1; hence u + v in W by STRUCT_0:def_5; ::_thesis: verum end; theorem Th21: :: RMOD_2:21 for R being Ring for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds v * a in W proof let R be Ring; ::_thesis: for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds v * a in W let a be Scalar of R; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds v * a in W let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V st v in W holds v * a in W let v be Vector of V; ::_thesis: for W being Submodule of V st v in W holds v * a in W let W be Submodule of V; ::_thesis: ( v in W implies v * a in W ) reconsider VW = the carrier of W as Subset of V by Def2; assume v in W ; ::_thesis: v * a in W then A1: v in the carrier of W by STRUCT_0:def_5; VW is linearly-closed by Lm1; then v * a in the carrier of W by A1, Def1; hence v * a in W by STRUCT_0:def_5; ::_thesis: verum end; theorem Th22: :: RMOD_2:22 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds - v in W proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds - v in W let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V st v in W holds - v in W let v be Vector of V; ::_thesis: for W being Submodule of V st v in W holds - v in W let W be Submodule of V; ::_thesis: ( v in W implies - v in W ) assume v in W ; ::_thesis: - v in W then v * (- (1_ R)) in W by Th21; hence - v in W by VECTSP_2:32; ::_thesis: verum end; theorem Th23: :: RMOD_2:23 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V st u in W & v in W holds u - v in W proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V st u in W & v in W holds u - v in W let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V st u in W & v in W holds u - v in W let u, v be Vector of V; ::_thesis: for W being Submodule of V st u in W & v in W holds u - v in W let W be Submodule of V; ::_thesis: ( u in W & v in W implies u - v in W ) assume that A1: u in W and A2: v in W ; ::_thesis: u - v in W - v in W by A2, Th22; hence u - v in W by A1, Th20; ::_thesis: verum end; theorem Th24: :: RMOD_2:24 for R being Ring for V being RightMod of R holds V is Submodule of V proof let R be Ring; ::_thesis: for V being RightMod of R holds V is Submodule of V let V be RightMod of R; ::_thesis: V is Submodule of V A1: the rmult of V = the rmult of V | [: the carrier of V, the carrier of R:] by RELSET_1:19; ( 0. V = 0. V & the addF of V = the addF of V | [: the carrier of V, the carrier of V:] ) by RELSET_1:19; hence V is Submodule of V by A1, Def2; ::_thesis: verum end; theorem Th25: :: RMOD_2:25 for R being Ring for X, V being strict RightMod of R st V is Submodule of X & X is Submodule of V holds V = X proof let R be Ring; ::_thesis: for X, V being strict RightMod of R st V is Submodule of X & X is Submodule of V holds V = X let X, V be strict RightMod of R; ::_thesis: ( V is Submodule of X & X is Submodule of V implies V = X ) assume that A1: V is Submodule of X and A2: X is Submodule of V ; ::_thesis: V = X set VX = the carrier of X; set VV = the carrier of V; ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, A2, Def2; then A3: the carrier of V = the carrier of X by XBOOLE_0:def_10; set AX = the addF of X; set AV = the addF of V; ( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X ) by A1, A2, Def2; then A4: the addF of V = the addF of X by A3, RELAT_1:72; set MX = the rmult of X; set MV = the rmult of V; A5: the rmult of X = the rmult of V | [: the carrier of X, the carrier of R:] by A2, Def2; ( 0. V = 0. X & the rmult of V = the rmult of X | [: the carrier of V, the carrier of R:] ) by A1, Def2; hence V = X by A3, A4, A5, RELAT_1:72; ::_thesis: verum end; registration let R be Ring; let V be RightMod of R; cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like for Submodule of V; existence ex b1 being Submodule of V st b1 is strict proof set M = the rmult of V; set W = RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); A1: RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is RightMod-like proof let a, b be Scalar of R; :: according to VECTSP_2:def_9 ::_thesis: for b1, b2 being Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) holds ( (b1 + b2) * a = (b1 * a) + (b2 * a) & b1 * (a + b) = (b1 * a) + (b1 * b) & b1 * (b * a) = (b1 * b) * a & b1 * (1_ R) = b1 ) let v, w be Vector of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); ::_thesis: ( (v + w) * a = (v * a) + (w * a) & v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v ) reconsider x = v, y = w as Vector of V ; thus (v + w) * a = (x + y) * a .= (x * a) + (y * a) by VECTSP_2:def_9 .= (v * a) + (w * a) ; ::_thesis: ( v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v ) thus v * (a + b) = x * (a + b) .= (x * a) + (x * b) by VECTSP_2:def_9 .= (v * a) + (v * b) ; ::_thesis: ( v * (b * a) = (v * b) * a & v * (1_ R) = v ) thus v * (b * a) = x * (b * a) .= (x * b) * a by VECTSP_2:def_9 .= (v * b) * a ; ::_thesis: v * (1_ R) = v thus v * (1_ R) = x * (1_ R) .= v by VECTSP_2:def_9 ; ::_thesis: verum end; A2: for a, b being Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) for x, y being Vector of V st x = a & b = y holds a + b = x + y ; ( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Abelian & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable ) proof thus RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Abelian ::_thesis: ( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable ) proof let a, b be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a reconsider x = a, y = b as Vector of V ; thus a + b = y + x by A2 .= b + a ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable ) let a, b, c be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); ::_thesis: (a + b) + c = a + (b + c) reconsider x = a, y = b, z = c as Vector of V ; thus (a + b) + c = (x + y) + z .= x + (y + z) by RLVECT_1:def_3 .= a + (b + c) ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable let a be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); ::_thesis: a + (0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) = a reconsider x = a as Vector of V ; thus a + (0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) = x + (0. V) .= a by RLVECT_1:def_4 ; ::_thesis: verum end; let a be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable reconsider x = a as Vector of V ; reconsider b = (comp V) . x as Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) ; take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) thus a + b = x + (- x) by VECTSP_1:def_13 .= 0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) by RLVECT_1:5 ; ::_thesis: verum end; then reconsider W = RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) as RightMod of R by A1; A3: ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19; the rmult of W = the rmult of V | [: the carrier of W, the carrier of R:] by RELSET_1:19; then reconsider W = W as Submodule of V by A3, Def2; take W ; ::_thesis: W is strict thus W is strict ; ::_thesis: verum end; end; theorem Th26: :: RMOD_2:26 for R being Ring for V, X, Y being RightMod of R st V is Submodule of X & X is Submodule of Y holds V is Submodule of Y proof let R be Ring; ::_thesis: for V, X, Y being RightMod of R st V is Submodule of X & X is Submodule of Y holds V is Submodule of Y let V, X, Y be RightMod of R; ::_thesis: ( V is Submodule of X & X is Submodule of Y implies V is Submodule of Y ) assume that A1: V is Submodule of X and A2: X is Submodule of Y ; ::_thesis: V is Submodule of Y ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y ) by A1, A2, Def2; then A3: the carrier of V c= the carrier of Y by XBOOLE_1:1; A4: the addF of V = the addF of Y | [: the carrier of V, the carrier of V:] proof set AY = the addF of Y; set VX = the carrier of X; set AX = the addF of X; set VV = the carrier of V; set AV = the addF of V; the carrier of V c= the carrier of X by A1, Def2; then A5: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96; the addF of V = the addF of X || the carrier of V by A1, Def2; then the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def2; hence the addF of V = the addF of Y | [: the carrier of V, the carrier of V:] by A5, FUNCT_1:51; ::_thesis: verum end; set MY = the rmult of Y; set MX = the rmult of X; set MV = the rmult of V; set VX = the carrier of X; set VV = the carrier of V; the carrier of V c= the carrier of X by A1, Def2; then A6: [: the carrier of V, the carrier of R:] c= [: the carrier of X, the carrier of R:] by ZFMISC_1:95; the rmult of V = the rmult of X | [: the carrier of V, the carrier of R:] by A1, Def2; then the rmult of V = ( the rmult of Y | [: the carrier of X, the carrier of R:]) | [: the carrier of V, the carrier of R:] by A2, Def2; then A7: the rmult of V = the rmult of Y | [: the carrier of V, the carrier of R:] by A6, FUNCT_1:51; 0. V = 0. X by A1, Def2; then 0. V = 0. Y by A2, Def2; hence V is Submodule of Y by A3, A4, A7, Def2; ::_thesis: verum end; theorem Th27: :: RMOD_2:27 for R being Ring for V being RightMod of R for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds W1 is Submodule of W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds W1 is Submodule of W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds W1 is Submodule of W2 let W1, W2 be Submodule of V; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2 ) set VW1 = the carrier of W1; set VW2 = the carrier of W2; set MW1 = the rmult of W1; set MW2 = the rmult of W2; set AV = the addF of V; set MV = the rmult of V; A1: ( the addF of W1 = the addF of V || the carrier of W1 & the addF of W2 = the addF of V || the carrier of W2 ) by Def2; assume A2: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 is Submodule of W2 then [: the carrier of W1, the carrier of W1:] c= [: the carrier of W2, the carrier of W2:] by ZFMISC_1:96; then A3: the addF of W1 = the addF of W2 | [: the carrier of W1, the carrier of W1:] by A1, FUNCT_1:51; A4: ( the rmult of W1 = the rmult of V | [: the carrier of W1, the carrier of R:] & the rmult of W2 = the rmult of V | [: the carrier of W2, the carrier of R:] ) by Def2; [: the carrier of W1, the carrier of R:] c= [: the carrier of W2, the carrier of R:] by A2, ZFMISC_1:95; then A5: the rmult of W1 = the rmult of W2 | [: the carrier of W1, the carrier of R:] by A4, FUNCT_1:51; ( 0. W1 = 0. V & 0. W2 = 0. V ) by Def2; hence W1 is Submodule of W2 by A2, A3, A5, Def2; ::_thesis: verum end; theorem :: RMOD_2:28 for R being Ring for V being RightMod of R for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds v in W2 ) holds W1 is Submodule of W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds v in W2 ) holds W1 is Submodule of W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds v in W2 ) holds W1 is Submodule of W2 let W1, W2 be Submodule of V; ::_thesis: ( ( for v being Vector of V st v in W1 holds v in W2 ) implies W1 is Submodule of W2 ) assume A1: for v being Vector of V st v in W1 holds v in W2 ; ::_thesis: W1 is Submodule of W2 the carrier of W1 c= the carrier of W2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 ) assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2 the carrier of W1 c= the carrier of V by Def2; then reconsider v = x as Vector of V by A2; v in W1 by A2, STRUCT_0:def_5; then v in W2 by A1; hence x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum end; hence W1 is Submodule of W2 by Th27; ::_thesis: verum end; theorem Th29: :: RMOD_2:29 for R being Ring for V being RightMod of R for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds W1 = W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds W1 = W2 let V be RightMod of R; ::_thesis: for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds W1 = W2 let W1, W2 be strict Submodule of V; ::_thesis: ( the carrier of W1 = the carrier of W2 implies W1 = W2 ) assume the carrier of W1 = the carrier of W2 ; ::_thesis: W1 = W2 then ( W1 is Submodule of W2 & W2 is Submodule of W1 ) by Th27; hence W1 = W2 by Th25; ::_thesis: verum end; theorem Th30: :: RMOD_2:30 for R being Ring for V being RightMod of R for W1, W2 being strict Submodule of V st ( for v being Vector of V holds ( v in W1 iff v in W2 ) ) holds W1 = W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being strict Submodule of V st ( for v being Vector of V holds ( v in W1 iff v in W2 ) ) holds W1 = W2 let V be RightMod of R; ::_thesis: for W1, W2 being strict Submodule of V st ( for v being Vector of V holds ( v in W1 iff v in W2 ) ) holds W1 = W2 let W1, W2 be strict Submodule of V; ::_thesis: ( ( for v being Vector of V holds ( v in W1 iff v in W2 ) ) implies W1 = W2 ) assume A1: for v being Vector of V holds ( v in W1 iff v in W2 ) ; ::_thesis: W1 = W2 for x being set holds ( x in the carrier of W1 iff x in the carrier of W2 ) proof let x be set ; ::_thesis: ( x in the carrier of W1 iff x in the carrier of W2 ) thus ( x in the carrier of W1 implies x in the carrier of W2 ) ::_thesis: ( x in the carrier of W2 implies x in the carrier of W1 ) proof assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2 the carrier of W1 c= the carrier of V by Def2; then reconsider v = x as Vector of V by A2; v in W1 by A2, STRUCT_0:def_5; then v in W2 by A1; hence x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum end; assume A3: x in the carrier of W2 ; ::_thesis: x in the carrier of W1 the carrier of W2 c= the carrier of V by Def2; then reconsider v = x as Vector of V by A3; v in W2 by A3, STRUCT_0:def_5; then v in W1 by A1; hence x in the carrier of W1 by STRUCT_0:def_5; ::_thesis: verum end; then the carrier of W1 = the carrier of W2 by TARSKI:1; hence W1 = W2 by Th29; ::_thesis: verum end; theorem :: RMOD_2:31 for R being Ring for V being strict RightMod of R for W being strict Submodule of V st the carrier of W = the carrier of V holds W = V proof let R be Ring; ::_thesis: for V being strict RightMod of R for W being strict Submodule of V st the carrier of W = the carrier of V holds W = V let V be strict RightMod of R; ::_thesis: for W being strict Submodule of V st the carrier of W = the carrier of V holds W = V let W be strict Submodule of V; ::_thesis: ( the carrier of W = the carrier of V implies W = V ) assume A1: the carrier of W = the carrier of V ; ::_thesis: W = V V is Submodule of V by Th24; hence W = V by A1, Th29; ::_thesis: verum end; theorem :: RMOD_2:32 for R being Ring for V being strict RightMod of R for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds W = V proof let R be Ring; ::_thesis: for V being strict RightMod of R for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds W = V let V be strict RightMod of R; ::_thesis: for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds W = V let W be strict Submodule of V; ::_thesis: ( ( for v being Vector of V holds v in W ) implies W = V ) assume for v being Vector of V holds v in W ; ::_thesis: W = V then A1: for v being Vector of V holds ( v in W iff v in V ) by RLVECT_1:1; V is Submodule of V by Th24; hence W = V by A1, Th30; ::_thesis: verum end; theorem :: RMOD_2:33 for R being Ring for V being RightMod of R for V1 being Subset of V for W being Submodule of V st the carrier of W = V1 holds V1 is linearly-closed by Lm1; theorem Th34: :: RMOD_2:34 for R being Ring for V being RightMod of R for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds ex W being strict Submodule of V st V1 = the carrier of W proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds ex W being strict Submodule of V st V1 = the carrier of W let V be RightMod of R; ::_thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds ex W being strict Submodule of V st V1 = the carrier of W let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Submodule of V st V1 = the carrier of W ) assume that A1: V1 <> {} and A2: V1 is linearly-closed ; ::_thesis: ex W being strict Submodule of V st V1 = the carrier of W reconsider D = V1 as non empty set by A1; reconsider d = 0. V as Element of D by A2, Th1; set VV = the carrier of V; set C = (comp V) | D; dom (comp V) = the carrier of V by FUNCT_2:def_1; then A3: dom ((comp V) | D) = D by RELAT_1:62; A4: rng ((comp V) | D) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((comp V) | D) or x in D ) assume x in rng ((comp V) | D) ; ::_thesis: x in D then consider y being set such that A5: y in dom ((comp V) | D) and A6: ((comp V) | D) . y = x by FUNCT_1:def_3; reconsider y = y as Vector of V by A3, A5; x = (comp V) . y by A5, A6, FUNCT_1:47 .= - y by VECTSP_1:def_13 ; hence x in D by A2, A3, A5, Th2; ::_thesis: verum end; set M = the rmult of V | [:D, the carrier of R:]; dom the rmult of V = [: the carrier of V, the carrier of R:] by FUNCT_2:def_1; then A7: dom ( the rmult of V | [:D, the carrier of R:]) = [:D, the carrier of R:] by RELAT_1:62, ZFMISC_1:96; A8: rng ( the rmult of V | [:D, the carrier of R:]) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the rmult of V | [:D, the carrier of R:]) or x in D ) assume x in rng ( the rmult of V | [:D, the carrier of R:]) ; ::_thesis: x in D then consider y being set such that A9: y in dom ( the rmult of V | [:D, the carrier of R:]) and A10: ( the rmult of V | [:D, the carrier of R:]) . y = x by FUNCT_1:def_3; consider y2, y1 being set such that A11: [y2,y1] = y by A7, A9, RELAT_1:def_1; reconsider y1 = y1 as Scalar of R by A7, A9, A11, ZFMISC_1:87; A12: y2 in V1 by A7, A9, A11, ZFMISC_1:87; then reconsider y2 = y2 as Vector of V ; x = y2 * y1 by A9, A10, A11, FUNCT_1:47; hence x in D by A2, A12, Def1; ::_thesis: verum end; reconsider C = (comp V) | D as UnOp of D by A3, A4, FUNCT_2:def_1, RELSET_1:4; set A = the addF of V || D; dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1; then A13: dom ( the addF of V || D) = [:D,D:] by RELAT_1:62, ZFMISC_1:96; A14: rng ( the addF of V || D) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the addF of V || D) or x in D ) assume x in rng ( the addF of V || D) ; ::_thesis: x in D then consider y being set such that A15: y in dom ( the addF of V || D) and A16: ( the addF of V || D) . y = x by FUNCT_1:def_3; consider y1, y2 being set such that A17: [y1,y2] = y by A13, A15, RELAT_1:def_1; A18: ( y1 in D & y2 in D ) by A13, A15, A17, ZFMISC_1:87; then reconsider y1 = y1, y2 = y2 as Vector of V ; x = y1 + y2 by A15, A16, A17, FUNCT_1:47; hence x in D by A2, A18, Def1; ::_thesis: verum end; reconsider M = the rmult of V | [:D, the carrier of R:] as Function of [:D, the carrier of R:],D by A7, A8, FUNCT_2:def_1, RELSET_1:4; reconsider A = the addF of V || D as BinOp of D by A13, A14, FUNCT_2:def_1, RELSET_1:4; set W = RightModStr(# D,A,d,M #); A19: for a, b being Element of RightModStr(# D,A,d,M #) for x, y being Vector of V st x = a & b = y holds a + b = x + y proof let a, b be Element of RightModStr(# D,A,d,M #); ::_thesis: for x, y being Vector of V st x = a & b = y holds a + b = x + y let x, y be Vector of V; ::_thesis: ( x = a & b = y implies a + b = x + y ) assume A20: ( x = a & b = y ) ; ::_thesis: a + b = x + y thus a + b = A . [a,b] .= x + y by A13, A20, FUNCT_1:47 ; ::_thesis: verum end; A21: ( RightModStr(# D,A,d,M #) is Abelian & RightModStr(# D,A,d,M #) is add-associative & RightModStr(# D,A,d,M #) is right_zeroed & RightModStr(# D,A,d,M #) is right_complementable ) proof thus RightModStr(# D,A,d,M #) is Abelian ::_thesis: ( RightModStr(# D,A,d,M #) is add-associative & RightModStr(# D,A,d,M #) is right_zeroed & RightModStr(# D,A,d,M #) is right_complementable ) proof let a, b be Element of RightModStr(# D,A,d,M #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a reconsider x = a, y = b as Vector of V by TARSKI:def_3; thus a + b = y + x by A19 .= b + a by A19 ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( RightModStr(# D,A,d,M #) is right_zeroed & RightModStr(# D,A,d,M #) is right_complementable ) let a, b, c be Element of RightModStr(# D,A,d,M #); ::_thesis: (a + b) + c = a + (b + c) reconsider x = a, y = b, z = c as Vector of V by TARSKI:def_3; A22: b + c = y + z by A19; a + b = x + y by A19; hence (a + b) + c = (x + y) + z by A19 .= x + (y + z) by RLVECT_1:def_3 .= a + (b + c) by A19, A22 ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: RightModStr(# D,A,d,M #) is right_complementable let a be Element of RightModStr(# D,A,d,M #); ::_thesis: a + (0. RightModStr(# D,A,d,M #)) = a reconsider x = a as Vector of V by TARSKI:def_3; thus a + (0. RightModStr(# D,A,d,M #)) = x + (0. V) by A19 .= a by RLVECT_1:def_4 ; ::_thesis: verum end; let a be Element of RightModStr(# D,A,d,M #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable reconsider x = a as Vector of V by TARSKI:def_3; reconsider b9 = (comp V) . x as Vector of V ; C . x in D by FUNCT_2:5; then reconsider b = ((comp V) | D) . x as Element of RightModStr(# D,A,d,M #) ; take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. RightModStr(# D,A,d,M #) thus a + b = x + b9 by A19, FUNCT_1:49 .= x + (- x) by VECTSP_1:def_13 .= 0. RightModStr(# D,A,d,M #) by RLVECT_1:5 ; ::_thesis: verum end; RightModStr(# D,A,d,M #) is RightMod-like proof let a, b be Scalar of R; :: according to VECTSP_2:def_9 ::_thesis: for b1, b2 being Element of the carrier of RightModStr(# D,A,d,M #) holds ( (b1 + b2) * a = (b1 * a) + (b2 * a) & b1 * (a + b) = (b1 * a) + (b1 * b) & b1 * (b * a) = (b1 * b) * a & b1 * (1_ R) = b1 ) let v, w be Vector of RightModStr(# D,A,d,M #); ::_thesis: ( (v + w) * a = (v * a) + (w * a) & v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v ) reconsider x = v, y = w as Vector of V by TARSKI:def_3; A23: now__::_thesis:_for_a_being_Scalar_of_R for_x_being_Element_of_RightModStr(#_D,A,d,M_#) for_y_being_Vector_of_V_st_y_=_x_holds_ x_*_a_=_y_*_a let a be Scalar of R; ::_thesis: for x being Element of RightModStr(# D,A,d,M #) for y being Vector of V st y = x holds x * a = y * a let x be Element of RightModStr(# D,A,d,M #); ::_thesis: for y being Vector of V st y = x holds x * a = y * a let y be Vector of V; ::_thesis: ( y = x implies x * a = y * a ) assume A24: y = x ; ::_thesis: x * a = y * a [x,a] in dom M by A7; hence x * a = y * a by A24, FUNCT_1:47; ::_thesis: verum end; then A25: v * a = x * a ; A26: w * a = y * a by A23; v + w = x + y by A19; hence (v + w) * a = (x + y) * a by A23 .= (x * a) + (y * a) by VECTSP_2:def_9 .= (v * a) + (w * a) by A19, A25, A26 ; ::_thesis: ( v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v ) A27: v * b = x * b by A23; thus v * (a + b) = x * (a + b) by A23 .= (x * a) + (x * b) by VECTSP_2:def_9 .= (v * a) + (v * b) by A19, A27, A25 ; ::_thesis: ( v * (b * a) = (v * b) * a & v * (1_ R) = v ) thus v * (b * a) = x * (b * a) by A23 .= (x * b) * a by VECTSP_2:def_9 .= (v * b) * a by A23, A27 ; ::_thesis: v * (1_ R) = v thus v * (1_ R) = x * (1_ R) by A23 .= v by VECTSP_2:def_9 ; ::_thesis: verum end; then reconsider W = RightModStr(# D,A,d,M #) as RightMod of R by A21; 0. W = 0. V ; then reconsider W = W as strict Submodule of V by Def2; take W ; ::_thesis: V1 = the carrier of W thus V1 = the carrier of W ; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; func (0). V -> strict Submodule of V means :Def3: :: RMOD_2:def 3 the carrier of it = {(0. V)}; correctness existence ex b1 being strict Submodule of V st the carrier of b1 = {(0. V)}; uniqueness for b1, b2 being strict Submodule of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds b1 = b2; by Th4, Th29, Th34; end; :: deftheorem Def3 defines (0). RMOD_2:def_3_:_ for R being Ring for V being RightMod of R for b3 being strict Submodule of V holds ( b3 = (0). V iff the carrier of b3 = {(0. V)} ); definition let R be Ring; let V be RightMod of R; func (Omega). V -> strict Submodule of V equals :: RMOD_2:def 4 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); coherence RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V proof set W = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); A1: RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is RightMod-like proof let x, y be Element of R; :: according to VECTSP_2:def_9 ::_thesis: for b1, b2 being Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) holds ( (b1 + b2) * x = (b1 * x) + (b2 * x) & b1 * (x + y) = (b1 * x) + (b1 * y) & b1 * (y * x) = (b1 * y) * x & b1 * (1_ R) = b1 ) let v, w be Element of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); ::_thesis: ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) reconsider v9 = v, w9 = w as Vector of V ; thus (v + w) * x = (v9 + w9) * x .= (v9 * x) + (w9 * x) by VECTSP_2:def_9 .= (v * x) + (w * x) ; ::_thesis: ( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) thus v * (x + y) = v9 * (x + y) .= (v9 * x) + (v9 * y) by VECTSP_2:def_9 .= (v * x) + (v * y) ; ::_thesis: ( v * (y * x) = (v * y) * x & v * (1_ R) = v ) thus v * (y * x) = v9 * (y * x) .= (v9 * y) * x by VECTSP_2:def_9 .= (v * y) * x ; ::_thesis: v * (1_ R) = v thus v * (1_ R) = v9 * (1_ R) .= v by VECTSP_2:def_9 ; ::_thesis: verum end; A2: for a being Scalar of R for v, w being Vector of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) for v9, w9 being Vector of V st v = v9 & w = w9 holds ( v + w = v9 + w9 & v * a = v9 * a ) ; ( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Abelian & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_complementable ) proof thus RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Abelian ::_thesis: ( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_complementable ) proof let x, y be Element of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x reconsider x9 = x, y9 = y as Vector of V ; thus x + y = y9 + x9 by A2 .= y + x ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_complementable ) let x, y, z be Element of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); ::_thesis: (x + y) + z = x + (y + z) reconsider x9 = x, y9 = y, z9 = z as Vector of V ; thus (x + y) + z = (x9 + y9) + z9 .= x9 + (y9 + z9) by RLVECT_1:def_3 .= x + (y + z) ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_complementable let x be Element of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); ::_thesis: x + (0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) = x reconsider x9 = x as Vector of V ; thus x + (0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) = x9 + (0. V) .= x by RLVECT_1:4 ; ::_thesis: verum end; let x be Element of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider x9 = x as Vector of V ; consider b being Vector of V such that A3: x9 + b = 0. V by ALGSTR_0:def_11; reconsider b9 = b as Element of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) ; take b9 ; :: according to ALGSTR_0:def_11 ::_thesis: x + b9 = 0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) thus x + b9 = 0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) by A3; ::_thesis: verum end; then reconsider W = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) as RightMod of R by A1; A4: the rmult of W = the rmult of V | [: the carrier of W, the carrier of R:] by RELSET_1:19; ( 0. W = 0. V & the addF of W = the addF of V | [: the carrier of W, the carrier of W:] ) by RELSET_1:19; hence RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V by A4, Def2; ::_thesis: verum end; end; :: deftheorem defines (Omega). RMOD_2:def_4_:_ for R being Ring for V being RightMod of R holds (Omega). V = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #); theorem :: RMOD_2:35 for x being set for R being Ring for V being RightMod of R holds ( x in (0). V iff x = 0. V ) proof let x be set ; ::_thesis: for R being Ring for V being RightMod of R holds ( x in (0). V iff x = 0. V ) let R be Ring; ::_thesis: for V being RightMod of R holds ( x in (0). V iff x = 0. V ) let V be RightMod of R; ::_thesis: ( x in (0). V iff x = 0. V ) thus ( x in (0). V implies x = 0. V ) ::_thesis: ( x = 0. V implies x in (0). V ) proof assume x in (0). V ; ::_thesis: x = 0. V then x in the carrier of ((0). V) by STRUCT_0:def_5; then x in {(0. V)} by Def3; hence x = 0. V by TARSKI:def_1; ::_thesis: verum end; thus ( x = 0. V implies x in (0). V ) by Th17; ::_thesis: verum end; theorem Th36: :: RMOD_2:36 for R being Ring for V being RightMod of R for W being Submodule of V holds (0). W = (0). V proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V holds (0). W = (0). V let V be RightMod of R; ::_thesis: for W being Submodule of V holds (0). W = (0). V let W be Submodule of V; ::_thesis: (0). W = (0). V ( the carrier of ((0). W) = {(0. W)} & the carrier of ((0). V) = {(0. V)} ) by Def3; then A1: the carrier of ((0). W) = the carrier of ((0). V) by Def2; (0). W is Submodule of V by Th26; hence (0). W = (0). V by A1, Th29; ::_thesis: verum end; theorem Th37: :: RMOD_2:37 for R being Ring for V being RightMod of R for W1, W2 being Submodule of V holds (0). W1 = (0). W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V holds (0). W1 = (0). W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds (0). W1 = (0). W2 let W1, W2 be Submodule of V; ::_thesis: (0). W1 = (0). W2 (0). W1 = (0). V by Th36; hence (0). W1 = (0). W2 by Th36; ::_thesis: verum end; theorem :: RMOD_2:38 for R being Ring for V being RightMod of R for W being Submodule of V holds (0). W is Submodule of V by Th26; theorem :: RMOD_2:39 for R being Ring for V being RightMod of R for W being Submodule of V holds (0). V is Submodule of W proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V holds (0). V is Submodule of W let V be RightMod of R; ::_thesis: for W being Submodule of V holds (0). V is Submodule of W let W be Submodule of V; ::_thesis: (0). V is Submodule of W (0). W = (0). V by Th36; hence (0). V is Submodule of W ; ::_thesis: verum end; theorem :: RMOD_2:40 for R being Ring for V being RightMod of R for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2 let V be RightMod of R; ::_thesis: for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2 let W1, W2 be Submodule of V; ::_thesis: (0). W1 is Submodule of W2 (0). W1 = (0). W2 by Th37; hence (0). W1 is Submodule of W2 ; ::_thesis: verum end; theorem :: RMOD_2:41 for R being Ring for V being strict RightMod of R holds V is Submodule of (Omega). V ; definition let R be Ring; let V be RightMod of R; let v be Vector of V; let W be Submodule of V; funcv + W -> Subset of V equals :: RMOD_2:def 5 { (v + u) where u is Vector of V : u in W } ; coherence { (v + u) where u is Vector of V : u in W } is Subset of V proof set Y = { (v + u) where u is Vector of V : u in W } ; defpred S1[ set ] means ex u being Vector of V st ( $1 = v + u & u in W ); consider X being set such that A1: for x being set holds ( x in X iff ( x in the carrier of V & S1[x] ) ) from XBOOLE_0:sch_1(); X c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of V ) assume x in X ; ::_thesis: x in the carrier of V hence x in the carrier of V by A1; ::_thesis: verum end; then reconsider X = X as Subset of V ; A2: { (v + u) where u is Vector of V : u in W } c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where u is Vector of V : u in W } or x in X ) assume x in { (v + u) where u is Vector of V : u in W } ; ::_thesis: x in X then ex u being Vector of V st ( x = v + u & u in W ) ; hence x in X by A1; ::_thesis: verum end; X c= { (v + u) where u is Vector of V : u in W } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { (v + u) where u is Vector of V : u in W } ) assume x in X ; ::_thesis: x in { (v + u) where u is Vector of V : u in W } then ex u being Vector of V st ( x = v + u & u in W ) by A1; hence x in { (v + u) where u is Vector of V : u in W } ; ::_thesis: verum end; hence { (v + u) where u is Vector of V : u in W } is Subset of V by A2, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines + RMOD_2:def_5_:_ for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds v + W = { (v + u) where u is Vector of V : u in W } ; Lm2: for R being Ring for V being RightMod of R for W being Submodule of V holds (0. V) + W = the carrier of W proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V holds (0. V) + W = the carrier of W let V be RightMod of R; ::_thesis: for W being Submodule of V holds (0. V) + W = the carrier of W let W be Submodule of V; ::_thesis: (0. V) + W = the carrier of W set A = { ((0. V) + u) where u is Vector of V : u in W } ; A1: the carrier of W c= { ((0. V) + u) where u is Vector of V : u in W } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in { ((0. V) + u) where u is Vector of V : u in W } ) assume x in the carrier of W ; ::_thesis: x in { ((0. V) + u) where u is Vector of V : u in W } then A2: x in W by STRUCT_0:def_5; then x in V by Th9; then reconsider y = x as Element of V by STRUCT_0:def_5; (0. V) + y = x by RLVECT_1:def_4; hence x in { ((0. V) + u) where u is Vector of V : u in W } by A2; ::_thesis: verum end; { ((0. V) + u) where u is Vector of V : u in W } c= the carrier of W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((0. V) + u) where u is Vector of V : u in W } or x in the carrier of W ) assume x in { ((0. V) + u) where u is Vector of V : u in W } ; ::_thesis: x in the carrier of W then consider u being Vector of V such that A3: x = (0. V) + u and A4: u in W ; x = u by A3, RLVECT_1:def_4; hence x in the carrier of W by A4, STRUCT_0:def_5; ::_thesis: verum end; hence (0. V) + W = the carrier of W by A1, XBOOLE_0:def_10; ::_thesis: verum end; definition let R be Ring; let V be RightMod of R; let W be Submodule of V; mode Coset of W -> Subset of V means :Def6: :: RMOD_2:def 6 ex v being Vector of V st it = v + W; existence ex b1 being Subset of V ex v being Vector of V st b1 = v + W proof reconsider VW = the carrier of W as Subset of V by Def2; take VW ; ::_thesis: ex v being Vector of V st VW = v + W take 0. V ; ::_thesis: VW = (0. V) + W thus VW = (0. V) + W by Lm2; ::_thesis: verum end; end; :: deftheorem Def6 defines Coset RMOD_2:def_6_:_ for R being Ring for V being RightMod of R for W being Submodule of V for b4 being Subset of V holds ( b4 is Coset of W iff ex v being Vector of V st b4 = v + W ); theorem Th42: :: RMOD_2:42 for x being set for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( x in v + W iff ex u being Vector of V st ( u in W & x = v + u ) ) proof let x be set ; ::_thesis: for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( x in v + W iff ex u being Vector of V st ( u in W & x = v + u ) ) let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( x in v + W iff ex u being Vector of V st ( u in W & x = v + u ) ) let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V holds ( x in v + W iff ex u being Vector of V st ( u in W & x = v + u ) ) let v be Vector of V; ::_thesis: for W being Submodule of V holds ( x in v + W iff ex u being Vector of V st ( u in W & x = v + u ) ) let W be Submodule of V; ::_thesis: ( x in v + W iff ex u being Vector of V st ( u in W & x = v + u ) ) thus ( x in v + W implies ex u being Vector of V st ( u in W & x = v + u ) ) ::_thesis: ( ex u being Vector of V st ( u in W & x = v + u ) implies x in v + W ) proof assume x in v + W ; ::_thesis: ex u being Vector of V st ( u in W & x = v + u ) then consider u being Vector of V such that A1: ( x = v + u & u in W ) ; take u ; ::_thesis: ( u in W & x = v + u ) thus ( u in W & x = v + u ) by A1; ::_thesis: verum end; given u being Vector of V such that A2: ( u in W & x = v + u ) ; ::_thesis: x in v + W thus x in v + W by A2; ::_thesis: verum end; theorem Th43: :: RMOD_2:43 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( 0. V in v + W iff v in W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( 0. V in v + W iff v in W ) let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V holds ( 0. V in v + W iff v in W ) let v be Vector of V; ::_thesis: for W being Submodule of V holds ( 0. V in v + W iff v in W ) let W be Submodule of V; ::_thesis: ( 0. V in v + W iff v in W ) thus ( 0. V in v + W implies v in W ) ::_thesis: ( v in W implies 0. V in v + W ) proof assume 0. V in v + W ; ::_thesis: v in W then consider u being Vector of V such that A1: 0. V = v + u and A2: u in W ; v = - u by A1, VECTSP_1:16; hence v in W by A2, Th22; ::_thesis: verum end; assume v in W ; ::_thesis: 0. V in v + W then A3: - v in W by Th22; 0. V = v + (- v) by VECTSP_1:19; hence 0. V in v + W by A3; ::_thesis: verum end; theorem Th44: :: RMOD_2:44 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds v in v + W proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V holds v in v + W let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V holds v in v + W let v be Vector of V; ::_thesis: for W being Submodule of V holds v in v + W let W be Submodule of V; ::_thesis: v in v + W ( v + (0. V) = v & 0. V in W ) by Th17, RLVECT_1:def_4; hence v in v + W ; ::_thesis: verum end; theorem :: RMOD_2:45 for R being Ring for V being RightMod of R for W being Submodule of V holds (0. V) + W = the carrier of W by Lm2; theorem Th46: :: RMOD_2:46 for R being Ring for V being RightMod of R for v being Vector of V holds v + ((0). V) = {v} proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V holds v + ((0). V) = {v} let V be RightMod of R; ::_thesis: for v being Vector of V holds v + ((0). V) = {v} let v be Vector of V; ::_thesis: v + ((0). V) = {v} thus v + ((0). V) c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= v + ((0). V) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + ((0). V) or x in {v} ) assume x in v + ((0). V) ; ::_thesis: x in {v} then consider u being Vector of V such that A1: x = v + u and A2: u in (0). V ; A3: the carrier of ((0). V) = {(0. V)} by Def3; u in the carrier of ((0). V) by A2, STRUCT_0:def_5; then u = 0. V by A3, TARSKI:def_1; then x = v by A1, RLVECT_1:def_4; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in v + ((0). V) ) assume x in {v} ; ::_thesis: x in v + ((0). V) then A4: x = v by TARSKI:def_1; ( 0. V in (0). V & v = v + (0. V) ) by Th17, RLVECT_1:def_4; hence x in v + ((0). V) by A4; ::_thesis: verum end; Lm3: for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( v in W iff v + W = the carrier of W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( v in W iff v + W = the carrier of W ) let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V holds ( v in W iff v + W = the carrier of W ) let v be Vector of V; ::_thesis: for W being Submodule of V holds ( v in W iff v + W = the carrier of W ) let W be Submodule of V; ::_thesis: ( v in W iff v + W = the carrier of W ) ( 0. V in W & v + (0. V) = v ) by Th17, RLVECT_1:def_4; then A1: v in { (v + u) where u is Vector of V : u in W } ; thus ( v in W implies v + W = the carrier of W ) ::_thesis: ( v + W = the carrier of W implies v in W ) proof assume A2: v in W ; ::_thesis: v + W = the carrier of W thus v + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= v + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in the carrier of W ) assume x in v + W ; ::_thesis: x in the carrier of W then consider u being Vector of V such that A3: x = v + u and A4: u in W ; v + u in W by A2, A4, Th20; hence x in the carrier of W by A3, STRUCT_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in v + W ) assume x in the carrier of W ; ::_thesis: x in v + W then reconsider y = x, z = v as Element of W by A2, STRUCT_0:def_5; reconsider y1 = y, z1 = z as Vector of V by Th10; A5: z + (y - z) = y + (z + (- z)) by RLVECT_1:def_3 .= y + (0. W) by VECTSP_1:19 .= x by RLVECT_1:def_4 ; y - z in W by STRUCT_0:def_5; then A6: y1 - z1 in W by Th16; y - z = y1 - z1 by Th16; then z1 + (y1 - z1) = x by A5, Th13; hence x in v + W by A6; ::_thesis: verum end; assume A7: v + W = the carrier of W ; ::_thesis: v in W assume not v in W ; ::_thesis: contradiction hence contradiction by A7, A1, STRUCT_0:def_5; ::_thesis: verum end; theorem Th47: :: RMOD_2:47 for R being Ring for V being RightMod of R for v being Vector of V holds v + ((Omega). V) = the carrier of V proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V holds v + ((Omega). V) = the carrier of V let V be RightMod of R; ::_thesis: for v being Vector of V holds v + ((Omega). V) = the carrier of V let v be Vector of V; ::_thesis: v + ((Omega). V) = the carrier of V v in (Omega). V by RLVECT_1:1; hence v + ((Omega). V) = the carrier of V by Lm3; ::_thesis: verum end; theorem Th48: :: RMOD_2:48 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( 0. V in v + W iff v + W = the carrier of W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( 0. V in v + W iff v + W = the carrier of W ) let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V holds ( 0. V in v + W iff v + W = the carrier of W ) let v be Vector of V; ::_thesis: for W being Submodule of V holds ( 0. V in v + W iff v + W = the carrier of W ) let W be Submodule of V; ::_thesis: ( 0. V in v + W iff v + W = the carrier of W ) ( 0. V in v + W iff v in W ) by Th43; hence ( 0. V in v + W iff v + W = the carrier of W ) by Lm3; ::_thesis: verum end; theorem :: RMOD_2:49 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V holds ( v in W iff v + W = the carrier of W ) by Lm3; theorem :: RMOD_2:50 for R being Ring for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds (v * a) + W = the carrier of W proof let R be Ring; ::_thesis: for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds (v * a) + W = the carrier of W let a be Scalar of R; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds (v * a) + W = the carrier of W let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V st v in W holds (v * a) + W = the carrier of W let v be Vector of V; ::_thesis: for W being Submodule of V st v in W holds (v * a) + W = the carrier of W let W be Submodule of V; ::_thesis: ( v in W implies (v * a) + W = the carrier of W ) assume v in W ; ::_thesis: (v * a) + W = the carrier of W then v * a in W by Th21; hence (v * a) + W = the carrier of W by Lm3; ::_thesis: verum end; theorem Th51: :: RMOD_2:51 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u in W iff v + W = (v + u) + W ) proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u in W iff v + W = (v + u) + W ) let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V holds ( u in W iff v + W = (v + u) + W ) let u, v be Vector of V; ::_thesis: for W being Submodule of V holds ( u in W iff v + W = (v + u) + W ) let W be Submodule of V; ::_thesis: ( u in W iff v + W = (v + u) + W ) thus ( u in W implies v + W = (v + u) + W ) ::_thesis: ( v + W = (v + u) + W implies u in W ) proof assume A1: u in W ; ::_thesis: v + W = (v + u) + W thus v + W c= (v + u) + W :: according to XBOOLE_0:def_10 ::_thesis: (v + u) + W c= v + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in (v + u) + W ) assume x in v + W ; ::_thesis: x in (v + u) + W then consider v1 being Vector of V such that A2: x = v + v1 and A3: v1 in W ; A4: (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def_3 .= v + ((v1 + u) - u) by RLVECT_1:def_3 .= v + (v1 + (u - u)) by RLVECT_1:def_3 .= v + (v1 + (0. V)) by VECTSP_1:19 .= x by A2, RLVECT_1:def_4 ; v1 - u in W by A1, A3, Th23; hence x in (v + u) + W by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v + u) + W or x in v + W ) assume x in (v + u) + W ; ::_thesis: x in v + W then consider v2 being Vector of V such that A5: x = (v + u) + v2 and A6: v2 in W ; A7: x = v + (u + v2) by A5, RLVECT_1:def_3; u + v2 in W by A1, A6, Th20; hence x in v + W by A7; ::_thesis: verum end; assume A8: v + W = (v + u) + W ; ::_thesis: u in W ( 0. V in W & v + (0. V) = v ) by Th17, RLVECT_1:def_4; then v in (v + u) + W by A8; then consider u1 being Vector of V such that A9: v = (v + u) + u1 and A10: u1 in W ; v = v + (u + u1) by A9, RLVECT_1:def_3; then u + u1 = 0. V by RLVECT_1:9; then u = - u1 by VECTSP_1:16; hence u in W by A10, Th22; ::_thesis: verum end; theorem :: RMOD_2:52 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u in W iff v + W = (v - u) + W ) proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u in W iff v + W = (v - u) + W ) let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V holds ( u in W iff v + W = (v - u) + W ) let u, v be Vector of V; ::_thesis: for W being Submodule of V holds ( u in W iff v + W = (v - u) + W ) let W be Submodule of V; ::_thesis: ( u in W iff v + W = (v - u) + W ) A1: ( - u in W implies u in W ) proof assume - u in W ; ::_thesis: u in W then - (- u) in W by Th22; hence u in W by RLVECT_1:17; ::_thesis: verum end; ( - u in W iff v + W = (v + (- u)) + W ) by Th51; hence ( u in W iff v + W = (v - u) + W ) by A1, Th22; ::_thesis: verum end; theorem Th53: :: RMOD_2:53 for R being Ring for V being RightMod of R for v, u being Vector of V for W being Submodule of V holds ( v in u + W iff u + W = v + W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W being Submodule of V holds ( v in u + W iff u + W = v + W ) let V be RightMod of R; ::_thesis: for v, u being Vector of V for W being Submodule of V holds ( v in u + W iff u + W = v + W ) let v, u be Vector of V; ::_thesis: for W being Submodule of V holds ( v in u + W iff u + W = v + W ) let W be Submodule of V; ::_thesis: ( v in u + W iff u + W = v + W ) thus ( v in u + W implies u + W = v + W ) ::_thesis: ( u + W = v + W implies v in u + W ) proof assume v in u + W ; ::_thesis: u + W = v + W then consider z being Vector of V such that A1: v = u + z and A2: z in W ; thus u + W c= v + W :: according to XBOOLE_0:def_10 ::_thesis: v + W c= u + W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in u + W or x in v + W ) assume x in u + W ; ::_thesis: x in v + W then consider v1 being Vector of V such that A3: x = u + v1 and A4: v1 in W ; v - z = u + (z - z) by A1, RLVECT_1:def_3 .= u + (0. V) by VECTSP_1:19 .= u by RLVECT_1:def_4 ; then A5: x = v + (v1 + (- z)) by A3, RLVECT_1:def_3 .= v + (v1 - z) ; v1 - z in W by A2, A4, Th23; hence x in v + W by A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in u + W ) assume x in v + W ; ::_thesis: x in u + W then consider v2 being Vector of V such that A6: ( x = v + v2 & v2 in W ) ; ( z + v2 in W & x = u + (z + v2) ) by A1, A2, A6, Th20, RLVECT_1:def_3; hence x in u + W ; ::_thesis: verum end; thus ( u + W = v + W implies v in u + W ) by Th44; ::_thesis: verum end; theorem Th54: :: RMOD_2:54 for R being Ring for V being RightMod of R for u, v1, v2 being Vector of V for W being Submodule of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W proof let R be Ring; ::_thesis: for V being RightMod of R for u, v1, v2 being Vector of V for W being Submodule of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W let V be RightMod of R; ::_thesis: for u, v1, v2 being Vector of V for W being Submodule of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W let u, v1, v2 be Vector of V; ::_thesis: for W being Submodule of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W let W be Submodule of V; ::_thesis: ( u in v1 + W & u in v2 + W implies v1 + W = v2 + W ) assume that A1: u in v1 + W and A2: u in v2 + W ; ::_thesis: v1 + W = v2 + W thus v1 + W = u + W by A1, Th53 .= v2 + W by A2, Th53 ; ::_thesis: verum end; theorem Th55: :: RMOD_2:55 for R being Ring for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds v * a in v + W proof let R be Ring; ::_thesis: for a being Scalar of R for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds v * a in v + W let a be Scalar of R; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds v * a in v + W let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V st v in W holds v * a in v + W let v be Vector of V; ::_thesis: for W being Submodule of V st v in W holds v * a in v + W let W be Submodule of V; ::_thesis: ( v in W implies v * a in v + W ) assume v in W ; ::_thesis: v * a in v + W then ( v + W = the carrier of W & v * a in W ) by Lm3, Th21; hence v * a in v + W by STRUCT_0:def_5; ::_thesis: verum end; theorem :: RMOD_2:56 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds - v in v + W proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V st v in W holds - v in v + W let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V st v in W holds - v in v + W let v be Vector of V; ::_thesis: for W being Submodule of V st v in W holds - v in v + W let W be Submodule of V; ::_thesis: ( v in W implies - v in v + W ) assume v in W ; ::_thesis: - v in v + W then v * (- (1_ R)) in v + W by Th55; hence - v in v + W by VECTSP_2:32; ::_thesis: verum end; theorem Th57: :: RMOD_2:57 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u + v in v + W iff u in W ) proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u + v in v + W iff u in W ) let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V holds ( u + v in v + W iff u in W ) let u, v be Vector of V; ::_thesis: for W being Submodule of V holds ( u + v in v + W iff u in W ) let W be Submodule of V; ::_thesis: ( u + v in v + W iff u in W ) thus ( u + v in v + W implies u in W ) ::_thesis: ( u in W implies u + v in v + W ) proof assume u + v in v + W ; ::_thesis: u in W then ex v1 being Vector of V st ( u + v = v + v1 & v1 in W ) ; hence u in W by RLVECT_1:8; ::_thesis: verum end; assume u in W ; ::_thesis: u + v in v + W hence u + v in v + W ; ::_thesis: verum end; theorem :: RMOD_2:58 for R being Ring for V being RightMod of R for v, u being Vector of V for W being Submodule of V holds ( v - u in v + W iff u in W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W being Submodule of V holds ( v - u in v + W iff u in W ) let V be RightMod of R; ::_thesis: for v, u being Vector of V for W being Submodule of V holds ( v - u in v + W iff u in W ) let v, u be Vector of V; ::_thesis: for W being Submodule of V holds ( v - u in v + W iff u in W ) let W be Submodule of V; ::_thesis: ( v - u in v + W iff u in W ) A1: v - u = (- u) + v ; A2: ( - u in W implies - (- u) in W ) by Th22; ( u in W implies - u in W ) by Th22; hence ( v - u in v + W iff u in W ) by A1, A2, Th57, RLVECT_1:17; ::_thesis: verum end; theorem :: RMOD_2:59 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u in v + W iff ex v1 being Vector of V st ( v1 in W & u = v - v1 ) ) proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V holds ( u in v + W iff ex v1 being Vector of V st ( v1 in W & u = v - v1 ) ) let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V holds ( u in v + W iff ex v1 being Vector of V st ( v1 in W & u = v - v1 ) ) let u, v be Vector of V; ::_thesis: for W being Submodule of V holds ( u in v + W iff ex v1 being Vector of V st ( v1 in W & u = v - v1 ) ) let W be Submodule of V; ::_thesis: ( u in v + W iff ex v1 being Vector of V st ( v1 in W & u = v - v1 ) ) thus ( u in v + W implies ex v1 being Vector of V st ( v1 in W & u = v - v1 ) ) ::_thesis: ( ex v1 being Vector of V st ( v1 in W & u = v - v1 ) implies u in v + W ) proof assume u in v + W ; ::_thesis: ex v1 being Vector of V st ( v1 in W & u = v - v1 ) then consider v1 being Vector of V such that A1: u = v + v1 and A2: v1 in W ; take x = - v1; ::_thesis: ( x in W & u = v - x ) thus x in W by A2, Th22; ::_thesis: u = v - x thus u = v - x by A1, RLVECT_1:17; ::_thesis: verum end; given v1 being Vector of V such that A3: v1 in W and A4: u = v - v1 ; ::_thesis: u in v + W - v1 in W by A3, Th22; hence u in v + W by A4; ::_thesis: verum end; theorem Th60: :: RMOD_2:60 for R being Ring for V being RightMod of R for v1, v2 being Vector of V for W being Submodule of V holds ( ex v being Vector of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V for W being Submodule of V holds ( ex v being Vector of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V for W being Submodule of V holds ( ex v being Vector of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) let v1, v2 be Vector of V; ::_thesis: for W being Submodule of V holds ( ex v being Vector of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) let W be Submodule of V; ::_thesis: ( ex v being Vector of V st ( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) thus ( ex v being Vector of V st ( v1 in v + W & v2 in v + W ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex v being Vector of V st ( v1 in v + W & v2 in v + W ) ) proof given v being Vector of V such that A1: v1 in v + W and A2: v2 in v + W ; ::_thesis: v1 - v2 in W consider u2 being Vector of V such that A3: u2 in W and A4: v2 = v + u2 by A2, Th42; consider u1 being Vector of V such that A5: u1 in W and A6: v1 = v + u1 by A1, Th42; v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, VECTSP_1:17 .= ((u1 + v) + (- v)) - u2 by RLVECT_1:def_3 .= (u1 + (v + (- v))) - u2 by RLVECT_1:def_3 .= (u1 + (0. V)) - u2 by RLVECT_1:5 .= u1 - u2 by RLVECT_1:def_4 ; hence v1 - v2 in W by A5, A3, Th23; ::_thesis: verum end; assume v1 - v2 in W ; ::_thesis: ex v being Vector of V st ( v1 in v + W & v2 in v + W ) then A7: - (v1 - v2) in W by Th22; take v1 ; ::_thesis: ( v1 in v1 + W & v2 in v1 + W ) thus v1 in v1 + W by Th44; ::_thesis: v2 in v1 + W v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by VECTSP_1:17 .= (v1 + (- v1)) + v2 by RLVECT_1:def_3 .= (0. V) + v2 by RLVECT_1:5 .= v2 by RLVECT_1:def_4 ; hence v2 in v1 + W by A7; ::_thesis: verum end; theorem Th61: :: RMOD_2:61 for R being Ring for V being RightMod of R for v, u being Vector of V for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v + v1 = u ) proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v + v1 = u ) let V be RightMod of R; ::_thesis: for v, u being Vector of V for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v + v1 = u ) let v, u be Vector of V; ::_thesis: for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v + v1 = u ) let W be Submodule of V; ::_thesis: ( v + W = u + W implies ex v1 being Vector of V st ( v1 in W & v + v1 = u ) ) assume v + W = u + W ; ::_thesis: ex v1 being Vector of V st ( v1 in W & v + v1 = u ) then v in u + W by Th44; then consider u1 being Vector of V such that A1: v = u + u1 and A2: u1 in W ; take v1 = u - v; ::_thesis: ( v1 in W & v + v1 = u ) 0. V = (u + u1) - v by A1, VECTSP_1:19 .= u1 + (u - v) by RLVECT_1:def_3 ; then v1 = - u1 by VECTSP_1:16; hence v1 in W by A2, Th22; ::_thesis: v + v1 = u thus v + v1 = (u + v) - v by RLVECT_1:def_3 .= u + (v - v) by RLVECT_1:def_3 .= u + (0. V) by VECTSP_1:19 .= u by RLVECT_1:def_4 ; ::_thesis: verum end; theorem Th62: :: RMOD_2:62 for R being Ring for V being RightMod of R for v, u being Vector of V for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v - v1 = u ) proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v - v1 = u ) let V be RightMod of R; ::_thesis: for v, u being Vector of V for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v - v1 = u ) let v, u be Vector of V; ::_thesis: for W being Submodule of V st v + W = u + W holds ex v1 being Vector of V st ( v1 in W & v - v1 = u ) let W be Submodule of V; ::_thesis: ( v + W = u + W implies ex v1 being Vector of V st ( v1 in W & v - v1 = u ) ) assume v + W = u + W ; ::_thesis: ex v1 being Vector of V st ( v1 in W & v - v1 = u ) then u in v + W by Th44; then consider u1 being Vector of V such that A1: u = v + u1 and A2: u1 in W ; take v1 = v - u; ::_thesis: ( v1 in W & v - v1 = u ) 0. V = (v + u1) - u by A1, VECTSP_1:19 .= u1 + (v - u) by RLVECT_1:def_3 ; then v1 = - u1 by VECTSP_1:16; hence v1 in W by A2, Th22; ::_thesis: v - v1 = u thus v - v1 = (v - v) + u by RLVECT_1:29 .= (0. V) + u by VECTSP_1:19 .= u by RLVECT_1:def_4 ; ::_thesis: verum end; theorem Th63: :: RMOD_2:63 for R being Ring for V being RightMod of R for v being Vector of V for W1, W2 being strict Submodule of V holds ( v + W1 = v + W2 iff W1 = W2 ) proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W1, W2 being strict Submodule of V holds ( v + W1 = v + W2 iff W1 = W2 ) let V be RightMod of R; ::_thesis: for v being Vector of V for W1, W2 being strict Submodule of V holds ( v + W1 = v + W2 iff W1 = W2 ) let v be Vector of V; ::_thesis: for W1, W2 being strict Submodule of V holds ( v + W1 = v + W2 iff W1 = W2 ) let W1, W2 be strict Submodule of V; ::_thesis: ( v + W1 = v + W2 iff W1 = W2 ) thus ( v + W1 = v + W2 implies W1 = W2 ) ::_thesis: ( W1 = W2 implies v + W1 = v + W2 ) proof assume A1: v + W1 = v + W2 ; ::_thesis: W1 = W2 the carrier of W1 = the carrier of W2 proof A2: the carrier of W1 c= the carrier of V by Def2; thus the carrier of W1 c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of W1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 ) assume A3: x in the carrier of W1 ; ::_thesis: x in the carrier of W2 then reconsider y = x as Element of V by A2; set z = v + y; x in W1 by A3, STRUCT_0:def_5; then v + y in v + W2 by A1; then consider u being Vector of V such that A4: v + y = v + u and A5: u in W2 ; y = u by A4, RLVECT_1:8; hence x in the carrier of W2 by A5, 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 ) assume A6: x in the carrier of W2 ; ::_thesis: x in the carrier of W1 the carrier of W2 c= the carrier of V by Def2; then reconsider y = x as Element of V by A6; set z = v + y; x in W2 by A6, STRUCT_0:def_5; then v + y in v + W1 by A1; then consider u being Vector of V such that A7: v + y = v + u and A8: u in W1 ; y = u by A7, RLVECT_1:8; hence x in the carrier of W1 by A8, STRUCT_0:def_5; ::_thesis: verum end; hence W1 = W2 by Th29; ::_thesis: verum end; thus ( W1 = W2 implies v + W1 = v + W2 ) ; ::_thesis: verum end; theorem Th64: :: RMOD_2:64 for R being Ring for V being RightMod of R for v, u being Vector of V for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2 proof let R be Ring; ::_thesis: for V being RightMod of R for v, u being Vector of V for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2 let V be RightMod of R; ::_thesis: for v, u being Vector of V for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2 let v, u be Vector of V; ::_thesis: for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2 let W1, W2 be strict Submodule of V; ::_thesis: ( v + W1 = u + W2 implies W1 = W2 ) assume A1: v + W1 = u + W2 ; ::_thesis: W1 = W2 set V2 = the carrier of W2; set V1 = the carrier of W1; assume A2: W1 <> W2 ; ::_thesis: contradiction A3: now__::_thesis:_not_the_carrier_of_W1_\_the_carrier_of_W2_<>_{} set x = the Element of the carrier of W1 \ the carrier of W2; assume the carrier of W1 \ the carrier of W2 <> {} ; ::_thesis: contradiction then the Element of the carrier of W1 \ the carrier of W2 in the carrier of W1 by XBOOLE_0:def_5; then A4: the Element of the carrier of W1 \ the carrier of W2 in W1 by STRUCT_0:def_5; then the Element of the carrier of W1 \ the carrier of W2 in V by Th9; then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V by STRUCT_0:def_5; set z = v + x; v + x in u + W2 by A1, A4; then consider u1 being Vector of V such that A5: v + x = u + u1 and A6: u1 in W2 ; x = (0. V) + x by RLVECT_1:def_4 .= (v + (- v)) + x by VECTSP_1:19 .= (- v) + (u + u1) by A5, RLVECT_1:def_3 ; then A7: (v + ((- v) + (u + u1))) + W1 = v + W1 by A4, Th51; v + ((- v) + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def_3 .= (0. V) + (u + u1) by VECTSP_1:19 .= u + u1 by RLVECT_1:def_4 ; then (u + u1) + W2 = (u + u1) + W1 by A1, A6, A7, Th51; hence contradiction by A2, Th63; ::_thesis: verum end; A8: now__::_thesis:_not_the_carrier_of_W2_\_the_carrier_of_W1_<>_{} set x = the Element of the carrier of W2 \ the carrier of W1; assume the carrier of W2 \ the carrier of W1 <> {} ; ::_thesis: contradiction then the Element of the carrier of W2 \ the carrier of W1 in the carrier of W2 by XBOOLE_0:def_5; then A9: the Element of the carrier of W2 \ the carrier of W1 in W2 by STRUCT_0:def_5; then the Element of the carrier of W2 \ the carrier of W1 in V by Th9; then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V by STRUCT_0:def_5; set z = u + x; u + x in v + W1 by A1, A9; then consider u1 being Vector of V such that A10: u + x = v + u1 and A11: u1 in W1 ; x = (0. V) + x by RLVECT_1:def_4 .= (u + (- u)) + x by VECTSP_1:19 .= (- u) + (v + u1) by A10, RLVECT_1:def_3 ; then A12: (u + ((- u) + (v + u1))) + W2 = u + W2 by A9, Th51; u + ((- u) + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def_3 .= (0. V) + (v + u1) by VECTSP_1:19 .= v + u1 by RLVECT_1:def_4 ; then (v + u1) + W1 = (v + u1) + W2 by A1, A11, A12, Th51; hence contradiction by A2, Th63; ::_thesis: verum end; the carrier of W1 <> the carrier of W2 by A2, Th29; then ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) by XBOOLE_0:def_10; hence contradiction by A3, A8, XBOOLE_1:37; ::_thesis: verum end; theorem :: RMOD_2:65 for R being Ring for V being RightMod of R for v being Vector of V for W being Submodule of V ex C being Coset of W st v in C proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V for W being Submodule of V ex C being Coset of W st v in C let V be RightMod of R; ::_thesis: for v being Vector of V for W being Submodule of V ex C being Coset of W st v in C let v be Vector of V; ::_thesis: for W being Submodule of V ex C being Coset of W st v in C let W be Submodule of V; ::_thesis: ex C being Coset of W st v in C reconsider C = v + W as Coset of W by Def6; take C ; ::_thesis: v in C thus v in C by Th44; ::_thesis: verum end; theorem :: RMOD_2:66 for R being Ring for V being RightMod of R for W being Submodule of V for C being Coset of W holds ( C is linearly-closed iff C = the carrier of W ) proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V for C being Coset of W holds ( C is linearly-closed iff C = the carrier of W ) let V be RightMod of R; ::_thesis: for W being Submodule of V for C being Coset of W holds ( C is linearly-closed iff C = the carrier of W ) let W be Submodule of V; ::_thesis: for C being Coset of W holds ( C is linearly-closed iff C = the carrier of W ) let C be Coset of W; ::_thesis: ( C is linearly-closed iff C = the carrier of W ) thus ( C is linearly-closed implies C = the carrier of W ) ::_thesis: ( C = the carrier of W implies C is linearly-closed ) proof assume A1: C is linearly-closed ; ::_thesis: C = the carrier of W consider v being Vector of V such that A2: C = v + W by Def6; C <> {} by A2, Th44; then 0. V in v + W by A1, A2, Th1; hence C = the carrier of W by A2, Th48; ::_thesis: verum end; thus ( C = the carrier of W implies C is linearly-closed ) by Lm1; ::_thesis: verum end; theorem :: RMOD_2:67 for R being Ring for V being RightMod of R for W1, W2 being strict Submodule of V for C1 being Coset of W1 for C2 being Coset of W2 st C1 = C2 holds W1 = W2 proof let R be Ring; ::_thesis: for V being RightMod of R for W1, W2 being strict Submodule of V for C1 being Coset of W1 for C2 being Coset of W2 st C1 = C2 holds W1 = W2 let V be RightMod of R; ::_thesis: for W1, W2 being strict Submodule of V for C1 being Coset of W1 for C2 being Coset of W2 st C1 = C2 holds W1 = W2 let W1, W2 be strict Submodule of V; ::_thesis: for C1 being Coset of W1 for C2 being Coset of W2 st C1 = C2 holds W1 = W2 let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 = C2 holds W1 = W2 let C2 be Coset of W2; ::_thesis: ( C1 = C2 implies W1 = W2 ) ( ex v1 being Vector of V st C1 = v1 + W1 & ex v2 being Vector of V st C2 = v2 + W2 ) by Def6; hence ( C1 = C2 implies W1 = W2 ) by Th64; ::_thesis: verum end; theorem :: RMOD_2:68 for R being Ring for V being RightMod of R for v being Vector of V holds {v} is Coset of (0). V proof let R be Ring; ::_thesis: for V being RightMod of R for v being Vector of V holds {v} is Coset of (0). V let V be RightMod of R; ::_thesis: for v being Vector of V holds {v} is Coset of (0). V let v be Vector of V; ::_thesis: {v} is Coset of (0). V v + ((0). V) = {v} by Th46; hence {v} is Coset of (0). V by Def6; ::_thesis: verum end; theorem :: RMOD_2:69 for R being Ring for V being RightMod of R for V1 being Subset of V st V1 is Coset of (0). V holds ex v being Vector of V st V1 = {v} proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st V1 is Coset of (0). V holds ex v being Vector of V st V1 = {v} let V be RightMod of R; ::_thesis: for V1 being Subset of V st V1 is Coset of (0). V holds ex v being Vector of V st V1 = {v} let V1 be Subset of V; ::_thesis: ( V1 is Coset of (0). V implies ex v being Vector of V st V1 = {v} ) assume V1 is Coset of (0). V ; ::_thesis: ex v being Vector of V st V1 = {v} then consider v being Vector of V such that A1: V1 = v + ((0). V) by Def6; take v ; ::_thesis: V1 = {v} thus V1 = {v} by A1, Th46; ::_thesis: verum end; theorem :: RMOD_2:70 for R being Ring for V being RightMod of R for W being Submodule of V holds the carrier of W is Coset of W proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V holds the carrier of W is Coset of W let V be RightMod of R; ::_thesis: for W being Submodule of V holds the carrier of W is Coset of W let W be Submodule of V; ::_thesis: the carrier of W is Coset of W the carrier of W = (0. V) + W by Lm2; hence the carrier of W is Coset of W by Def6; ::_thesis: verum end; theorem :: RMOD_2:71 for R being Ring for V being RightMod of R holds the carrier of V is Coset of (Omega). V proof let R be Ring; ::_thesis: for V being RightMod of R holds the carrier of V is Coset of (Omega). V let V be RightMod of R; ::_thesis: the carrier of V is Coset of (Omega). V set v = the Vector of V; the carrier of V c= the carrier of V ; then reconsider A = the carrier of V as Subset of V ; A = the Vector of V + ((Omega). V) by Th47; hence the carrier of V is Coset of (Omega). V by Def6; ::_thesis: verum end; theorem :: RMOD_2:72 for R being Ring for V being RightMod of R for V1 being Subset of V st V1 is Coset of (Omega). V holds V1 = the carrier of V proof let R be Ring; ::_thesis: for V being RightMod of R for V1 being Subset of V st V1 is Coset of (Omega). V holds V1 = the carrier of V let V be RightMod of R; ::_thesis: for V1 being Subset of V st V1 is Coset of (Omega). V holds V1 = the carrier of V let V1 be Subset of V; ::_thesis: ( V1 is Coset of (Omega). V implies V1 = the carrier of V ) assume V1 is Coset of (Omega). V ; ::_thesis: V1 = the carrier of V then ex v being Vector of V st V1 = v + ((Omega). V) by Def6; hence V1 = the carrier of V by Th47; ::_thesis: verum end; theorem :: RMOD_2:73 for R being Ring for V being RightMod of R for W being Submodule of V for C being Coset of W holds ( 0. V in C iff C = the carrier of W ) proof let R be Ring; ::_thesis: for V being RightMod of R for W being Submodule of V for C being Coset of W holds ( 0. V in C iff C = the carrier of W ) let V be RightMod of R; ::_thesis: for W being Submodule of V for C being Coset of W holds ( 0. V in C iff C = the carrier of W ) let W be Submodule of V; ::_thesis: for C being Coset of W holds ( 0. V in C iff C = the carrier of W ) let C be Coset of W; ::_thesis: ( 0. V in C iff C = the carrier of W ) ex v being Vector of V st C = v + W by Def6; hence ( 0. V in C iff C = the carrier of W ) by Th48; ::_thesis: verum end; theorem Th74: :: RMOD_2:74 for R being Ring for V being RightMod of R for u being Vector of V for W being Submodule of V for C being Coset of W holds ( u in C iff C = u + W ) proof let R be Ring; ::_thesis: for V being RightMod of R for u being Vector of V for W being Submodule of V for C being Coset of W holds ( u in C iff C = u + W ) let V be RightMod of R; ::_thesis: for u being Vector of V for W being Submodule of V for C being Coset of W holds ( u in C iff C = u + W ) let u be Vector of V; ::_thesis: for W being Submodule of V for C being Coset of W holds ( u in C iff C = u + W ) let W be Submodule of V; ::_thesis: for C being Coset of W holds ( u in C iff C = u + W ) let C be Coset of W; ::_thesis: ( u in C iff C = u + W ) thus ( u in C implies C = u + W ) ::_thesis: ( C = u + W implies u in C ) proof assume A1: u in C ; ::_thesis: C = u + W ex v being Vector of V st C = v + W by Def6; hence C = u + W by A1, Th53; ::_thesis: verum end; thus ( C = u + W implies u in C ) by Th44; ::_thesis: verum end; theorem :: RMOD_2:75 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u + v1 = v ) proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u + v1 = v ) let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u + v1 = v ) let u, v be Vector of V; ::_thesis: for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u + v1 = v ) let W be Submodule of V; ::_thesis: for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u + v1 = v ) let C be Coset of W; ::_thesis: ( u in C & v in C implies ex v1 being Vector of V st ( v1 in W & u + v1 = v ) ) assume ( u in C & v in C ) ; ::_thesis: ex v1 being Vector of V st ( v1 in W & u + v1 = v ) then ( C = u + W & C = v + W ) by Th74; hence ex v1 being Vector of V st ( v1 in W & u + v1 = v ) by Th61; ::_thesis: verum end; theorem :: RMOD_2:76 for R being Ring for V being RightMod of R for u, v being Vector of V for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u - v1 = v ) proof let R be Ring; ::_thesis: for V being RightMod of R for u, v being Vector of V for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u - v1 = v ) let V be RightMod of R; ::_thesis: for u, v being Vector of V for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u - v1 = v ) let u, v be Vector of V; ::_thesis: for W being Submodule of V for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u - v1 = v ) let W be Submodule of V; ::_thesis: for C being Coset of W st u in C & v in C holds ex v1 being Vector of V st ( v1 in W & u - v1 = v ) let C be Coset of W; ::_thesis: ( u in C & v in C implies ex v1 being Vector of V st ( v1 in W & u - v1 = v ) ) assume ( u in C & v in C ) ; ::_thesis: ex v1 being Vector of V st ( v1 in W & u - v1 = v ) then ( C = u + W & C = v + W ) by Th74; hence ex v1 being Vector of V st ( v1 in W & u - v1 = v ) by Th62; ::_thesis: verum end; theorem :: RMOD_2:77 for R being Ring for V being RightMod of R for v1, v2 being Vector of V for W being Submodule of V holds ( ex C being Coset of W st ( v1 in C & v2 in C ) iff v1 - v2 in W ) proof let R be Ring; ::_thesis: for V being RightMod of R for v1, v2 being Vector of V for W being Submodule of V holds ( ex C being Coset of W st ( v1 in C & v2 in C ) iff v1 - v2 in W ) let V be RightMod of R; ::_thesis: for v1, v2 being Vector of V for W being Submodule of V holds ( ex C being Coset of W st ( v1 in C & v2 in C ) iff v1 - v2 in W ) let v1, v2 be Vector of V; ::_thesis: for W being Submodule of V holds ( ex C being Coset of W st ( v1 in C & v2 in C ) iff v1 - v2 in W ) let W be Submodule of V; ::_thesis: ( ex C being Coset of W st ( v1 in C & v2 in C ) iff v1 - v2 in W ) thus ( ex C being Coset of W st ( v1 in C & v2 in C ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex C being Coset of W st ( v1 in C & v2 in C ) ) proof given C being Coset of W such that A1: ( v1 in C & v2 in C ) ; ::_thesis: v1 - v2 in W ex v being Vector of V st C = v + W by Def6; hence v1 - v2 in W by A1, Th60; ::_thesis: verum end; assume v1 - v2 in W ; ::_thesis: ex C being Coset of W st ( v1 in C & v2 in C ) then consider v being Vector of V such that A2: ( v1 in v + W & v2 in v + W ) by Th60; reconsider C = v + W as Coset of W by Def6; take C ; ::_thesis: ( v1 in C & v2 in C ) thus ( v1 in C & v2 in C ) by A2; ::_thesis: verum end; theorem :: RMOD_2:78 for R being Ring for V being RightMod of R for u being Vector of V for W being Submodule of V for B, C being Coset of W st u in B & u in C holds B = C proof let R be Ring; ::_thesis: for V being RightMod of R for u being Vector of V for W being Submodule of V for B, C being Coset of W st u in B & u in C holds B = C let V be RightMod of R; ::_thesis: for u being Vector of V for W being Submodule of V for B, C being Coset of W st u in B & u in C holds B = C let u be Vector of V; ::_thesis: for W being Submodule of V for B, C being Coset of W st u in B & u in C holds B = C let W be Submodule of V; ::_thesis: for B, C being Coset of W st u in B & u in C holds B = C let B, C be Coset of W; ::_thesis: ( u in B & u in C implies B = C ) assume A1: ( u in B & u in C ) ; ::_thesis: B = C ( ex v1 being Vector of V st B = v1 + W & ex v2 being Vector of V st C = v2 + W ) by Def6; hence B = C by A1, Th54; ::_thesis: verum end;