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