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