let V be RealLinearSpace; for u, v, x, y being VECTOR of V st Gen x,y & Orte (x,y,u) = Orte (x,y,v) holds
u = v
let u, v, x, y be VECTOR of V; ( Gen x,y & Orte (x,y,u) = Orte (x,y,v) implies u = v )
assume that
A1:
Gen x,y
and
A2:
Orte (x,y,u) = Orte (x,y,v)
; u = v
(((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y)) - (((pr2 (x,y,v)) * x) + ((- (pr1 (x,y,v))) * y)) = 0. V
by A2, RLVECT_1:15;
then
((((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y)) - ((pr2 (x,y,v)) * x)) - ((- (pr1 (x,y,v))) * y) = 0. V
by RLVECT_1:27;
then
((((pr2 (x,y,u)) * x) + (- ((pr2 (x,y,v)) * x))) + ((- (pr1 (x,y,u))) * y)) - ((- (pr1 (x,y,v))) * y) = 0. V
by RLVECT_1:def 3;
then
(((pr2 (x,y,u)) * x) - ((pr2 (x,y,v)) * x)) + (((- (pr1 (x,y,u))) * y) - ((- (pr1 (x,y,v))) * y)) = 0. V
by RLVECT_1:def 3;
then
(((pr2 (x,y,u)) - (pr2 (x,y,v))) * x) + (((- (pr1 (x,y,u))) * y) - ((- (pr1 (x,y,v))) * y)) = 0. V
by RLVECT_1:35;
then A3:
(((pr2 (x,y,u)) - (pr2 (x,y,v))) * x) + (((- (pr1 (x,y,u))) - (- (pr1 (x,y,v)))) * y) = 0. V
by RLVECT_1:35;
then A4:
(pr2 (x,y,u)) - (pr2 (x,y,v)) = 0
by A1, ANALMETR:def 1;
(- (pr1 (x,y,u))) - (- (pr1 (x,y,v))) = 0
by A1, A3, ANALMETR:def 1;
hence u =
((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y)
by A1, A4, Lm5
.=
v
by A1, Lm5
;
verum