let z1, z2 be quaternion number ; ( (z1 * z2) *' = (z1 *') * (z2 *') implies (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) )
assume A2:
(z1 * z2) *' = (z1 *') * (z2 *')
; (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)
A3:
z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*]
by Th43;
A4:
z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*]
by Th43;
A5:
(z1 * z2) *' = [*(Rea (z1 * z2)),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*]
by Th43;
A6: (z1 *') * (z2 *') =
[*(((((Rea z1) * (Rea z2)) - ((- (Im1 z1)) * (- (Im1 z2)))) - ((- (Im2 z1)) * (- (Im2 z2)))) - ((- (Im3 z1)) * (- (Im3 z2)))),(((((Rea z1) * (- (Im1 z2))) + ((- (Im1 z1)) * (Rea z2))) + ((- (Im2 z1)) * (- (Im3 z2)))) - ((- (Im3 z1)) * (- (Im2 z2)))),(((((Rea z1) * (- (Im2 z2))) + ((Rea z2) * (- (Im2 z1)))) + ((- (Im1 z2)) * (- (Im3 z1)))) - ((- (Im3 z2)) * (- (Im1 z1)))),(((((Rea z1) * (- (Im3 z2))) + ((- (Im3 z1)) * (Rea z2))) + ((- (Im1 z1)) * (- (Im2 z2)))) - ((- (Im2 z1)) * (- (Im1 z2))))*]
by A3, A4, Def10
.=
[*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),((((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))),((((- ((Rea z1) * (Im2 z2))) - ((Rea z2) * (Im2 z1))) + ((Im1 z2) * (Im3 z1))) - ((Im3 z2) * (Im1 z1))),((((- ((Rea z1) * (Im3 z2))) - ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*]
;
A7: (z1 * z2) *' =
[*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*]
by A5, Lm18
.=
[*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*]
by Lm18
.=
[*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))),(- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))),(- (Im3 (z1 * z2)))*]
by Lm18
.=
[*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))),(- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))),(- (((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))))*]
by Lm18
.=
[*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),((((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2))),((((- ((Rea z1) * (Im2 z2))) - ((Im2 z1) * (Rea z2))) - ((Im3 z1) * (Im1 z2))) + ((Im1 z1) * (Im3 z2))),((((- ((Rea z1) * (Im3 z2))) - ((Im3 z1) * (Rea z2))) - ((Im1 z1) * (Im2 z2))) + ((Im2 z1) * (Im1 z2)))*]
;
A8:
Im1 ((z1 *') * (z2 *')) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))
by A6, Th23;
Im1 ((z1 * z2) *') = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2))
by A7, Th23;
hence
(Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)
by A2, A8; verum