let r be Quaternion; :: 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
A1: 1q = [*q0,q1,q2,q3*] and
A2: r = [*r0,r1,r2,r3*] and
A3: 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;
A4: 1q = [*jj,(In (0,REAL))*] by ARYTM_0:def 5
.= [*jj,0,0,0*] by QUATERNI:91 ;
then A5: q0 = jj by A1, QUATERNI:12;
A6: q1 = 0 by A1, A4, QUATERNI:12;
A7: q2 = 0 by A1, A4, QUATERNI:12;
A8: q3 = 0 by A1, A4, QUATERNI:12;
A9: Rea r = r0 by A2, QUATERNI:23;
A10: Im1 r = r1 by A2, QUATERNI:23;
A11: Im2 r = r2 by A2, QUATERNI:23;
A12: Im3 r = r3 by A2, QUATERNI:23;
r " = [*(r0 / (|.r.| ^2)),(- (r1 / (|.r.| ^2))),(- (r2 / (|.r.| ^2))),(- (r3 / (|.r.| ^2)))*] by A3, A5, A6, A7, A8;
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 A9, A10, A11, A12, QUATERNI:23; :: thesis: verum