let V be RealLinearSpace; for w, y being VECTOR of V st Gen w,y holds
for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
let w, y be VECTOR of V; ( Gen w,y implies for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) ) )
assume A1:
Gen w,y
; for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
let u, v, v1 be VECTOR of V; ( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
A2:
now for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) )let u,
v,
v1 be
VECTOR of
V;
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) )A3:
PProJ (
w,
y,
u,
(v - v1)) =
((pr1 (w,y,u)) * ((pr1 (w,y,v)) - (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * (pr2 (w,y,(v - v1))))
by A1, Lm17
.=
((pr1 (w,y,u)) * ((pr1 (w,y,v)) - (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * ((pr2 (w,y,v)) - (pr2 (w,y,v1))))
by A1, Lm17
.=
(PProJ (w,y,u,v)) - (PProJ (w,y,u,v1))
;
PProJ (
w,
y,
u,
(v + v1)) =
((pr1 (w,y,u)) * ((pr1 (w,y,v)) + (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * (pr2 (w,y,(v + v1))))
by A1, Lm17
.=
((pr1 (w,y,u)) * ((pr1 (w,y,v)) + (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * ((pr2 (w,y,v)) + (pr2 (w,y,v1))))
by A1, Lm17
.=
(PProJ (w,y,u,v)) + (PProJ (w,y,u,v1))
;
hence
(
PProJ (
w,
y,
u,
(v + v1))
= (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) &
PProJ (
w,
y,
u,
(v - v1))
= (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) )
by A3;
verum end;
hence
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) )
; ( PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
thus PProJ (w,y,(v - v1),u) =
PProJ (w,y,u,(v - v1))
.=
(PProJ (w,y,u,v)) - (PProJ (w,y,u,v1))
by A2
.=
(PProJ (w,y,v,u)) - (PProJ (w,y,v1,u))
; PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u))
thus PProJ (w,y,(v + v1),u) =
PProJ (w,y,u,(v + v1))
.=
(PProJ (w,y,u,v)) + (PProJ (w,y,u,v1))
by A2
.=
(PProJ (w,y,v,u)) + (PProJ (w,y,v1,u))
; verum