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 = 0. F iff 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 = 0. F iff 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 = 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, Th11, Th12;
A4: ( PProJ a,b,x,y = 0. F implies x _|_ )

proof

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

A6: now

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

end;

now

given p being Element of S such that A7: ( not a _|_ & not x _|_ ) ; :: thesis: x _|_
((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = 0. F by A1, A2, A5, A7, Def6;
then ( (ProJ a,b,p) * (ProJ p,a,x) = 0. F or ProJ x,p,y = 0. F ) by VECTSP_1:44;
then A8: ( ProJ a,b,p = 0. F or ProJ p,a,x = 0. F or ProJ x,p,y = 0. F ) by VECTSP_1:44;

now

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

end;

hence x _|_ by A2, A7, A8, Th36; :: thesis: verum

end;

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

end;

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

proof

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

A11: 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, A2, Def6; :: thesis: verum

end;

now

assume x <> 0. S ; :: thesis: PProJ a,b,x,y = 0. F
then consider p being Element of S such that
A12: ( not a _|_ & not x _|_ ) by A3, Th21;
ProJ x,p,y = 0. F by A10, A12, Th36;
then ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = 0. F by VECTSP_1:39;
hence PProJ a,b,x,y = 0. F by A1, A2, A12, Def6; :: thesis: verum

end;

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

end;

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