let V be RealLinearSpace; :: thesis: for u, v, x, y being VECTOR of V st Gen x,y holds
u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y
let u, v, x, y be VECTOR of V; :: thesis: ( Gen x,y implies u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y )
assume A1: Gen x,y ; :: thesis: u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y
set w = (Orte (x,y,v)) - (Orte (x,y,u));
A2: (Orte (x,y,v)) - (Orte (x,y,u)) = Orte (x,y,(v - u)) by A1, Th11
.= ((pr2 (x,y,(v - u))) * x) + ((- (pr1 (x,y,(v - u)))) * y) ;
PProJ (x,y,(v - u),((Orte (x,y,v)) - (Orte (x,y,u)))) = ((pr1 (x,y,(v - u))) * (pr1 (x,y,((Orte (x,y,v)) - (Orte (x,y,u)))))) + ((pr2 (x,y,(v - u))) * (pr2 (x,y,((Orte (x,y,v)) - (Orte (x,y,u)))))) by GEOMTRAP:def 6
.= ((pr1 (x,y,(v - u))) * (pr2 (x,y,(v - u)))) + ((pr2 (x,y,(v - u))) * (pr2 (x,y,((Orte (x,y,v)) - (Orte (x,y,u)))))) by A1, A2, Lm6
.= ((pr1 (x,y,(v - u))) * (pr2 (x,y,(v - u)))) + ((- (pr1 (x,y,(v - u)))) * (pr2 (x,y,(v - u)))) by A1, A2, Lm6
.= 0 ;
then v - u,(Orte (x,y,v)) - (Orte (x,y,u)) are_Ort_wrt x,y by A1, GEOMTRAP:32;
hence u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y by ANALMETR:def 3; :: thesis: verum