let r be quaternion number ; :: thesis: ( Rea (r " ) = (Rea r) / (|.r.| ^2 ) & Im1 (r " ) = - ((Im1 r) / (|.r.| ^2 )) & Im2 (r " ) = - ((Im2 r) / (|.r.| ^2 )) & Im3 (r " ) = - ((Im3 r) / (|.r.| ^2 )) )
consider q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL such that
W1: 1q = [*q0,q1,q2,q3*] and
W2: r = [*r0,r1,r2,r3*] and
W3: r " = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] by Def1;
A2: 1q = [*1,0 *] by ARYTM_0:def 7
.= [*1,0 ,0 ,0 *] by QUATERNI:def 6, QUATERNI:91 ;
X: ( q0 = 1 & q1 = 0 & q2 = 0 & q3 = 0 ) by A2, W1, QUATERNI:12;
A4: ( Rea r = r0 & Im1 r = r1 & Im2 r = r2 & Im3 r = r3 ) by W2, QUATERNI:23;
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 W3, X
.= [*(r0 / (|.r.| ^2 )),(- (r1 / (|.r.| ^2 ))),(- (r2 / (|.r.| ^2 ))),(- (r3 / (|.r.| ^2 )))*] ;
hence ( Rea (r " ) = (Rea r) / (|.r.| ^2 ) & Im1 (r " ) = - ((Im1 r) / (|.r.| ^2 )) & Im2 (r " ) = - ((Im2 r) / (|.r.| ^2 )) & Im3 (r " ) = - ((Im3 r) / (|.r.| ^2 )) ) by QUATERNI:23, A4; :: thesis: verum