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) = 0. F iff 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) = 0. F iff 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) = 0. F iff x _|_ ) )
set 0F = 0. F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; :: thesis: ( PProJ (a,b,x,y) = 0. F iff x _|_ )
A3: a <> 0. S by A2, Th1, Th2;
A4: ( PProJ (a,b,x,y) = 0. F implies x _|_ )

proof

assume A5: PProJ (a,b,x,y) = 0. F ; :: thesis: x _|_

A6: now :: thesis: ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies x _|_ )

given p being Element of S such that A7: not a _|_ and
A8: not x _|_ ; :: thesis: x _|_

A9: now :: thesis: not ProJ (p,a,x) = 0. F

assume A10: ProJ (p,a,x) = 0. F ; :: thesis: contradiction
not p _|_ by A7, Th2;
then p _|_ by A10, Th23;
hence contradiction by A8, Th2; :: thesis: verum

end;

((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by A1, A2, A5, A7, A8, Def3;
then ( (ProJ (a,b,p)) * (ProJ (p,a,x)) = 0. F or ProJ (x,p,y) = 0. F ) by VECTSP_1:12;
then ( ProJ (a,b,p) = 0. F or ProJ (p,a,x) = 0. F or ProJ (x,p,y) = 0. F ) by VECTSP_1:12;
hence x _|_ by A2, A7, A8, A9, Th23; :: thesis: verum

end;

now :: thesis: ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies x _|_ )

assume for p being Element of S holds
( a _|_ or x _|_ ) ; :: thesis: x _|_
then x = 0. S by A3, Th9;
hence x _|_ by Th1, Th2; :: thesis: verum

end;

hence x _|_ by A6; :: thesis: verum

end;

( x _|_ implies PProJ (a,b,x,y) = 0. F )

proof

assume A11: x _|_ ; :: thesis: PProJ (a,b,x,y) = 0. F

A12: now :: thesis: ( x <> 0. S implies PProJ (a,b,x,y) = 0. F )

assume x <> 0. S ; :: thesis: PProJ (a,b,x,y) = 0. F
then consider p being Element of S such that
A13: not a _|_ and
A14: not x _|_ by A3, Th9;
ProJ (x,p,y) = 0. F by A11, A14, Th23;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F ;
hence PProJ (a,b,x,y) = 0. F by A1, A2, A13, A14, Def3; :: thesis: verum

end;

now :: thesis: ( x = 0. S implies PProJ (a,b,x,y) = 0. F )

assume x = 0. S ; :: thesis: PProJ (a,b,x,y) = 0. F
then for p being Element of S holds
( a _|_ or x _|_ ) by Th1, Th2;
hence PProJ (a,b,x,y) = 0. F by A1, A2, Def3; :: thesis: verum

end;

hence PProJ (a,b,x,y) = 0. F by A12; :: thesis: verum

end;

hence ( PProJ (a,b,x,y) = 0. F iff x _|_ ) by A4; :: thesis: verum