let r be Quaternion; ( r <> 0 implies r * (r ") = 1 )
assume A1:
r <> 0
; r * (r ") = 1
consider r0, r1, r2, r3 being Element of REAL such that
A2:
r = [*r0,r1,r2,r3*]
by Lm1;
A3: 1q =
[*jj,(In (0,REAL))*]
by ARYTM_0:def 5
.=
[*1,0,0,0*]
by QUATERNI:91
;
A4:
Rea r = r0
by A2, QUATERNI:23;
A5:
Im1 r = r1
by A2, QUATERNI:23;
A6:
Im2 r = r2
by A2, QUATERNI:23;
A7:
Im3 r = r3
by A2, 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 2;
A9: r " =
[*(((((r0 * 1) + (r1 * 0)) + (r2 * 0)) + (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) - (r1 * 1)) - (r2 * 0)) + (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) + (r1 * 0)) - (r2 * 1)) - (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) - (r1 * 0)) + (r2 * 0)) - (r3 * jj)) / (|.r.| ^2))*]
by A2, A3, Def1, Lm5
.=
[*(r0 / (|.r.| ^2)),((- r1) / (|.r.| ^2)),((- r2) / (|.r.| ^2)),((- r3) / (|.r.| ^2))*]
;
|.r.| <> 0
by A1, Th10;
then A10:
|.r.| ^2 > 0
by SQUARE_1:12;
r * (r ") =
[*((((r0 * (r0 / (|.r.| ^2))) - (r1 * ((- r1) / (|.r.| ^2)))) - (r2 * ((- r2) / (|.r.| ^2)))) - (r3 * ((- r3) / (|.r.| ^2)))),((((r0 * ((- r1) / (|.r.| ^2))) + (r1 * (r0 / (|.r.| ^2)))) + (r2 * ((- r3) / (|.r.| ^2)))) - (r3 * ((- r2) / (|.r.| ^2)))),((((r0 * ((- r2) / (|.r.| ^2))) + ((r0 / (|.r.| ^2)) * r2)) + (((- r1) / (|.r.| ^2)) * r3)) - (((- r3) / (|.r.| ^2)) * r1)),((((r0 * ((- r3) / (|.r.| ^2))) + (r3 * (r0 / (|.r.| ^2)))) + (r1 * ((- r2) / (|.r.| ^2)))) - (r2 * ((- r1) / (|.r.| ^2))))*]
by A2, A9, QUATERNI:def 10
.=
[*((|.r.| ^2) / (|.r.| ^2)),0,0,0*]
by A8
.=
[*1,0,0,0*]
by A10, XCMPLX_1:60
.=
[*jj,(In (0,REAL))*]
by QUATERNI:91
.=
1
by ARYTM_0:def 5
;
hence
r * (r ") = 1
; verum