let V be RealLinearSpace; :: thesis: for x, y, u being VECTOR of V st Gen x,y holds
Orte x,y,(Orte x,y,u) = - u
let x, y, u be VECTOR of V; :: thesis: ( Gen x,y implies Orte x,y,(Orte x,y,u) = - u )
assume A1: Gen x,y ; :: thesis: Orte x,y,(Orte x,y,u) = - u
hence Orte x,y,(Orte x,y,u) = ((- (pr1 x,y,u)) * x) + ((- (pr1 x,y,(((pr2 x,y,u) * x) + ((- (pr1 x,y,u)) * y)))) * y) by GEOMTRAP:def 5
.= ((- (pr1 x,y,u)) * x) + ((- (pr2 x,y,u)) * y) by A1, GEOMTRAP:def 4
.= ((pr1 x,y,u) * (- x)) + ((- (pr2 x,y,u)) * y) by RLVECT_1:38
.= (- ((pr1 x,y,u) * x)) + ((- (pr2 x,y,u)) * y) by RLVECT_1:39
.= (- ((pr1 x,y,u) * x)) + ((pr2 x,y,u) * (- y)) by RLVECT_1:38
.= (- ((pr1 x,y,u) * x)) + (- ((pr2 x,y,u) * y)) by RLVECT_1:39
.= - (((pr1 x,y,u) * x) + ((pr2 x,y,u) * y)) by RLVECT_1:45
.= - u by A1, Lm5 ;
:: thesis: verum