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