let z1, z2 be quaternion number ; :: thesis: (z1 - z2) *' = (z1 *' ) - (z2 *' )
A1: ( z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] & z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] & (- 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;
A2: (z1 *' ) - (z2 *' ) = (z1 *' ) + ((- z2) *' ) by Th55
.= [*((Rea z1) + (Rea (- z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by A1, Def7
.= [*((Rea z1) + (- (Rea z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th41
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) - (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th41
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) - (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th41
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) - (- (Im3 z2)))*] by Th41
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) + (Im3 z2))*] ;
(z1 - z2) *' = [*((Rea z1) - (Rea z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by A1, Lm20
.= [*((Rea z1) - (Rea z2)),(- ((Im1 z1) - (Im1 z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by Lm20
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),(- ((Im2 z1) - (Im2 z2))),(- (Im3 (z1 - z2)))*] by Lm20
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),(- ((Im3 z1) - (Im3 z2)))*] by Lm20 ;
hence (z1 - z2) *' = (z1 *' ) - (z2 *' ) by A2; :: thesis: verum