let F be Field; :: thesis: for S being OrtSp of F

for a, b, 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 a, b, x, y being Element of S st not a _|_ holds

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

let a, b, 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 Th1, Th2;

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

for a, b, 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 a, b, x, y being Element of S st not a _|_ holds

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

let a, b, 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 Th1, Th2;

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

proof

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

end;A5: now :: thesis: ( ex p being Element of S st

( not a _|_ & not x _|_ ) implies x _|_ )

( not a _|_ & not x _|_ ) implies x _|_ )

given p being Element of S such that A6:
not a _|_
and

A7: not x _|_ ; :: thesis: x _|_

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, Th20; :: thesis: verum

end;A7: not x _|_ ; :: thesis: x _|_

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

((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F
by A1, A4, A6, A7, Def3;assume A9:
ProJ (p,a,x) = 0. F
; :: thesis: contradiction

not p _|_ by A6, Th2;

then p _|_ by A9, Th20;

hence contradiction by A7, Th2; :: thesis: verum

end;not p _|_ by A6, Th2;

then p _|_ by A9, Th20;

hence contradiction by A7, Th2; :: thesis: verum

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, Th20; :: thesis: verum

now :: thesis: ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) implies x _|_ )

hence
x _|_
by A5; :: thesis: verum( a _|_ or x _|_ ) ) implies x _|_ )

assume A10:
for p being Element of S holds

( a _|_ or x _|_ ) ; :: thesis: x _|_

x = 0. S

end;( a _|_ or x _|_ ) ; :: thesis: x _|_

x = 0. S

proof

hence
x _|_
by Th1, Th2; :: thesis: verum
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, Def1;

hence contradiction by A10; :: thesis: verum

end;then ex p being Element of S st

( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A2, Def1;

hence contradiction by A10; :: thesis: verum

proof

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

end;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 ex p being Element of S st

( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A2, Def1;

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, Th20;

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, A13, A14, Def3; :: thesis: verum

end;then ex p being Element of S st

( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A2, Def1;

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, Th20;

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, A13, A14, Def3; :: thesis: verum

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

hence
PProJ (a,b,x,y) = 0. F
by A12; :: thesis: verumassume
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, Def3; :: thesis: verum

end;then for p being Element of S holds

( a _|_ or x _|_ ) by Th1, Th2;

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