let r be quaternion number ; ( 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 =
[*1,0 *]
by ARYTM_0:def 7
.=
[*1,0 ,0 ,0 *]
by QUATERNI:91
;
then A5:
q0 = 1
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 * 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 A3, A5, A6, A7, A8
.=
[*(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 A9, A10, A11, A12, QUATERNI:23; verum