let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for X being Subspace of V st not v in X holds
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let v be VECTOR of V; :: thesis: for X being Subspace of V st not v in X holds
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let X be Subspace of V; :: thesis: ( not v in X implies for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume A1: not v in X ; :: thesis: for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let y be VECTOR of (X + (Lin {v})); :: thesis: for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & W = X implies X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume that
A2: v = y and
A3: W = X ; :: thesis: X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
Lin {v} = Lin {y} by A2, Th10;
hence RLSStruct(# the carrier of (X + (Lin {v})), the ZeroF of (X + (Lin {v})), the addF of (X + (Lin {v})), the Mult of (X + (Lin {v})) #) = W + (Lin {y}) by A3, Th9; :: according to RLSUB_2:def 4 :: thesis: W /\ (Lin {y}) = (0). (X + (Lin {v}))
assume W /\ (Lin {y}) <> (0). (X + (Lin {v})) ; :: thesis: contradiction
then consider z being VECTOR of (X + (Lin {v})) such that
A4: ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( z in (0). (X + (Lin {v})) & not z in W /\ (Lin {y}) ) ) by RLSUB_1:31;
per cases ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( not z in W /\ (Lin {y}) & z in (0). (X + (Lin {v})) ) ) by A4;
suppose that A5: z in W /\ (Lin {y}) and
A6: not z in (0). (X + (Lin {v})) ; :: thesis: contradiction
z in Lin {y} by A5, RLSUB_2:3;
then consider a being Real such that
A7: z = a * y by RLVECT_4:8;
A8: z in W by A5, RLSUB_2:3;
now :: thesis: contradiction
per cases ( a = 0 or a <> 0 ) ;
suppose A9: a <> 0 ; :: thesis: contradiction
y = 1 * y by RLVECT_1:def 8
.= ((a ") * a) * y by A9, XCMPLX_0:def 7
.= (a ") * (a * y) by RLVECT_1:def 7 ;
hence contradiction by A1, A2, A3, A8, A7, RLSUB_1:21; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose that A10: not z in W /\ (Lin {y}) and
A11: z in (0). (X + (Lin {v})) ; :: thesis: contradiction
z = 0. (X + (Lin {v})) by A11, RLVECT_3:29;
hence contradiction by A10, RLSUB_1:17; :: thesis: verum
end;
end;