let c be quaternion number ; :: thesis: - c = (- 1q ) * c
consider x, y, w, z being Element of REAL such that
A1: c = [*x,y,w,z*] by Lm1;
A2: c + [*(- x),(- y),(- w),(- z)*] = [*(x + (- x)),(y + (- y)),(w + (- w)),(z + (- z))*] by A1, QUATERNI:def 7
.= [*0 ,0 *] by QUATERNI:91
.= 0 by ARYTM_0:def 7 ;
1q = [*1,0 *] by ARYTM_0:def 7
.= [*1,0 ,0 ,0 *] by QUATERNI:91 ;
then 1q + [*(- 1),0 ,0 ,0 *] = [*(1 + (- 1)),(0 + 0 ),(0 + 0 ),(0 + 0 )*] by QUATERNI:def 7
.= [*0 ,0 *] by QUATERNI:91
.= 0 by ARYTM_0:def 7 ;
then (- 1q ) * c = [*(- 1),0 ,0 ,0 *] * [*x,y,w,z*] by A1, QUATERNI:def 8
.= [*(((((- 1) * x) - (0 * y)) - (0 * w)) - (0 * z)),(((((- 1) * y) + (0 * x)) + (0 * z)) - (0 * w)),(((((- 1) * w) + (x * 0 )) + (y * 0 )) - (z * 0 )),(((((- 1) * z) + (0 * x)) + (0 * w)) - (0 * y))*] by QUATERNI:def 10 ;
hence - c = (- 1q ) * c by A2, QUATERNI:def 8; :: thesis: verum