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 u, v being Element of V

for W being Subspace of V holds

( u in W iff v + W = (v + u) + 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 u, v being Element of V

for W being Subspace of V holds

( u in W iff v + W = (v + u) + W )

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

( u in W iff v + W = (v + u) + W )

let W be Subspace 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 )

( 0. V in W & v + (0. V) = v ) by Th17, RLVECT_1:4;

then v in (v + u) + W by A8;

then consider u1 being Element 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

for u, v being Element of V

for W being Subspace of V holds

( u in W iff v + W = (v + u) + 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 u, v being Element of V

for W being Subspace of V holds

( u in W iff v + W = (v + u) + W )

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

( u in W iff v + W = (v + u) + W )

let W be Subspace 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 A8:
v + W = (v + u) + W
; :: thesis: u in W
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

assume x in (v + u) + W ; :: thesis: x in v + W

then consider v2 being Element 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;thus v + W c= (v + u) + W :: according to XBOOLE_0:def 10 :: thesis: (v + u) + W c= v + W

proof

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

v1 - u in W by A1, A3, Th23;

hence x in (v + u) + W by A4; :: thesis: verum

end;assume x in v + W ; :: thesis: x in (v + u) + W

then consider v1 being Element 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:4 ;

v1 - u in W by A1, A3, Th23;

hence x in (v + u) + W by A4; :: thesis: verum

assume x in (v + u) + W ; :: thesis: x in v + W

then consider v2 being Element 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

( 0. V in W & v + (0. V) = v ) by Th17, RLVECT_1:4;

then v in (v + u) + W by A8;

then consider u1 being Element 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