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))*] & z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] & (z1 * z2) *' = [*(Rea (z1 * z2)),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] ) by Th43;
then A4: (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 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)))*] ;
A5: (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 A3, Lm16
.= [*(((((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 Lm16
.= [*(((((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 Lm16
.= [*(((((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 Lm16
.= [*(((((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)))*] ;
A6: Im1 ((z1 *' ) * (z2 *' )) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by A4, Th23;
Im1 ((z1 * z2) *' ) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2)) by A5, Th23;
hence contradiction by A1, A2, A6; :: thesis: verum