let z1, z2 be quaternion number ; (z1 - z2) *' = (z1 *') - (z2 *')
A1:
z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*]
by Th43;
A2:
(- z2) *' = [*(Rea (- z2)),(- (Im1 (- z2))),(- (Im2 (- z2))),(- (Im3 (- z2)))*]
by Th43;
A3:
(z1 - z2) *' = [*(Rea (z1 - z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*]
by Th43;
A4: (z1 *') - (z2 *') =
(z1 *') + ((- z2) *')
by Th55
.=
[*((Rea z1) + (Rea (- z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*]
by A1, A2, Def7
.=
[*((Rea z1) + (- (Rea z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*]
by Th41
.=
[*((Rea z1) - (Rea z2)),((- (Im1 z1)) - (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*]
by Th41
.=
[*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) - (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 (- z2))))*]
by Th41
.=
[*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) - (- (Im3 z2)))*]
by Th41
.=
[*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) + (Im3 z2))*]
;
(z1 - z2) *' =
[*((Rea z1) - (Rea z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*]
by A3, Th42
.=
[*((Rea z1) - (Rea z2)),(- ((Im1 z1) - (Im1 z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*]
by Th42
.=
[*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),(- ((Im2 z1) - (Im2 z2))),(- (Im3 (z1 - z2)))*]
by Th42
.=
[*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),(- ((Im3 z1) - (Im3 z2)))*]
by Th42
;
hence
(z1 - z2) *' = (z1 *') - (z2 *')
by A4; verum