thus
Cayley-Dickson (Cayley-Dickson N_Real) is associative
not Cayley-Dickson (Cayley-Dickson N_Real) is commutative proof
let a,
b,
c be
Element of
(Cayley-Dickson (Cayley-Dickson N_Real));
GROUP_1:def 3 (a * b) * c = a * (b * c)
consider a1,
b1,
a2,
b2 being
Element of
N_Real such that A1:
a = <%<%a1,b1%>,<%a2,b2%>%>
by Th13;
consider a3,
b3,
a4,
b4 being
Element of
N_Real such that A2:
b = <%<%a3,b3%>,<%a4,b4%>%>
by Th13;
consider a5,
b5,
a6,
b6 being
Element of
N_Real such that A3:
c = <%<%a5,b5%>,<%a6,b6%>%>
by Th13;
set x1 =
(<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>);
set x2 =
(<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>);
set x3 =
(<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>);
set x4 =
(<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>);
set x11 =
((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)));
set x12 =
((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)));
set x21 =
((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)));
set x22 =
((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)));
set x31 =
((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)));
set x32 =
((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)));
set x41 =
((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)));
set x42 =
((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)));
A4:
<%a1,b1%> * <%a3,b3%> = <%((a1 * a3) - ((b3 *') * b1)),((a1 * b3) + ((a3 *') * b1))%>
by Def9;
A5:
<%a4,b4%> *' = <%(a4 *'),(- b4)%>
by Def9;
A6:
<%(a4 *'),(- b4)%> * <%a2,b2%> = <%(((a4 *') * a2) - ((b2 *') * (- b4))),(((a4 *') * b2) + ((a2 *') * (- b4)))%>
by Def9;
A7:
(<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>) = <%(((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))),(((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4))))%>
by A4, A5, A6, Th28;
A8:
<%a1,b1%> * <%a4,b4%> = <%((a1 * a4) - ((b4 *') * b1)),((a1 * b4) + ((a4 *') * b1))%>
by Def9;
A9:
<%a3,b3%> *' = <%(a3 *'),(- b3)%>
by Def9;
A10:
<%(a3 *'),(- b3)%> * <%a2,b2%> = <%(((a3 *') * a2) - ((b2 *') * (- b3))),(((a3 *') * b2) + ((a2 *') * (- b3)))%>
by Def9;
A11:
(<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>) = <%(((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))),(((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))%>
by A8, A9, A10, Def9;
A12:
<%a3,b3%> * <%a5,b5%> = <%((a3 * a5) - ((b5 *') * b3)),((a3 * b5) + ((a5 *') * b3))%>
by Def9;
A13:
<%a6,b6%> *' = <%(a6 *'),(- b6)%>
by Def9;
A14:
<%(a6 *'),(- b6)%> * <%a4,b4%> = <%(((a6 *') * a4) - ((b4 *') * (- b6))),(((a6 *') * b4) + ((a4 *') * (- b6)))%>
by Def9;
A15:
(<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>) = <%(((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))),(((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))%>
by A12, A13, A14, Th28;
A16:
<%a3,b3%> * <%a6,b6%> = <%((a3 * a6) - ((b6 *') * b3)),((a3 * b6) + ((a6 *') * b3))%>
by Def9;
A17:
<%a5,b5%> *' = <%(a5 *'),(- b5)%>
by Def9;
A18:
<%(a5 *'),(- b5)%> * <%a4,b4%> = <%(((a5 *') * a4) - ((b4 *') * (- b5))),(((a5 *') * b4) + ((a4 *') * (- b5)))%>
by Def9;
A19:
(<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>) = <%(((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))),(((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))%>
by A16, A17, A18, Def9;
A20:
<%a1,b1%> * ((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) = <%((a1 * (((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6))))) - (((((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))) *') * b1)),((a1 * (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))) + (((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b1))%>
by A15, Def9;
((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) *' = <%((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *'),(- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))))%>
by A19, Def9;
then A21:
(((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) *') * <%a2,b2%> = <%((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * a2) - ((b2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))))),((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b2) + ((a2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))))))%>
by Def9;
A22:
((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a5,b5%> = <%(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a5) - ((b5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))),(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b5) + ((a5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4))))))%>
by A7, Def9;
(<%a6,b6%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>)) = <%(((a6 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b6))),(((a6 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b6)))%>
by A11, A13, Def9;
then A23:
(((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a5,b5%>) - ((<%a6,b6%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))) =
<%((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a5) - ((b5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) - (((a6 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b6)))),((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b5) + ((a5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) - (((a6 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b6))))%>
by A22, Th28
.=
<%(((a1 * (((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6))))) - (((((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))) *') * b1)) - ((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * a2) - ((b2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))))))),(((a1 * (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))) + (((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b1)) - ((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b2) + ((a2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))))))%>
.=
(<%a1,b1%> * ((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>))) - ((((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) *') * <%a2,b2%>)
by A20, A21, Th28
;
A24:
<%a1,b1%> * ((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) = <%((a1 * (((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5))))) - (((((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))) *') * b1)),((a1 * (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))) + (((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b1))%>
by A19, Def9;
((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) *' = <%((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *'),(- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))))%>
by A15, Def9;
then A25:
(((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) *') * <%a2,b2%> = <%((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * a2) - ((b2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))))),((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b2) + ((a2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))))))%>
by Def9;
A26:
((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a6,b6%> = <%(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a6) - ((b6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))),(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b6) + ((a6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4))))))%>
by A7, Def9;
(<%a5,b5%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>)) = <%(((a5 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b5))),(((a5 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b5)))%>
by A17, A11, Def9;
then A27:
(((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a6,b6%>) + ((<%a5,b5%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))) =
<%((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a6) - ((b6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) + (((a5 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b5)))),((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b6) + ((a6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) + (((a5 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b5))))%>
by A26, Def9
.=
<%(((a1 * (((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5))))) - (((((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))) *') * b1)) + ((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * a2) - ((b2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))))))),(((a1 * (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))) + (((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b1)) + ((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b2) + ((a2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))))))%>
.=
(<%a1,b1%> * ((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>))) + ((((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) *') * <%a2,b2%>)
by A24, A25, Def9
;
A28:
b * c = <%((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)),((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>))%>
by A2, A3, Def9;
a * b = <%((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)),((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))%>
by A1, A2, Def9;
hence (a * b) * c =
<%((((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a5,b5%>) - ((<%a6,b6%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>)))),((((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a6,b6%>) + ((<%a5,b5%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))))%>
by A3, Def9
.=
a * (b * c)
by A1, A28, A23, A27, Def9
;
verum
end;
take
<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>
; GROUP_1:def 12 not for b1 being Element of the carrier of (Cayley-Dickson (Cayley-Dickson N_Real)) holds <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%> * b1 = b1 * <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>
take
<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>
; not <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> = <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>
<%(0. N_Real),(1. N_Real)%> <> <%(0. N_Real),(- (1. N_Real))%>
by Th3;
hence
not <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> = <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>
by Th30, Th31, Th3; verum