thus
Cayley-Dickson N_Real is associative
Cayley-Dickson N_Real is commutative proof
let x,
y,
z be
Element of
(Cayley-Dickson N_Real);
GROUP_1:def 3 (x * y) * z = x * (y * z)
consider x1,
x2 being
Element of
N_Real such that A1:
x = <%x1,x2%>
by Th12;
consider y1,
y2 being
Element of
N_Real such that A2:
y = <%y1,y2%>
by Th12;
consider z1,
z2 being
Element of
N_Real such that A3:
z = <%z1,z2%>
by Th12;
set a1 =
(x1 * y1) - ((y2 *') * x2);
set b1 =
(x1 * y2) + ((y1 *') * x2);
set a2 =
(y1 * z1) - ((z2 *') * y2);
set b2 =
(y1 * z2) + ((z1 *') * y2);
A4:
y * z = <%((y1 * z1) - ((z2 *') * y2)),((y1 * z2) + ((z1 *') * y2))%>
by A2, A3, Def9;
x * y = <%((x1 * y1) - ((y2 *') * x2)),((x1 * y2) + ((y1 *') * x2))%>
by A1, A2, Def9;
hence (x * y) * z =
<%((((x1 * y1) - ((y2 *') * x2)) * z1) - ((z2 *') * ((x1 * y2) + ((y1 *') * x2)))),((((x1 * y1) - ((y2 *') * x2)) * z2) + ((z1 *') * ((x1 * y2) + ((y1 *') * x2))))%>
by A3, Def9
.=
<%((x1 * ((y1 * z1) - ((z2 *') * y2))) - ((((y1 * z2) + ((z1 *') * y2)) *') * x2)),((x1 * ((y1 * z2) + ((z1 *') * y2))) + ((((y1 * z1) - ((z2 *') * y2)) *') * x2))%>
.=
x * (y * z)
by A1, A4, Def9
;
verum
end;
let x, y be Element of (Cayley-Dickson N_Real); GROUP_1:def 12 x * y = y * x
consider x1, x2 being Element of N_Real such that
A5:
x = <%x1,x2%>
by Th12;
consider y1, y2 being Element of N_Real such that
A6:
y = <%y1,y2%>
by Th12;
thus x * y =
<%((x1 * y1) - ((y2 *') * x2)),((x1 * y2) + ((y1 *') * x2))%>
by A5, A6, Def9
.=
<%((y1 * x1) - ((x2 *') * y2)),((y1 * x2) + ((x1 *') * y2))%>
.=
y * x
by A5, A6, Def9
; verum