let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
let v be VECTOR of V; :: thesis: for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
let W be Subspace of V; :: thesis: ( v + W = (- v) + W iff v in W )
thus ( v + W = (- v) + W implies v in W ) :: thesis: ( v in W implies v + W = (- v) + W )
proof
assume v + W = (- v) + W ; :: thesis: v in W
then v in (- v) + W by Th62;
then consider u being VECTOR of V such that
A1: v = (- v) + u and
A2: u in W ;
0. V = v - ((- v) + u) by A1, RLVECT_1:15
.= (v - (- v)) - u by RLVECT_1:27
.= (v + v) - u by RLVECT_1:17
.= ((1r * v) + v) - u by Def5
.= ((1r * v) + (1r * v)) - u by Def5
.= ((1r + 1r) * v) - u by Def3 ;
then ((1r + 1r) ") * ((1r + 1r) * v) = ((1r + 1r) ") * u by RLVECT_1:21;
then (((1r + 1r) ") * (1r + 1r)) * v = ((1r + 1r) ") * u by Def4;
then v = ((1r + 1r) ") * u by Def5;
hence v in W by A2, Th40; :: thesis: verum
end;
assume A3: v in W ; :: thesis: v + W = (- v) + W
then v + W = the carrier of W by Lm6;
hence v + W = (- v) + W by A3, Th70; :: thesis: verum