let c1, c2 be Quaternion; (- c1) * c2 = - (c1 * c2)
consider x1, y1, w1, z1 being Element of REAL such that
A1:
c1 = [*x1,y1,w1,z1*]
by Lm1;
consider x2, y2, w2, z2 being Element of REAL such that
A2:
c2 = [*x2,y2,w2,z2*]
by Lm1;
A3: (- c1) * c2 =
[*(- x1),(- y1),(- w1),(- z1)*] * [*x2,y2,w2,z2*]
by A1, A2, Th4
.=
[*(((((- x1) * x2) - ((- y1) * y2)) - ((- w1) * w2)) - ((- z1) * z2)),(((((- x1) * y2) + ((- y1) * x2)) + ((- w1) * z2)) - ((- z1) * w2)),(((((- x1) * w2) + (x2 * (- w1))) + (y2 * (- z1))) - (z2 * (- y1))),(((((- x1) * z2) + ((- z1) * x2)) + ((- y1) * w2)) - ((- w1) * y2))*]
by QUATERNI:def 10
.=
[*((((- (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)),((((- (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)),((((- (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)),((((- (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2))*]
;
c1 * c2 = [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)),((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)),((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)),((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*]
by A1, A2, QUATERNI:def 10;
then ((- c1) * c2) + (c1 * c2) =
[*(((((- (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)) + ((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2))),(((((- (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)) + ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2))),(((((- (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)) + ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1))),(((((- (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2)) + ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))*]
by A3, QUATERNI:def 7
.=
[*(In (0,REAL)),(In (0,REAL))*]
by QUATERNI:91
.=
0
by ARYTM_0:def 5
;
hence
(- c1) * c2 = - (c1 * c2)
by QUATERNI:def 8; verum