let F be Field; :: thesis: for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
let S be SymSp of F; :: thesis: for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
let b, a, x, y be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; :: thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))

A3: now

assume not y _|_ ; :: thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
then A4: ( x <> 0. S & y <> 0. S ) by Th11, Th12;
a <> 0. S by A2, Th11, Th12;
then consider r being Element of S such that
A5: not a _|_ and
A6: not x _|_ and
A7: not y _|_ by A1, A4, Th22;
A8: not r _|_ by A7, Th12;
PProJ (a,b,y,x) = ((ProJ (a,b,r)) * (ProJ (r,a,y))) * (ProJ (y,r,x)) by A1, A2, A5, A7, Def6;
then A9: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,y)) * (ProJ (y,r,x))) by GROUP_1:def 4;
( not r _|_ & not r _|_ ) by A5, A6, Th12;
then PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((- (ProJ (r,a,x))) * (ProJ (x,r,y))) by A8, A9, Th44;
then PProJ (a,b,y,x) = ((- (ProJ (r,a,x))) * (ProJ (a,b,r))) * (ProJ (x,r,y)) by GROUP_1:def 4;
then PProJ (a,b,y,x) = (- ((ProJ (r,a,x)) * (ProJ (a,b,r)))) * (ProJ (x,r,y)) by VECTSP_1:41;
then (- (1_ F)) * (PProJ (a,b,y,x)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) by VECTSP_1:41;
then - ((PProJ (a,b,y,x)) * (1_ F)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) by VECTSP_1:41;
then - (PProJ (a,b,y,x)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) by VECTSP_1:def 19;
then A10: - (PProJ (a,b,y,x)) = (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y))) * (1_ F) by VECTSP_1:42;
PProJ (a,b,x,y) = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)) by A1, A2, A5, A6, Def6;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A10, VECTSP_1:def 19; :: thesis: verum

end;

now

assume A11: y _|_ ; :: thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
then (- (1_ F)) * (PProJ (a,b,y,x)) = (- (1_ F)) * (0. F) by A1, A2, Th48;
then - ((PProJ (a,b,y,x)) * (1_ F)) = (- (1_ F)) * (0. F) by VECTSP_1:41;
then A12: - (PProJ (a,b,y,x)) = (- (1_ F)) * (0. F) by VECTSP_1:def 19;
x _|_ by A11, Th12;
then PProJ (a,b,x,y) = 0. F by A1, A2, Th48;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A12, VECTSP_1:39; :: thesis: verum

end;

hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A3; :: thesis: verum