let c be quaternion number ; :: thesis: (- c) " = - (c " )
A1: 1q = [*1,0 *] by ARYTM_0:def 7
.= [*1,0 ,0 ,0 *] by QUATERNI:def 6, QUATERNI:91 ;
consider x1, x2, x3, x4 being Element of REAL such that
A2: c = [*x1,x2,x3,x4*] by QUA7;
A3: - c = [*(- x1),(- x2),(- x3),(- x4)*] by A2, Thc1;
A4: |.(- c).| = |.c.| by QUATERNI:72;
A6: c " = [*(((((x1 * 1) + (x2 * 0 )) + (x3 * 0 )) + (x4 * 0 )) / (|.c.| ^2 )),(((((x1 * 0 ) - (x2 * 1)) - (x3 * 0 )) + (x4 * 0 )) / (|.c.| ^2 )),(((((x1 * 0 ) + (x2 * 0 )) - (x3 * 1)) - (x4 * 0 )) / (|.c.| ^2 )),(((((x1 * 0 ) - (x2 * 0 )) + (x3 * 0 )) - (x4 * 1)) / (|.c.| ^2 ))*] by A1, A2, Def1
.= [*(x1 / (|.c.| ^2 )),(- (x2 / (|.c.| ^2 ))),(- (x3 / (|.c.| ^2 ))),(- (x4 / (|.c.| ^2 )))*] ;
(- c) " = [*((((((- x1) * 1) + ((- x2) * 0 )) + ((- x3) * 0 )) + ((- x4) * 0 )) / (|.(- c).| ^2 )),((((((- x1) * 0 ) - ((- x2) * 1)) - ((- x3) * 0 )) + ((- x4) * 0 )) / (|.(- c).| ^2 )),((((((- x1) * 0 ) + ((- x2) * 0 )) - ((- x3) * 1)) - ((- x4) * 0 )) / (|.(- c).| ^2 )),((((((- x1) * 0 ) - ((- x2) * 0 )) + ((- x3) * 0 )) - ((- x4) * 1)) / (|.(- c).| ^2 ))*] by A1, A3, Def1
.= [*(- (x1 / (|.c.| ^2 ))),(x2 / (|.c.| ^2 )),(x3 / (|.c.| ^2 )),(x4 / (|.c.| ^2 ))*] by A4 ;
then (c " ) + ((- c) " ) = [*((x1 / (|.c.| ^2 )) + (- (x1 / (|.c.| ^2 )))),((- (x2 / (|.c.| ^2 ))) + (x2 / (|.c.| ^2 ))),((- (x3 / (|.c.| ^2 ))) + (x3 / (|.c.| ^2 ))),((- (x4 / (|.c.| ^2 ))) + (x4 / (|.c.| ^2 )))*] by A6, QUATERNI:def 7
.= [*0 ,0 *] by QUATERNI:def 6, QUATERNI:91
.= 0 by ARYTM_0:def 7 ;
hence (- c) " = - (c " ) by QUATERNI:def 8; :: thesis: verum