let q, r be Quaternion; :: thesis: ( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) )
consider q0, q1, q2, q3 being Element of REAL such that
A1: q = [*q0,q1,q2,q3*] by Lm1;
consider r0, r1, r2, r3 being Element of REAL such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
A3: Rea q = q0 by A1, QUATERNI:23;
A4: Im1 q = q1 by A1, QUATERNI:23;
A5: Im2 q = q2 by A1, QUATERNI:23;
A6: Im3 q = q3 by A1, QUATERNI:23;
A7: Rea r = r0 by A2, QUATERNI:23;
A8: Im1 r = r1 by A2, QUATERNI:23;
A9: Im2 r = r2 by A2, QUATERNI:23;
A10: Im3 r = r3 by A2, QUATERNI:23;
q / 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 A1, A2, Def1;
hence ( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) ) by A3, A4, A5, A6, A7, A8, A9, A10, QUATERNI:23; :: thesis: verum