let z be Quaternion; :: thesis: ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) )
A1: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th17;
A2: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th36;
A3: Im1 (z *') = - (Im1 z) by A2, Th16;
A4: Im2 (z *') = - (Im2 z) by A2, Th16;
A5: Im3 (z *') = - (Im3 z) by A2, Th16;
set zz = z *' ;
- (z *') = [*(- (Rea (z *'))),(- (Im1 (z *'))),(- (Im2 (z *'))),(- (Im3 (z *')))*] by Th55;
then - (z *') = [*(- (Rea z)),(Im1 z),(Im2 z),(Im3 z)*] by A2, Th16, A3, A4, A5;
then z - (z *') = [*((Rea z) + (- (Rea z))),((Im1 z) + (Im1 z)),((Im2 z) + (Im2 z)),((Im3 z) + (Im3 z))*] by A1, Def6
.= [*0,(2 * (Im1 z)),(2 * (Im2 z)),(2 * (Im3 z))*] ;
hence ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) ) by Th16; :: thesis: verum