let F be Field; for S being OrtSp of F
for p, a, x, q being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ a,q,p) * (ProJ p,a,x) = (ProJ q,a,x) * (ProJ x,q,p)
let S be OrtSp of F; for p, a, x, q being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ a,q,p) * (ProJ p,a,x) = (ProJ q,a,x) * (ProJ x,q,p)
let p, a, x, q be Element of S; ( not a _|_ & not x _|_ & not a _|_ & not x _|_ implies (ProJ a,q,p) * (ProJ p,a,x) = (ProJ q,a,x) * (ProJ x,q,p) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1:
not a _|_
and
A2:
not x _|_
and
A3:
not a _|_
and
A4:
not x _|_
; (ProJ a,q,p) * (ProJ p,a,x) = (ProJ q,a,x) * (ProJ x,q,p)
A5:
( p <> 0. S & q <> 0. S )
by A1, A3, Th11;
A6:
not p _|_
by A1, Th12;
( a <> 0. S & x <> 0. S )
by A1, A2, Th11, Th12;
then consider r being Element of S such that
A7:
not p _|_
and
A8:
not q _|_
and
A9:
not a _|_
and
A10:
not x _|_
by A5, Def2;
A11:
not r _|_
by A8, Th12;
A12:
not r _|_
by A10, Th12;
A13:
not r _|_
by A7, Th12;
then A14:
ProJ r,q,p <> 0. F
by A11, Th33;
A15:
not r _|_
by A9, Th12;
A16:
not q _|_
by A4, Th12;
A17:
not p _|_
by A2, Th12;
A18:
not q _|_
by A3, Th12;
((ProJ a,q,p) * (ProJ p,a,x)) * ((ProJ q,a,x) " ) =
(((ProJ a,r,p) * ((ProJ a,r,q) " )) * (ProJ p,a,x)) * ((ProJ q,a,x) " )
by A3, A9, Th34
.=
(((ProJ a,r,p) * ((ProJ a,r,q) " )) * ((ProJ p,r,x) * ((ProJ p,r,a) " ))) * ((ProJ q,a,x) " )
by A6, A7, Th34
.=
(((ProJ a,r,p) * ((ProJ a,r,q) " )) * ((ProJ p,r,x) * ((ProJ p,r,a) " ))) * (ProJ q,x,a)
by A18, A16, Th35
.=
(((ProJ a,r,p) * ((ProJ a,r,q) " )) * ((ProJ p,r,x) * ((ProJ p,r,a) " ))) * ((ProJ q,r,a) * ((ProJ q,r,x) " ))
by A16, A8, Th34
.=
((((ProJ a,p,r) " ) * ((ProJ a,r,q) " )) * ((ProJ p,r,x) * ((ProJ p,r,a) " ))) * ((ProJ q,r,a) * ((ProJ q,r,x) " ))
by A1, A9, Th35
.=
((((ProJ a,p,r) " ) * ((ProJ a,r,q) " )) * ((ProJ p,r,x) * (ProJ p,a,r))) * ((ProJ q,r,a) * ((ProJ q,r,x) " ))
by A6, A7, Th35
.=
((((ProJ a,p,r) " ) * (ProJ a,q,r)) * ((ProJ p,r,x) * (ProJ p,a,r))) * ((ProJ q,r,a) * ((ProJ q,r,x) " ))
by A3, A9, Th35
.=
((((ProJ a,p,r) " ) * (ProJ a,q,r)) * ((ProJ p,r,x) * (ProJ p,a,r))) * (((ProJ q,a,r) " ) * ((ProJ q,r,x) " ))
by A18, A8, Th35
.=
((((ProJ a,p,r) " ) * (ProJ a,q,r)) * (((ProJ p,x,r) " ) * (ProJ p,a,r))) * (((ProJ q,a,r) " ) * ((ProJ q,r,x) " ))
by A17, A7, Th35
.=
((((ProJ p,x,r) " ) * (ProJ p,a,r)) * (((ProJ a,p,r) " ) * (ProJ a,q,r))) * (((ProJ q,a,r) " ) * (ProJ q,x,r))
by A16, A8, Th35
.=
(((ProJ p,x,r) " ) * ((((ProJ a,p,r) " ) * (ProJ a,q,r)) * (ProJ p,a,r))) * (((ProJ q,a,r) " ) * (ProJ q,x,r))
by GROUP_1:def 4
.=
(((ProJ p,x,r) " ) * ((((ProJ a,p,r) " ) * (ProJ p,a,r)) * (ProJ a,q,r))) * (((ProJ q,a,r) " ) * (ProJ q,x,r))
by GROUP_1:def 4
.=
(((ProJ p,x,r) " ) * ((ProJ r,a,p) * (ProJ a,q,r))) * (((ProJ q,a,r) " ) * (ProJ q,x,r))
by A1, A9, Th37
.=
((((ProJ p,x,r) " ) * (ProJ r,a,p)) * (ProJ a,q,r)) * (((ProJ q,a,r) " ) * (ProJ q,x,r))
by GROUP_1:def 4
.=
(((ProJ p,x,r) " ) * (ProJ r,a,p)) * ((ProJ a,q,r) * (((ProJ q,a,r) " ) * (ProJ q,x,r)))
by GROUP_1:def 4
.=
(((ProJ p,x,r) " ) * (ProJ r,a,p)) * ((((ProJ q,a,r) " ) * (ProJ a,q,r)) * (ProJ q,x,r))
by GROUP_1:def 4
.=
(((ProJ p,x,r) " ) * (ProJ r,a,p)) * ((ProJ r,q,a) * (ProJ q,x,r))
by A18, A8, Th37
.=
((ProJ p,x,r) " ) * ((ProJ r,a,p) * ((ProJ r,q,a) * (ProJ q,x,r)))
by GROUP_1:def 4
.=
((ProJ p,x,r) " ) * (((ProJ r,a,p) * (ProJ r,q,a)) * (ProJ q,x,r))
by GROUP_1:def 4
.=
((ProJ p,x,r) " ) * (((ProJ r,a,p) * ((ProJ r,a,q) " )) * (ProJ q,x,r))
by A11, A15, Th35
.=
((ProJ p,x,r) " ) * ((ProJ r,q,p) * (ProJ q,x,r))
by A11, A15, Th34
.=
(ProJ p,r,x) * ((ProJ r,q,p) * (ProJ q,x,r))
by A17, A7, Th35
.=
(((ProJ r,x,p) " ) * (ProJ x,r,p)) * ((ProJ r,q,p) * (ProJ q,x,r))
by A13, A12, Th37
.=
(((ProJ r,x,p) " ) * (ProJ x,r,p)) * ((ProJ r,q,p) * (((ProJ x,r,q) " ) * (ProJ r,x,q)))
by A4, A10, Th37
.=
(((ProJ r,x,p) " ) * (ProJ x,r,p)) * ((ProJ r,x,q) * ((ProJ r,q,p) * ((ProJ x,r,q) " )))
by GROUP_1:def 4
.=
(((ProJ x,r,p) * ((ProJ r,x,p) " )) * (ProJ r,x,q)) * ((ProJ r,q,p) * ((ProJ x,r,q) " ))
by GROUP_1:def 4
.=
((ProJ x,r,p) * ((ProJ r,x,q) * ((ProJ r,x,p) " ))) * ((ProJ r,q,p) * ((ProJ x,r,q) " ))
by GROUP_1:def 4
.=
((ProJ x,r,p) * (ProJ r,p,q)) * ((ProJ r,q,p) * ((ProJ x,r,q) " ))
by A13, A12, Th34
.=
(ProJ x,r,p) * ((ProJ r,p,q) * ((ProJ r,q,p) * ((ProJ x,r,q) " )))
by GROUP_1:def 4
.=
(ProJ x,r,p) * (((ProJ r,p,q) * (ProJ r,q,p)) * ((ProJ x,r,q) " ))
by GROUP_1:def 4
.=
(ProJ x,r,p) * ((((ProJ r,q,p) " ) * (ProJ r,q,p)) * ((ProJ x,r,q) " ))
by A13, A11, Th35
.=
(ProJ x,r,p) * (((ProJ x,r,q) " ) * (1_ F))
by A14, VECTSP_1:def 22
.=
(ProJ x,r,p) * ((ProJ x,r,q) " )
by VECTSP_1:def 19
.=
ProJ x,q,p
by A4, A10, Th34
;
then A19:
((ProJ q,a,x) * ((ProJ q,a,x) " )) * ((ProJ a,q,p) * (ProJ p,a,x)) = (ProJ q,a,x) * (ProJ x,q,p)
by GROUP_1:def 4;
ProJ q,a,x <> 0. F
by A18, A16, Th33;
then
((ProJ a,q,p) * (ProJ p,a,x)) * (1_ F) = (ProJ q,a,x) * (ProJ x,q,p)
by A19, VECTSP_1:def 22;
hence
(ProJ a,q,p) * (ProJ p,a,x) = (ProJ q,a,x) * (ProJ x,q,p)
by VECTSP_1:def 19; verum