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 )
thus ( v in W implies v + W = the carrier of W ) :: thesis: ( v + W = the carrier of W implies v in W )

proof

assume A1: 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
A2: x = v + u and
A3: u in W ;
v + u in W by A1, A3, Th28;
hence x in the carrier of W by A2, 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 A1, STRUCT_0:def 5;
reconsider y1 = y, z1 = z as Vector of V by Th18;
A4: y - z in W by STRUCT_0:def 5;
A5: z + (y - z) = y + (z + (- z)) by RLVECT_1:def 6
.= y + (0. W) by VECTSP_1:66
.= x by RLVECT_1:def 7 ;
A6: y - z = y1 - z1 by Th24;
A7: y1 - z1 in W by A4, Th24;
z1 + (y1 - z1) = x by A5, A6, Th21;
hence x in v + W by A7; :: thesis: verum

end;

assume A8: v + W = the carrier of W ; :: thesis: v in W
assume A9: not v in W ; :: thesis: contradiction
( 0. V in W & v + (0. V) = v ) by Th25, RLVECT_1:def 7;
then v in { (v + u) where u is Vector of V : u in W } ;
hence contradiction by A8, A9, STRUCT_0:def 5; :: thesis: verum