let z1, z2 be Quaternion; ( (z1 * z2) *' = (z1 *') * (z2 *') implies (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) )
assume A1:
(z1 * z2) *' = (z1 *') * (z2 *')
; (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)
A2:
z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*]
by Th36;
A3:
z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*]
by Th36;
A4:
(z1 * z2) *' = [*(Rea (z1 * z2)),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*]
by Th36;
A5: (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 A2, A3, Def9
.=
[*(((((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)))*]
;
A6: (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 A4, Lm17
.=
[*(((((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 Lm17
.=
[*(((((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 Lm17
.=
[*(((((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 Lm17
.=
[*(((((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)))*]
;
A7:
Im1 ((z1 *') * (z2 *')) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))
by A5, Th16;
Im1 ((z1 * z2) *') = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2))
by A6, Th16;
hence
(Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)
by A1, A7; verum