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;
consider c being Real such that
c <> 0 and
A5: v = ((c * a2) * w) + ((- (c * a1)) * y) by A1, A2, A3, A4, Th18;
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:32
.= ((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:32
.= (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:32
.= (- (PProJ w,y,u,(((c * b) * w) + ((- (c * a)) * y)))) - ((PProJ w,y,((a * w) + (b * y)),v) - 0 ) by A1, A3, GEOMTRAP:34
.= (- 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:34; :: thesis: verum