let F be Field; :: thesis: for S being SymSp of F
for a, b, p, q being Element of S st (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ holds
(ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
let S be SymSp of F; :: thesis: for a, b, p, q being Element of S st (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ holds
(ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
let a, b, p, q be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ implies (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not p _|_ and
A3: not q _|_ and
A4: not q _|_ ; :: thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))

A5: now :: thesis: ( q _|_ & b _|_ implies (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) )

assume that
A6: q _|_ and
A7: b _|_ ; :: thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
not b _|_ by A4, Th2;
then A8: ProJ (b,q,p) = ProJ (b,q,(p + a)) by A7, Th19;
A9: not q _|_ by A3, A6, Th4;
then A10: ProJ (b,q,(p + a)) = (- ((ProJ (q,(p + a),b)) ")) * (ProJ ((p + a),q,b)) by A4, Th27;
A11: a _|_ by A1, Th13;
A12: not a _|_ by A2, Th2;
then A13: ProJ (a,p,q) = ProJ (a,(p + a),q) by A11, Th19;
not a _|_ by A12, A11, Th4;
then A14: not p + a _|_ by Th2;
A15: not p + a _|_ by A9, Th2;
then ProJ (a,(p + a),q) = (- ((ProJ ((p + a),q,a)) ")) * (ProJ (q,(p + a),a)) by A14, Th27;
then (ProJ (a,p,q)) * (ProJ (b,q,p)) = (((ProJ (q,(p + a),a)) * (- ((ProJ ((p + a),q,a)) "))) * (- ((ProJ (q,(p + a),b)) "))) * (ProJ ((p + a),q,b)) by A13, A8, A10, GROUP_1:def 3
.= ((ProJ (q,(p + a),a)) * ((- ((ProJ ((p + a),q,a)) ")) * (- ((ProJ (q,(p + a),b)) ")))) * (ProJ ((p + a),q,b)) by GROUP_1:def 3
.= ((ProJ (q,(p + a),a)) * (((ProJ (q,(p + a),b)) ") * ((ProJ ((p + a),q,a)) "))) * (ProJ ((p + a),q,b)) by VECTSP_1:10
.= (((ProJ (q,(p + a),a)) * ((ProJ (q,(p + a),b)) ")) * ((ProJ ((p + a),q,a)) ")) * (ProJ ((p + a),q,b)) by GROUP_1:def 3
.= ((ProJ (q,b,a)) * ((ProJ ((p + a),q,a)) ")) * (ProJ ((p + a),q,b)) by A4, A9, Th24
.= (ProJ (q,b,a)) * ((ProJ ((p + a),q,b)) * ((ProJ ((p + a),q,a)) ")) by GROUP_1:def 3
.= (ProJ (q,b,a)) * (ProJ ((p + a),a,b)) by A14, A15, Th24
.= (ProJ (q,b,a)) * (ProJ (p,a,b)) by A2, A7, A11, Th20 ;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) ; :: thesis: verum

end;

A16: now :: thesis: ( not b _|_ implies (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) )

assume A17: not b _|_ ; :: thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
A18: not b _|_ by A4, Th2;
then A19: ProJ (q,b,a) = (- ((ProJ (b,a,q)) ")) * (ProJ (a,b,q)) by A17, Th27;
A20: not a _|_ by A2, Th2;
A21: not a _|_ by A17, Th2;
then ProJ (p,a,b) = (- ((ProJ (a,b,p)) ")) * (ProJ (b,a,p)) by A20, Th27;
then (ProJ (p,a,b)) * (ProJ (q,b,a)) = (((ProJ (b,a,p)) * (- ((ProJ (a,b,p)) "))) * (- ((ProJ (b,a,q)) "))) * (ProJ (a,b,q)) by A19, GROUP_1:def 3
.= ((ProJ (b,a,p)) * ((- ((ProJ (a,b,p)) ")) * (- ((ProJ (b,a,q)) ")))) * (ProJ (a,b,q)) by GROUP_1:def 3
.= ((ProJ (b,a,p)) * (((ProJ (b,a,q)) ") * ((ProJ (a,b,p)) "))) * (ProJ (a,b,q)) by VECTSP_1:10
.= (((ProJ (b,a,p)) * ((ProJ (b,a,q)) ")) * ((ProJ (a,b,p)) ")) * (ProJ (a,b,q)) by GROUP_1:def 3
.= ((ProJ (b,q,p)) * ((ProJ (a,b,p)) ")) * (ProJ (a,b,q)) by A17, A18, Th24
.= (ProJ (b,q,p)) * ((ProJ (a,b,q)) * ((ProJ (a,b,p)) ")) by GROUP_1:def 3
.= (ProJ (b,q,p)) * (ProJ (a,p,q)) by A21, A20, Th24 ;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) ; :: thesis: verum

end;

now :: thesis: ( not q _|_ implies (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) )

assume A22: not q _|_ ; :: thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
then A23: ProJ (b,q,p) = (- ((ProJ (q,p,b)) ")) * (ProJ (p,q,b)) by A4, Th27;
A24: not p _|_ by A22, Th2;
then ProJ (a,p,q) = (- ((ProJ (p,q,a)) ")) * (ProJ (q,p,a)) by A2, Th27;
then (ProJ (a,p,q)) * (ProJ (b,q,p)) = (((ProJ (q,p,a)) * (- ((ProJ (p,q,a)) "))) * (- ((ProJ (q,p,b)) "))) * (ProJ (p,q,b)) by A23, GROUP_1:def 3
.= ((ProJ (q,p,a)) * ((- ((ProJ (p,q,a)) ")) * (- ((ProJ (q,p,b)) ")))) * (ProJ (p,q,b)) by GROUP_1:def 3
.= ((ProJ (q,p,a)) * (((ProJ (q,p,b)) ") * ((ProJ (p,q,a)) "))) * (ProJ (p,q,b)) by VECTSP_1:10
.= (((ProJ (q,p,a)) * ((ProJ (q,p,b)) ")) * ((ProJ (p,q,a)) ")) * (ProJ (p,q,b)) by GROUP_1:def 3
.= ((ProJ (q,b,a)) * ((ProJ (p,q,a)) ")) * (ProJ (p,q,b)) by A4, A22, Th24
.= (ProJ (q,b,a)) * ((ProJ (p,q,b)) * ((ProJ (p,q,a)) ")) by GROUP_1:def 3
.= (ProJ (q,b,a)) * (ProJ (p,a,b)) by A2, A24, Th24 ;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) ; :: thesis: verum

end;

hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) by A16, A5; :: thesis: verum