let r be Quaternion; :: thesis: ( r <> 0 implies r * (r ") = 1 )
assume A1: r <> 0 ; :: thesis: 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 ; :: thesis: verum