let z1, z2 be quaternion number ; ( Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 implies ( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) )
assume A1:
( Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 )
; ( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) )
A2: z1 * z2 =
(((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) * <i>)) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) * <j>)) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) * <k>)
by Lm22
.=
(((Rea z1) * (Rea z2)) + 0q) + 0q
by Lm23, Lm24, A1
.=
((Rea z1) * (Rea z2)) + 0q
by Lm23
;
consider y1, y2, y3, y4 being Element of REAL such that
A3:
( 0q = [*y1,y2,y3,y4*] & ((Rea z1) * (Rea z2)) + 0q = [*(((Rea z1) * (Rea z2)) + y1),y2,y3,y4*] )
by Def19;
( y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 )
by Th12, A3, Lm7;
then
((Rea z1) * (Rea z2)) + 0q = [*((Rea z1) * (Rea z2)),0*]
by A3, Lm4;
then
((Rea z1) * (Rea z2)) + 0q = (Rea z1) * (Rea z2)
by ARYTM_0:def 5;
hence
( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) )
by Lm19, A2, A1; verum