let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V

for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

let v be Element of V; :: thesis: for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

let W be Subspace 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:4;

then A1: v in { (v + u) where u is Element 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 )

assume not v in W ; :: thesis: contradiction

hence contradiction by A7, A1; :: thesis: verum

for v being Element of V

for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V

for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

let v be Element of V; :: thesis: for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

let W be Subspace 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:4;

then A1: v in { (v + u) where u is Element 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 A7:
v + W = the carrier of W
; :: thesis: v in W
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

assume x in the carrier of W ; :: thesis: x in v + W

then reconsider y = x, z = v as Element of W by A2;

reconsider y1 = y, z1 = z as Element 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:4 ;

y - z in W ;

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;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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W or x in v + W )
let x be object ; :: 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 Element 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; :: thesis: verum

end;assume x in v + W ; :: thesis: x in the carrier of W

then consider u being Element 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; :: thesis: verum

assume x in the carrier of W ; :: thesis: x in v + W

then reconsider y = x, z = v as Element of W by A2;

reconsider y1 = y, z1 = z as Element 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:4 ;

y - z in W ;

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

assume not v in W ; :: thesis: contradiction

hence contradiction by A7, A1; :: thesis: verum