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 = PProJ a,b,y,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 = PProJ a,b,y,x
let b, a, x, y be Element of S; :: thesis: ( not a _|_ implies PProJ a,b,x,y = PProJ a,b,y,x )
assume A1:
not a _|_
; :: thesis: PProJ a,b,x,y = PProJ a,b,y,x
A2:
now assume
y _|_
;
:: thesis: PProJ a,b,x,y = PProJ a,b,y,xthen
(
x _|_ &
y _|_ )
by Th12;
then
(
PProJ a,
b,
x,
y = 0. F &
PProJ a,
b,
y,
x = 0. F )
by A1, Th44;
hence
PProJ a,
b,
x,
y = PProJ a,
b,
y,
x
;
:: thesis: verum end;
now assume
not
y _|_
;
:: thesis: PProJ a,b,x,y = PProJ a,b,y,xthen
(
a <> 0. S &
x <> 0. S &
y <> 0. S )
by A1, Th11, Th12;
then
ex
r being
Element of
S st
( not
a _|_ & not
x _|_ & not
y _|_ & not
a _|_ )
by Def2;
then consider r being
Element of
S such that A3:
( not
a _|_ & not
x _|_ & not
y _|_ )
;
A4:
( not
b _|_ & not
r _|_ & not
r _|_ & not
r _|_ )
by A1, A3, Th12;
A5:
PProJ a,
b,
x,
y = ((ProJ a,b,r) * (ProJ r,a,x)) * (ProJ x,r,y)
by A1, A3, Def7;
PProJ a,
b,
y,
x = ((ProJ a,b,r) * (ProJ r,a,y)) * (ProJ y,r,x)
by A1, A3, Def7;
then
PProJ a,
b,
y,
x = (ProJ a,b,r) * ((ProJ r,a,y) * (ProJ y,r,x))
by GROUP_1:def 4;
then
PProJ a,
b,
y,
x = (ProJ a,b,r) * ((ProJ r,a,x) * (ProJ x,r,y))
by A4, Th40;
hence
PProJ a,
b,
x,
y = PProJ a,
b,
y,
x
by A5, GROUP_1:def 4;
:: thesis: verum end;
hence
PProJ a,b,x,y = PProJ a,b,y,x
by A2; :: thesis: verum