let z1, z2 be Quaternion; ( 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 Lm21
.=
(((Rea z1) * (Rea z2)) + 0q) + 0q
by Lm22, Lm23, A1
.=
((Rea z1) * (Rea z2)) + 0q
by Lm22
;
consider y1, y2, y3, y4 being Real such that
A3:
( 0q = [*y1,y2,y3,y4*] & ((Rea z1) * (Rea z2)) + 0q = [*(((Rea z1) * (Rea z2)) + y1),y2,y3,y4*] )
by Def18;
reconsider RR = (Rea z1) * (Rea z2), zz = 0 as Element of REAL by XREAL_0:def 1;
( y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 )
by Th5, A3, Lm6;
then
((Rea z1) * (Rea z2)) + 0q = [*RR,zz*]
by A3, Lm3;
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 Lm18, A2, A1; verum