let z1, z2 be quaternion number ; ( |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " implies z1 = z2 )
assume that
A1:
|.z1.| = |.z2.|
and
A2:
|.z1.| <> 0
and
A3:
z1 " = z2 "
; z1 = z2
A4:
|.z1.| ^2 <> 0
by A2, XCMPLX_1:6;
A5:
Im3 (z1 " ) = - ((Im3 z1) / (|.z1.| ^2 ))
by QUATERN2:29;
A6:
- ((Im3 z1) / (|.z1.| ^2 )) = - ((Im3 z2) / (|.z2.| ^2 ))
by A3, A5, QUATERN2:29;
A7:
Im3 z1 = Im3 z2
by A1, A6, A4, XCMPLX_1:53;
A8:
Im2 (z1 " ) = - ((Im2 z1) / (|.z1.| ^2 ))
by QUATERN2:29;
A9:
- ((Im2 z1) / (|.z1.| ^2 )) = - ((Im2 z2) / (|.z2.| ^2 ))
by A3, A8, QUATERN2:29;
A10:
Im2 z1 = Im2 z2
by A1, A9, A4, XCMPLX_1:53;
A11:
Im1 (z1 " ) = - ((Im1 z1) / (|.z1.| ^2 ))
by QUATERN2:29;
A12:
- ((Im1 z1) / (|.z1.| ^2 )) = - ((Im1 z2) / (|.z2.| ^2 ))
by A3, A11, QUATERN2:29;
A13:
Im1 z1 = Im1 z2
by A1, A12, A4, XCMPLX_1:53;
A14:
Rea (z1 " ) = (Rea z1) / (|.z1.| ^2 )
by QUATERN2:29;
A15:
(Rea z1) / (|.z1.| ^2 ) = (Rea z2) / (|.z2.| ^2 )
by A3, A14, QUATERN2:29;
A16:
Rea z1 = Rea z2
by A1, A15, A4, XCMPLX_1:53;
thus
z1 = z2
by A16, A13, A10, A7, QUATERNI:25; verum