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