let V be RealLinearSpace; :: thesis: for w, y, u, v being VECTOR of V
for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
let w, y, u, v be VECTOR of V; :: thesis: for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
let a, b be Real; :: thesis: ( Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) implies ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) ) )
assume that
A1: Gen w,y and
A2: ( 0. V <> u & 0. V <> v ) and
A3: u,v are_Ort_wrt w,y and
A4: u = (a * w) + (b * y) ; :: thesis: ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
set v' = (b * w) + ((- a) * y);
(b * w) + ((- a) * y) = ((1 * b) * w) + ((- (1 * a)) * y) ;
then u,(b * w) + ((- a) * y) are_Ort_wrt w,y by A1, A4, Lm5;
then consider a1, b1 being Real such that
A5: a1 * v = b1 * ((b * w) + ((- a) * y)) and
A6: ( a1 <> 0 or b1 <> 0 ) by A1, A2, A3, ANALMETR:13;

A7: now

assume A8: b1 = 0 ; :: thesis: contradiction
then 0. V = a1 * v by A5, RLVECT_1:23;
hence contradiction by A2, A6, A8, RLVECT_1:24; :: thesis: verum

end;

A9: now

assume A10: a1 = 0 ; :: thesis: contradiction
then 0. V = b1 * ((b * w) + ((- a) * y)) by A5, RLVECT_1:23;
then (b * w) + ((- a) * y) = 0. V by A6, A10, RLVECT_1:24;
then ( b = 0 & - a = 0 ) by A1, ANALMETR:def 1;
then u = (0. V) + (0 * y) by A4, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
hence contradiction by A2; :: thesis: verum

end;

take c = (a1 " ) * b1; :: thesis: ( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )

now

assume c = 0 ; :: thesis: contradiction
then a1 " = 0 by A7, XCMPLX_1:6;
hence contradiction by A9, XCMPLX_1:203; :: thesis: verum

end;

hence c <> 0 ; :: thesis: v = ((c * b) * w) + ((- (c * a)) * y)
thus v = (a1 " ) * (b1 * ((b * w) + ((- a) * y))) by A5, A9, ANALOAF:12
.= c * ((b * w) + ((- a) * y)) by RLVECT_1:def 9
.= (c * (b * w)) + (c * ((- a) * y)) by RLVECT_1:def 9
.= ((c * b) * w) + (c * ((- a) * y)) by RLVECT_1:def 9
.= ((c * b) * w) + ((c * (- a)) * y) by RLVECT_1:def 9
.= ((c * b) * w) + ((- (c * a)) * y) ; :: thesis: verum