let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st Gen w,y & u <> 0. V holds
ex a being Real st v - (a * u),u are_Ort_wrt w,y
let u, v, w, y be VECTOR of V; :: thesis: ( Gen w,y & u <> 0. V implies ex a being Real st v - (a * u),u are_Ort_wrt w,y )
assume that
A1: Gen w,y and
A2: u <> 0. V ; :: thesis: ex a being Real st v - (a * u),u are_Ort_wrt w,y
consider a1, a2 being Real such that
A3: u = (a1 * w) + (a2 * y) by A1;
consider b1, b2 being Real such that
A4: v = (b1 * w) + (b2 * y) by A1;
set a = ((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ");
(((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u = (((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1) * w) + (((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2) * y) by A3, Lm3;
then A5: v - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u) = ((b1 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) * w) + ((b2 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)) * y) by A4, Lm1;
A6: ((b1 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) * a1) + ((b2 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)) * a2) = ((a1 * b1) + (a2 * b2)) + ((- 1) * ((a1 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) + (a2 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)))) ;
A7: (a1 * a1) + (a2 * a2) <> 0 by A1, A2, Th11, A3, Def2;
(- 1) * ((a1 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) + (a2 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2))) = (- 1) * (((b1 * a1) + (b2 * a2)) * ((((a1 * a1) + (a2 * a2)) ") * ((a1 * a1) + (a2 * a2))))
.= (- 1) * (((b1 * a1) + (b2 * a2)) * 1) by A7, XCMPLX_0:def 7
.= - ((a1 * b1) + (a2 * b2)) ;
then v - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u),u are_Ort_wrt w,y by A3, A5, A6;
hence ex a being Real st v - (a * u),u are_Ort_wrt w,y ; :: thesis: verum