let r be quaternion number ; ( r <> 0 implies |.r.| <> 0 )
assume A1:
r <> 0
; |.r.| <> 0
assume A2:
|.r.| = 0
; contradiction
consider r0, r1, r2, r3 being Element of REAL such that
A3:
r = [*r0,r1,r2,r3*]
by Lm1;
A4:
Rea r = r0
by A3, QUATERNI:23;
A5:
Im1 r = r1
by A3, QUATERNI:23;
A6:
Im2 r = r2
by A3, QUATERNI:23;
A7:
Im3 r = r3
by A3, QUATERNI:23;
0 <= ((((Rea r) ^2 ) + ((Im1 r) ^2 )) + ((Im2 r) ^2 )) + ((Im3 r) ^2 )
by QUATERNI:74;
then A8:
|.r.| ^2 = (((r0 ^2 ) + (r1 ^2 )) + (r2 ^2 )) + (r3 ^2 )
by A4, A5, A6, A7, SQUARE_1:def 4;
then A9:
r0 = 0
by A2, Lm3;
A10:
r1 = 0
by A2, A8, Lm3;
A11:
r2 = 0
by A2, A8, Lm3;
r3 = 0
by A2, A8, Lm3;
then r =
[*0 ,0 *]
by A3, A9, A10, A11, QUATERNI:91
.=
0
by ARYTM_0:def 7
;
hence
contradiction
by A1; verum