let r be quaternion number ; :: 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 QUA7;
A3: 1q = [*1,0 *] by ARYTM_0:def 7
.= [*1,0 ,0 ,0 *] by QUATERNI:def 6, QUATERNI:91 ;
A4: ( Rea r = r0 & Im1 r = r1 & Im2 r = r2 & Im3 r = r3 ) by A2, QUATERNI:23;
A5: 0 <= ((((Rea r) ^2 ) + ((Im1 r) ^2 )) + ((Im2 r) ^2 )) + ((Im3 r) ^2 ) by QUATERNI:74;
A6: |.r.| ^2 = (((r0 ^2 ) + (r1 ^2 )) + (r2 ^2 )) + (r3 ^2 ) by A4, A5, SQUARE_1:def 4;
A7: 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 * 1)) / (|.r.| ^2 ))*] by A2, A3, Def1
.= [*(r0 / (|.r.| ^2 )),((- r1) / (|.r.| ^2 )),((- r2) / (|.r.| ^2 )),((- r3) / (|.r.| ^2 ))*] ;
|.r.| <> 0 by A1, Th40;
then A8: |.r.| ^2 > 0 by SQUARE_1:74;
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, A7, QUATERNI:def 10
.= [*((|.r.| ^2 ) / (|.r.| ^2 )),0 ,0 ,0 *] by A6
.= [*1,0 ,0 ,0 *] by A8, XCMPLX_1:60
.= [*1,0 *] by QUATERNI:def 6, QUATERNI:91
.= 1 by ARYTM_0:def 7 ;
hence r * (r " ) = 1 ; :: thesis: verum