let F be Field; :: thesis: for S being OrtSp of F
for a, p, q, x 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; :: thesis: for a, p, q, x 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 a, p, q, x be Element of S; :: thesis: ( 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 _|_ ; :: thesis: (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, Th1;
A6: not p _|_ by A1, Th2;
( a <> 0. S & x <> 0. S ) by A1, A2, Th1, Th2;
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, Def1;
A11: not r _|_ by A8, Th2;
A12: not r _|_ by A10, Th2;
A13: not r _|_ by A7, Th2;
then A14: ProJ (r,q,p) <> 0. F by A11, Th20;
A15: not r _|_ by A9, Th2;
A16: not q _|_ by A4, Th2;
A17: not p _|_ by A2, Th2;
A18: not q _|_ by A3, Th2;
((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, Th21
.= (((ProJ (a,r,p)) * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * ((ProJ (p,r,a)) "))) * ((ProJ (q,a,x)) ") by A6, A7, Th21
.= (((ProJ (a,r,p)) * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * ((ProJ (p,r,a)) "))) * (ProJ (q,x,a)) by A18, A16, Th22
.= (((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, Th21
.= ((((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, Th22
.= ((((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, Th22
.= ((((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, Th22
.= ((((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, Th22
.= ((((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, Th22
.= ((((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, Th22
.= (((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 3
.= (((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 3
.= (((ProJ (p,x,r)) ") * ((ProJ (r,a,p)) * (ProJ (a,q,r)))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by A1, A9, Th24
.= ((((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * (ProJ (a,q,r))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * ((ProJ (a,q,r)) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r)))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * ((((ProJ (q,a,r)) ") * (ProJ (a,q,r))) * (ProJ (q,x,r))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * ((ProJ (r,q,a)) * (ProJ (q,x,r))) by A18, A8, Th24
.= ((ProJ (p,x,r)) ") * ((ProJ (r,a,p)) * ((ProJ (r,q,a)) * (ProJ (q,x,r)))) by GROUP_1:def 3
.= ((ProJ (p,x,r)) ") * (((ProJ (r,a,p)) * (ProJ (r,q,a))) * (ProJ (q,x,r))) by GROUP_1:def 3
.= ((ProJ (p,x,r)) ") * (((ProJ (r,a,p)) * ((ProJ (r,a,q)) ")) * (ProJ (q,x,r))) by A11, A15, Th22
.= ((ProJ (p,x,r)) ") * ((ProJ (r,q,p)) * (ProJ (q,x,r))) by A11, A15, Th21
.= (ProJ (p,r,x)) * ((ProJ (r,q,p)) * (ProJ (q,x,r))) by A17, A7, Th22
.= (((ProJ (r,x,p)) ") * (ProJ (x,r,p))) * ((ProJ (r,q,p)) * (ProJ (q,x,r))) by A13, A12, Th24
.= (((ProJ (r,x,p)) ") * (ProJ (x,r,p))) * ((ProJ (r,q,p)) * (((ProJ (x,r,q)) ") * (ProJ (r,x,q)))) by A4, A10, Th24
.= (((ProJ (r,x,p)) ") * (ProJ (x,r,p))) * ((ProJ (r,x,q)) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) "))) by GROUP_1:def 3
.= (((ProJ (x,r,p)) * ((ProJ (r,x,p)) ")) * (ProJ (r,x,q))) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) ")) by GROUP_1:def 3
.= ((ProJ (x,r,p)) * ((ProJ (r,x,q)) * ((ProJ (r,x,p)) "))) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) ")) by GROUP_1:def 3
.= ((ProJ (x,r,p)) * (ProJ (r,p,q))) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) ")) by A13, A12, Th21
.= (ProJ (x,r,p)) * ((ProJ (r,p,q)) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) "))) by GROUP_1:def 3
.= (ProJ (x,r,p)) * (((ProJ (r,p,q)) * (ProJ (r,q,p))) * ((ProJ (x,r,q)) ")) by GROUP_1:def 3
.= (ProJ (x,r,p)) * ((((ProJ (r,q,p)) ") * (ProJ (r,q,p))) * ((ProJ (x,r,q)) ")) by A13, A11, Th22
.= (ProJ (x,r,p)) * (((ProJ (x,r,q)) ") * (1_ F)) by A14, VECTSP_1:def 10
.= (ProJ (x,r,p)) * ((ProJ (x,r,q)) ")
.= ProJ (x,q,p) by A4, A10, Th21 ;
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 3;
ProJ (q,a,x) <> 0. F by A18, A16, Th20;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (q,a,x)) * (ProJ (x,q,p)) by A19, VECTSP_1:def 10;
hence (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p)) ; :: thesis: verum