let z be quaternion number ; :: thesis: - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>)
set z9 = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*];
A1: [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) by Lm20;
[*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] + z = [*((Rea [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Rea z)),((Im1 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Lm14
.= [*((- (Rea z)) + (Rea z)),((Im1 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th23
.= [*0,((- (Im1 z)) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th23
.= [*0,0,((- (Im2 z)) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th23
.= [*0,0,0,((- (Im3 z)) + (Im3 z))*] by Th23
.= 0 by Lm7 ;
hence - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) by A1, Def8; :: thesis: verum