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 and
A3: 0. V <> v and
A4: u,v are_Ort_wrt w,y and
A5: u = (a * w) + (b * y) ; :: thesis: ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
set v9 = (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, A5, Lm5;
then consider a1, b1 being Real such that
A6: a1 * v = b1 * ((b * w) + ((- a) * y)) and
A7: ( a1 <> 0 or b1 <> 0 ) by A1, A2, A4, ANALMETR:9;
A8: now :: thesis: not a1 = 0
assume A9: a1 = 0 ; :: thesis: contradiction
then 0. V = b1 * ((b * w) + ((- a) * y)) by A6, RLVECT_1:10;
then (b * w) + ((- a) * y) = 0. V by A7, A9, RLVECT_1:11;
then ( b = 0 & - a = 0 ) by A1, ANALMETR:def 1;
then u = (0. V) + (0 * y) by A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A2; :: thesis: verum
end;
take c = (a1 ") * b1; :: thesis: ( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
A10: now :: thesis: not b1 = 0
assume A11: b1 = 0 ; :: thesis: contradiction
then 0. V = a1 * v by A6, RLVECT_1:10;
hence contradiction by A3, A7, A11, RLVECT_1:11; :: thesis: verum
end;
now :: thesis: not c = 0
assume c = 0 ; :: thesis: contradiction
then a1 " = 0 by A10, XCMPLX_1:6;
hence contradiction by A8, XCMPLX_1:202; :: thesis: verum
end;
hence c <> 0 ; :: thesis: v = ((c * b) * w) + ((- (c * a)) * y)
thus v = (a1 ") * (b1 * ((b * w) + ((- a) * y))) by A6, A8, ANALOAF:5
.= c * ((b * w) + ((- a) * y)) by RLVECT_1:def 7
.= (c * (b * w)) + (c * ((- a) * y)) by RLVECT_1:def 5
.= ((c * b) * w) + (c * ((- a) * y)) by RLVECT_1:def 7
.= ((c * b) * w) + ((c * (- a)) * y) by RLVECT_1:def 7
.= ((c * b) * w) + ((- (c * a)) * y) ; :: thesis: verum