let F be Field; :: thesis: for S being OrtSp of F
for b, a, x, y being Element of S st not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
let S be OrtSp of F; :: thesis: for b, a, x, y being Element of S st not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
let b, a, x, y be Element of S; :: thesis: ( not a _|_ implies ( PProJ (a,b,x,y) = 0. F iff x _|_ ) )
set 0F = 0. F;
assume A1: not a _|_ ; :: thesis: ( PProJ (a,b,x,y) = 0. F iff x _|_ )
then A2: a <> 0. S by Th11, Th12;
A3: ( PProJ (a,b,x,y) = 0. F implies x _|_ )

proof

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

A5: now

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

A8: now

assume A9: ProJ (p,a,x) = 0. F ; :: thesis: contradiction
not p _|_ by A6, Th12;
then p _|_ by A9, Th33;
hence contradiction by A7, Th12; :: thesis: verum

end;

((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by A1, A4, A6, A7, Def7;
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 A1, A6, A7, A8, Th33; :: thesis: verum

end;

now

assume A10: for p being Element of S holds
( a _|_ or x _|_ ) ; :: thesis: x _|_
x = 0. S

proof

assume not x = 0. S ; :: thesis: contradiction
then ex p being Element of S st
( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A2, Def2;
hence contradiction by A10; :: thesis: verum

end;

hence x _|_ by Th11, Th12; :: thesis: verum

end;

hence x _|_ by A5; :: 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

assume x <> 0. S ; :: thesis: PProJ (a,b,x,y) = 0. F
then ex p being Element of S st
( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A2, Def2;
then consider p being Element of S such that
A13: not a _|_ and
A14: not x _|_ ;
ProJ (x,p,y) = 0. F by A11, A14, Th33;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by VECTSP_1:7;
hence PProJ (a,b,x,y) = 0. F by A1, A13, A14, Def7; :: thesis: verum

end;

now

assume x = 0. S ; :: thesis: PProJ (a,b,x,y) = 0. F
then for p being Element of S holds
( a _|_ or x _|_ ) by Th11, Th12;
hence PProJ (a,b,x,y) = 0. F by A1, Def7; :: 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 A3; :: thesis: verum