let V be RealLinearSpace; :: thesis: for v, w being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds
ex a being Real st v = a * w
let v, w be VECTOR of V; :: thesis: ( w <> 0. V & {v,w} is linearly-dependent implies ex a being Real st v = a * w )
assume that
A1: w <> 0. V and
A2: {v,w} is linearly-dependent ; :: thesis: ex a being Real st v = a * w
consider a, b being Real such that
A3: (a * v) + (b * w) = 0. V and
A4: ( a <> 0 or b <> 0 ) by A2, RLVECT_3:13;
A5: a * v = - (b * w) by A3, RLVECT_1:6;
now :: thesis: ex a being Real st v = a * w
per cases ( a <> 0 or a = 0 ) ;
suppose A6: a <> 0 ; :: thesis: ex a being Real st v = a * w
((a ") * a) * v = (a ") * (- (b * w)) by A5, RLVECT_1:def 7;
then 1 * v = (a ") * (- (b * w)) by A6, XCMPLX_0:def 7;
then v = (a ") * (- (b * w)) by RLVECT_1:def 8
.= (a ") * ((- b) * w) by Th3
.= ((a ") * (- b)) * w by RLVECT_1:def 7 ;
hence ex a being Real st v = a * w ; :: thesis: verum
end;
suppose A7: a = 0 ; :: thesis: ex a being Real st v = a * w
then 0. V = - (b * w) by A5, RLVECT_1:10;
then A8: 0. V = (- b) * w by Th3;
- b <> 0 by A4, A7;
hence ex a being Real st v = a * w by A1, A8, RLVECT_1:11; :: thesis: verum
end;
end;
end;
hence ex a being Real st v = a * w ; :: thesis: verum