let F be Field; :: thesis: for S being SymSp of F
for a, p, q, x being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
let S be SymSp of F; :: thesis: for a, p, q, x being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
let a, p, q, x be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ implies (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ and
A3: not x _|_ and
A4: not a _|_ and
A5: not x _|_ ; :: thesis: (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
A6: ( not q _|_ & not q _|_ ) by A4, A5, Th2;
(ProJ (p,a,x)) * (ProJ (q,x,a)) = (ProJ (a,p,q)) * (ProJ (x,q,p)) by A1, A2, A3, A5, Th28;
then (ProJ (p,a,x)) * (ProJ (q,x,a)) = ((ProJ (a,q,p)) ") * (ProJ (x,q,p)) by A2, A4, Th25;
then A7: (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = ((ProJ (a,q,p)) * ((ProJ (a,q,p)) ")) * (ProJ (x,q,p)) by GROUP_1:def 3;
ProJ (a,q,p) <> 0. F by A2, A4, Th23;
then (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = (ProJ (x,q,p)) * (1_ F) by A7, VECTSP_1:def 10;
then (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = ProJ (x,q,p) ;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (ProJ (q,x,a)) = ProJ (x,q,p) by GROUP_1:def 3;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * ((ProJ (q,a,x)) ") = ProJ (x,q,p) by A6, Th25;
then A8: ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (((ProJ (q,a,x)) ") * (ProJ (q,a,x))) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by GROUP_1:def 3;
ProJ (q,a,x) <> 0. F by A6, Th23;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A8, VECTSP_1:def 10;
hence (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) ; :: thesis: verum