let F be Field; :: thesis: for S being SymSp of F
for a, b, 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 a, b, 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 a, b, 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 :: thesis: ( not y _|_ implies PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) )

assume not y _|_ ; :: thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
then A4: ( x <> 0. S & y <> 0. S ) by Th1, Th2;
a <> 0. S by A2, Th1, Th2;
then consider r being Element of S such that
A5: not a _|_ and
A6: not x _|_ and
A7: not y _|_ by A1, A4, Th10;
A8: not r _|_ by A7, Th2;
PProJ (a,b,y,x) = ((ProJ (a,b,r)) * (ProJ (r,a,y))) * (ProJ (y,r,x)) by A1, A2, A5, A7, Def3;
then A9: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,y)) * (ProJ (y,r,x))) by GROUP_1:def 3;
( not r _|_ & not r _|_ ) by A5, A6, Th2;
then PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((- (ProJ (r,a,x))) * (ProJ (x,r,y))) by A8, A9, Th31;
then PProJ (a,b,y,x) = ((- (ProJ (r,a,x))) * (ProJ (a,b,r))) * (ProJ (x,r,y)) by GROUP_1:def 3;
then PProJ (a,b,y,x) = (- ((ProJ (r,a,x)) * (ProJ (a,b,r)))) * (ProJ (x,r,y)) by VECTSP_1:9;
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:9;
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:9;
then - (PProJ (a,b,y,x)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) ;
then A10: - (PProJ (a,b,y,x)) = (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y))) * (1_ F) by VECTSP_1:10;
PProJ (a,b,x,y) = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)) by A1, A2, A5, A6, Def3;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A10; :: thesis: verum

end;

now :: thesis: ( y _|_ implies PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) )

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, Th33;
then - ((PProJ (a,b,y,x)) * (1_ F)) = (- (1_ F)) * (0. F) by VECTSP_1:9;
then A12: - (PProJ (a,b,y,x)) = (- (1_ F)) * (0. F) ;
x _|_ by A11, Th2;
then PProJ (a,b,x,y) = 0. F by A1, A2, Th33;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A12; :: thesis: verum

end;

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