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