let F be Field; for S being OrtSp of F
for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
let S be OrtSp of F; for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
let a, p, x, y be Element of S; ( not p _|_ & not p _|_ & not p _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1:
not p _|_
and
A2:
not p _|_
and
A3:
not p _|_
; (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
A4:
not y _|_
by A3, Th2;
A5:
not x _|_
by A2, Th2;
A6:
now ( not x _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) )A7:
ProJ (
p,
a,
x)
<> 0. F
by A1, A2, Th20;
assume A8:
not
x _|_
;
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))then A9:
not
y _|_
by Th2;
(ProJ (p,a,y)) * ((ProJ (p,a,x)) ") = ProJ (
p,
x,
y)
by A1, A2, Th21;
then
((ProJ (p,a,y)) * ((ProJ (p,a,x)) ")) * (ProJ (p,a,x)) = (((ProJ (x,y,p)) ") * (ProJ (y,x,p))) * (ProJ (p,a,x))
by A5, A8, Th24;
then
(ProJ (p,a,y)) * (((ProJ (p,a,x)) ") * (ProJ (p,a,x))) = (((ProJ (x,y,p)) ") * (ProJ (y,x,p))) * (ProJ (p,a,x))
by GROUP_1:def 3;
then
(ProJ (p,a,y)) * (1_ F) = (((ProJ (x,y,p)) ") * (ProJ (y,x,p))) * (ProJ (p,a,x))
by A7, VECTSP_1:def 10;
then
ProJ (
p,
a,
y)
= ((ProJ (y,x,p)) * ((ProJ (x,y,p)) ")) * (ProJ (p,a,x))
;
then
ProJ (
p,
a,
y)
= (ProJ (y,x,p)) * (((ProJ (x,y,p)) ") * (ProJ (p,a,x)))
by GROUP_1:def 3;
then
(ProJ (y,p,x)) * (ProJ (p,a,y)) = (ProJ (y,p,x)) * (((ProJ (y,p,x)) ") * (((ProJ (x,y,p)) ") * (ProJ (p,a,x))))
by A4, A9, Th22;
then A10:
(ProJ (y,p,x)) * (ProJ (p,a,y)) = ((ProJ (y,p,x)) * ((ProJ (y,p,x)) ")) * (((ProJ (x,y,p)) ") * (ProJ (p,a,x)))
by GROUP_1:def 3;
ProJ (
y,
p,
x)
<> 0. F
by A4, A9, Th20;
then (ProJ (y,p,x)) * (ProJ (p,a,y)) =
(((ProJ (x,y,p)) ") * (ProJ (p,a,x))) * (1_ F)
by A10, VECTSP_1:def 10
.=
((ProJ (x,y,p)) ") * (ProJ (p,a,x))
;
hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
by A5, A8, Th22;
verum end;
now ( x _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) )assume A11:
x _|_
;
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))then
ProJ (
x,
p,
y)
= 0. F
by A5, Th20;
then A12:
(ProJ (p,a,x)) * (ProJ (x,p,y)) = 0. F
;
y _|_
by A11, Th2;
then
ProJ (
y,
p,
x)
= 0. F
by A4, Th20;
hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
by A12;
verum end;
hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
by A6; verum