let F be Field; 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; 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; ( not a _|_ implies ( PProJ (a,b,x,y) = 0. F iff x _|_ ) )
set 0F = 0. F;
assume A1:
not a _|_
; ( 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
assume A4:
PProJ (
a,
b,
x,
y)
= 0. F
;
x _|_
A5:
now ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies x _|_ )given p being
Element of
S such that A6:
not
a _|_
and A7:
not
x _|_
;
x _|_
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F
by A1, A4, A6, A7, 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 A1, A6, A7, A8, Th20;
verum end;
hence
x _|_
by A5;
verum
end;
( x _|_ implies PProJ (a,b,x,y) = 0. F )
proof
assume A11:
x _|_
;
PProJ (a,b,x,y) = 0. F
A12:
now ( x <> 0. S implies PProJ (a,b,x,y) = 0. F )assume
x <> 0. S
;
PProJ (a,b,x,y) = 0. Fthen
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;
verum end;
hence
PProJ (
a,
b,
x,
y)
= 0. F
by A12;
verum
end;
hence
( PProJ (a,b,x,y) = 0. F iff x _|_ )
by A3; verum