let V be RealLinearSpace; for u, x, y being VECTOR of V st Gen x,y holds
Orte (x,y,(Orte (x,y,u))) = - u
let u, x, y be VECTOR of V; ( Gen x,y implies Orte (x,y,(Orte (x,y,u))) = - u )
assume A1:
Gen x,y
; 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:24
.=
(- ((pr1 (x,y,u)) * x)) + ((- (pr2 (x,y,u))) * y)
by RLVECT_1:25
.=
(- ((pr1 (x,y,u)) * x)) + ((pr2 (x,y,u)) * (- y))
by RLVECT_1:24
.=
(- ((pr1 (x,y,u)) * x)) + (- ((pr2 (x,y,u)) * y))
by RLVECT_1:25
.=
- (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y))
by RLVECT_1:31
.=
- u
by A1, Lm5
;
verum