let V be RealLinearSpace; for u, v, x, y being VECTOR of V
for a being Real st Gen x,y holds
( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
let u, v, x, y be VECTOR of V; for a being Real st Gen x,y holds
( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
let a be Real; ( Gen x,y implies ( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) ) )
assume A1:
Gen x,y
; ( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
set p1u = pr1 (x,y,u);
set p2u = pr2 (x,y,u);
set p1v = pr1 (x,y,v);
set p2v = pr2 (x,y,v);
A2:
u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)
by A1, Lm5;
A3:
v = ((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y)
by A1, Lm5;
then u + v =
((((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)) + ((pr1 (x,y,v)) * x)) + ((pr2 (x,y,v)) * y)
by A2, RLVECT_1:def 3
.=
((((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + ((pr2 (x,y,u)) * y)) + ((pr2 (x,y,v)) * y)
by RLVECT_1:def 3
.=
(((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (((pr2 (x,y,u)) * y) + ((pr2 (x,y,v)) * y))
by RLVECT_1:def 3
.=
(((pr1 (x,y,u)) + (pr1 (x,y,v))) * x) + (((pr2 (x,y,u)) * y) + ((pr2 (x,y,v)) * y))
by RLVECT_1:def 6
.=
(((pr1 (x,y,u)) + (pr1 (x,y,v))) * x) + (((pr2 (x,y,u)) + (pr2 (x,y,v))) * y)
by RLVECT_1:def 6
;
hence
( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) )
by A1, Lm6; ( pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
u - v = (((pr1 (x,y,u)) - (pr1 (x,y,v))) * x) + (((pr2 (x,y,u)) - (pr2 (x,y,v))) * y)
by A2, A3, Lm1;
hence
( pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) )
by A1, Lm6; ( pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
a * u = ((a * (pr1 (x,y,u))) * x) + ((a * (pr2 (x,y,u))) * y)
by A2, Lm2;
hence
( pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
by A1, Lm6; verum