let F be Field; :: thesis: for S being SymSp of F
for p, a, x, q 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 p, a, x, q 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 p, a, x, q 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, Th12;
(ProJ (p,a,x)) * (ProJ (q,x,a)) = (ProJ (a,p,q)) * (ProJ (x,q,p)) by A1, A2, A3, A5, Th41;
then (ProJ (p,a,x)) * (ProJ (q,x,a)) = ((ProJ (a,q,p)) ") * (ProJ (x,q,p)) by A2, A4, Th38;
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 4;
ProJ (a,q,p) <> 0. F by A2, A4, Th36;
then (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = (ProJ (x,q,p)) * (1_ F) by A7, VECTSP_1:def 22;
then (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = ProJ (x,q,p) by VECTSP_1:def 19;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (ProJ (q,x,a)) = ProJ (x,q,p) by GROUP_1:def 4;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * ((ProJ (q,a,x)) ") = ProJ (x,q,p) by A6, Th38;
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 4;
ProJ (q,a,x) <> 0. F by A6, Th36;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A8, VECTSP_1:def 22;
hence (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by VECTSP_1:def 19; :: thesis: verum