let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u,v are_Ort_wrt w,y iff PProJ w,y,u,v = 0 )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v being VECTOR of V holds
( u,v are_Ort_wrt w,y iff PProJ w,y,u,v = 0 ) )
assume A1: Gen w,y ; :: thesis: for u, v being VECTOR of V holds
( u,v are_Ort_wrt w,y iff PProJ w,y,u,v = 0 )
let u, v be VECTOR of V; :: thesis: ( u,v are_Ort_wrt w,y iff PProJ w,y,u,v = 0 )
set a1 = pr1 w,y,u;
set a2 = pr2 w,y,u;
set b1 = pr1 w,y,v;
set b2 = pr2 w,y,v;
( u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y) & v = ((pr1 w,y,v) * w) + ((pr2 w,y,v) * y) ) by A1, Lm15;
hence ( u,v are_Ort_wrt w,y iff PProJ w,y,u,v = 0 ) by A1, ANALMETR:5, ANALMETR:def 2; :: thesis: verum