let z3, z be Quaternion; ( z is Real implies z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] )
assume A1:
z is Real
; z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*]
then A2:
Im3 z = 0
by Lm1;
A3:
z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*]
proof
reconsider z9 =
z * z3 as
Quaternion ;
set z1 =
[*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*];
A4:
Im1 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] =
((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))
by QUATERNI:23
.=
Im1 z9
by QUATERNI:97
;
A5:
Im2 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] =
((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))
by QUATERNI:23
.=
Im2 z9
by QUATERNI:97
;
A6:
Im3 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] =
((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3))
by QUATERNI:23
.=
Im3 z9
by QUATERNI:97
;
Rea [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] =
((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))
by QUATERNI:23
.=
Rea z9
by QUATERNI:97
;
hence
z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*]
by A4, A5, A6, QUATERNI:25;
verum
end;
( Im1 z = 0 & Im2 z = 0 )
by A1, Lm1;
hence
z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*]
by A2, A3; verum