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