let z be quaternion number ; :: thesis: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]
<i> = [*0 ,1,0 ,0 *] by Def6', Lmx;
then z *' = (((Rea z) + [*((- (Im1 z)) * 0 ),((- (Im1 z)) * 1),((- (Im1 z)) * 0 ),((- (Im1 z)) * 0 )*]) + ((- (Im2 z)) * <j> )) + ((- (Im3 z)) * <k> ) by Def21
.= (((Rea z) + [*0 ,(- (Im1 z)),0 ,0 *]) + [*((- (Im2 z)) * 0 ),((- (Im2 z)) * 0 ),((- (Im2 z)) * 1),((- (Im2 z)) * 0 )*]) + ((- (Im3 z)) * <k> ) by Def21
.= (((Rea z) + [*0 ,(- (Im1 z)),0 ,0 *]) + [*0 ,0 ,(- (Im2 z)),0 *]) + [*((- (Im3 z)) * 0 ),((- (Im3 z)) * 0 ),((- (Im3 z)) * 0 ),((- (Im3 z)) * 1)*] by Def21
.= ([*((Rea z) + 0 ),(- (Im1 z)),0 ,0 *] + [*0 ,0 ,(- (Im2 z)),0 *]) + [*0 ,0 ,0 ,(- (Im3 z))*] by Def19
.= [*((Rea z) + 0 ),((- (Im1 z)) + 0 ),(0 + (- (Im2 z))),(0 + 0 )*] + [*0 ,0 ,0 ,(- (Im3 z))*] by Def7
.= [*((Rea z) + 0 ),((- (Im1 z)) + 0 ),((- (Im2 z)) + 0 ),(0 + (- (Im3 z)))*] by Def7 ;
hence z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] ; :: thesis: verum