let z1, z2 be quaternion number ; :: thesis: ( (Im2 z1) * (Im3 z2) <> (Im3 z1) * (Im2 z2) implies (z1 * z2) *' <> (z1 *' ) * (z2 *' ) )
assume A1: (Im2 z1) * (Im3 z2) <> (Im3 z1) * (Im2 z2) ; :: thesis: (z1 * z2) *' <> (z1 *' ) * (z2 *' )
assume A2: (z1 * z2) *' = (z1 *' ) * (z2 *' ) ; :: thesis: contradiction
A3: z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] by Th43;
A4: z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th43;
A5: (z1 * z2) *' = [*(Rea (z1 * z2)),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] by Th43;
A6: (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)))),(((((Rea z1) * (- (Im2 z2))) + ((Rea z2) * (- (Im2 z1)))) + ((- (Im1 z2)) * (- (Im3 z1)))) - ((- (Im3 z2)) * (- (Im1 z1)))),(((((Rea z1) * (- (Im3 z2))) + ((- (Im3 z1)) * (Rea z2))) + ((- (Im1 z1)) * (- (Im2 z2)))) - ((- (Im2 z1)) * (- (Im1 z2))))*] by A3, A4, Def10
.= [*(((((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))),((((- ((Rea z1) * (Im2 z2))) - ((Rea z2) * (Im2 z1))) + ((Im1 z2) * (Im3 z1))) - ((Im3 z2) * (Im1 z1))),((((- ((Rea z1) * (Im3 z2))) - ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*] ;
A7: (z1 * z2) *' = [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] by A5, Lm18
.= [*(((((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)))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] by Lm18
.= [*(((((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)))),(- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))),(- (Im3 (z1 * z2)))*] by Lm18
.= [*(((((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)))),(- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))),(- (((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))))*] by Lm18
.= [*(((((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))),((((- ((Rea z1) * (Im2 z2))) - ((Im2 z1) * (Rea z2))) - ((Im3 z1) * (Im1 z2))) + ((Im1 z1) * (Im3 z2))),((((- ((Rea z1) * (Im3 z2))) - ((Im3 z1) * (Rea z2))) - ((Im1 z1) * (Im2 z2))) + ((Im2 z1) * (Im1 z2)))*] ;
A8: Im1 ((z1 *' ) * (z2 *' )) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by A6, Th23;
Im1 ((z1 * z2) *' ) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2)) by A7, Th23;
hence contradiction by A1, A2, A8; :: thesis: verum