let V be RealLinearSpace; :: thesis: for w, y, u, v being VECTOR of V st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y holds
ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
let w, y, u, v be VECTOR of V; :: thesis: ( Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y implies ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y ) )
assume that
A1: Gen w,y and
A2: ( 0. V <> u & 0. V <> v ) and
A3: u,v are_Ort_wrt w,y ; :: thesis: ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
consider a1, a2 being Real such that
A4: u = (a1 * w) + (a2 * y) by A1, ANALMETR:def 1;
reconsider a1 = a1, a2 = a2 as Real ;
consider c being Real such that
c <> 0 and
A5: v = ((c * a2) * w) + ((- (c * a1)) * y) by A1, A2, A3, A4, Th18;
reconsider c = c as Real ;
take c ; :: thesis: for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
let a, b be Real; :: thesis: ( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
set u9 = (a * w) + (b * y);
set v9 = ((c * b) * w) + ((- (c * a)) * y);
A6: ( pr1 (w,y,((a * w) + (b * y))) = a & pr2 (w,y,((a * w) + (b * y))) = b ) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;
A7: ( pr1 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = c * b & pr2 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = - (c * a) ) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;
( pr1 (w,y,u) = a1 & pr2 (w,y,u) = a2 ) by A1, A4, GEOMTRAP:def 4, GEOMTRAP:def 5;
then A8: PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))) = (a1 * (c * b)) + (a2 * (- (c * a))) by A7, GEOMTRAP:def 6;
( pr1 (w,y,v) = c * a2 & pr2 (w,y,v) = - (c * a1) ) by A1, A5, GEOMTRAP:def 4, GEOMTRAP:def 5;
then A9: PProJ (w,y,((a * w) + (b * y)),v) = ((c * a2) * a) + ((- (c * a1)) * b) by A6, GEOMTRAP:def 6;
thus (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y by A1, Lm5; :: thesis: ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y
PProJ (w,y,(((a * w) + (b * y)) - u),((((c * b) * w) + ((- (c * a)) * y)) - v)) = (PProJ (w,y,(((a * w) + (b * y)) - u),(((c * b) * w) + ((- (c * a)) * y)))) - (PProJ (w,y,(((a * w) + (b * y)) - u),v)) by A1, GEOMTRAP:30
.= ((PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y)))) - (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - (PProJ (w,y,(((a * w) + (b * y)) - u),v)) by A1, GEOMTRAP:30
.= (0 - (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - (PProJ (w,y,(((a * w) + (b * y)) - u),v)) by A1, Lm5
.= (- (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - ((PProJ (w,y,((a * w) + (b * y)),v)) - (PProJ (w,y,u,v))) by A1, GEOMTRAP:30
.= (- (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - ((PProJ (w,y,((a * w) + (b * y)),v)) - 0) by A1, A3, GEOMTRAP:32
.= (- 1) * ((PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y)))) + (PProJ (w,y,((a * w) + (b * y)),v))) ;
hence ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y by A1, A8, A9, GEOMTRAP:32; :: thesis: verum