:: QUATERN2 semantic presentation

begin

Lm1:  for g being quaternion number ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
by QUATERNI:7;

Lm2:  for a, b, c, d being real number holds (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0
by QUATERNI:74;

Lm3:  for a, b, c, d being real number st (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
by QUATERNI:96;


definition
:: original: 0q
redefine func 0q  ->  Element of QUATERNION ;
coherence
 0q is Element of QUATERNION by QUATERNI:def_2;
end;

definition
:: original: 1q
redefine func 1q  ->  Element of QUATERNION ;
coherence
 1q is Element of QUATERNION by QUATERNI:def_2;
end;

theorem Th1: :: QUATERN2:1
for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
proof
let x, y, z, w be Real; ::_thesis: [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
 <i> = [*0,1*] by ARYTM_0:def_5;
then  <i> = [*0,1,0,0*] by QUATERNI:91;
then A1: y * <i> = [*(y * 0),(y * 1),(y * 0),(y * 0)*] by QUATERNI:def_21
.= [*0,y,0,0*] ;
A2: z * <j> = [*(z * 0),(z * 0),(z * 1),(y * 0)*] by QUATERNI:def_21
.= [*0,0,z,0*] ;
A3: w * <k> = [*(w * 0),(w * 0),(w * 0),(w * 1)*] by QUATERNI:def_21
.= [*0,0,0,w*] ;
x + (y * <i>) = [*(x + 0),y,0,0*] by A1, QUATERNI:def_19
.= [*x,y,0,0*] ;
then (x + (y * <i>)) + (z * <j>) = [*(x + 0),(y + 0),(0 + z),(0 + 0)*] by A2, QUATERNI:def_7
.= [*x,y,z,0*] ;
then  ((x + (y * <i>)) + (z * <j>)) + (w * <k>) = [*(x + 0),(y + 0),(0 + z),(0 + w)*] by A3, QUATERNI:def_7;
hence  [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>) ; ::_thesis: verum
end;

theorem Th2: :: QUATERN2:2
for c1, c2, c3 being quaternion number holds (c1 + c2) + c3 = c1 + (c2 + c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: (c1 + c2) + c3 = c1 + (c2 + c3)
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;
consider x3, y3, w3, z3 being Element of REAL  such that
A3: c3 = [*x3,y3,w3,z3*] by Lm1;
A4: c2 + c3 = [*(x2 + x3),(y2 + y3),(w2 + w3),(z2 + z3)*] by A2, A3, QUATERNI:def_7;
(c1 + c2) + c3 = [*(x1 + x2),(y1 + y2),(w1 + w2),(z1 + z2)*] + [*x3,y3,w3,z3*] by A1, A2, A3, QUATERNI:def_7
.= [*((x1 + x2) + x3),((y1 + y2) + y3),((w1 + w2) + w3),((z1 + z2) + z3)*] by QUATERNI:def_7
.= [*(x1 + (x2 + x3)),(y1 + (y2 + y3)),(w1 + (w2 + w3)),(z1 + (z2 + z3))*]
.= c1 + (c2 + c3) by A1, A4, QUATERNI:def_7 ;
hence  (c1 + c2) + c3 = c1 + (c2 + c3) ; ::_thesis: verum
end;

theorem Th3: :: QUATERN2:3
for c being quaternion number holds c + 0q = c
proof
let c be quaternion number ; ::_thesis: c + 0q = c
A1: 0q = [*0,0*] by ARYTM_0:def_5
.= [*0,0,0,0*] by QUATERNI:91 ;
consider x, y, w, z being Element of REAL  such that
A2: c = [*x,y,w,z*] by Lm1;
c + 0q = [*(x + 0),(y + 0),(w + 0),(z + 0)*] by A1, A2, QUATERNI:def_7
.= [*x,y,w,z*] ;
hence  c + 0q = c by A2; ::_thesis: verum
end;

theorem Th4: :: QUATERN2:4
for x1, x2, x3, x4 being Element of REAL holds - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*]
proof
let x1, x2, x3, x4 be Element of REAL ; ::_thesis: - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*]
[*x1,x2,x3,x4*] + [*(- x1),(- x2),(- x3),(- x4)*] = [*(x1 - x1),(x2 - x2),(x3 - x3),(x4 - x4)*] by QUATERNI:def_7
.= [*0,0*] by QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*] by QUATERNI:def_8; ::_thesis: verum
end;

theorem :: QUATERN2:5
for x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL holds [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*]
proof
let x1, x2, x3, x4, y1, y2, y3, y4 be Element of REAL ; ::_thesis: [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*]
[*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*x1,x2,x3,x4*] + [*(- y1),(- y2),(- y3),(- y4)*] by Th4
.= [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*] by QUATERNI:def_7 ;
hence  [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*] ; ::_thesis: verum
end;

theorem :: QUATERN2:6
for c1, c2, c3 being quaternion number holds (c1 - c2) + c3 = (c1 + c3) - c2 by Th2;

theorem Th7: :: QUATERN2:7
for c1, c2 being quaternion number holds c1 = (c1 + c2) - c2
proof
let c1, c2 be quaternion number ; ::_thesis: c1 = (c1 + c2) - c2
thus (c1 + c2) - c2 = c1 + (c2 - c2) by Th2
.= c1 + 0q by QUATERNI:def_8
.= c1 by Th3 ; ::_thesis: verum
end;

theorem :: QUATERN2:8
for c1, c2 being quaternion number holds c1 = (c1 - c2) + c2
proof
let c1, c2 be quaternion number ; ::_thesis: c1 = (c1 - c2) + c2
thus (c1 - c2) + c2 = (c1 + c2) - c2 by Th2
.= c1 by Th7 ; ::_thesis: verum
end;

theorem Th9: :: QUATERN2:9
for c being quaternion number
for x1 being Element of REAL holds (- x1) * c = - (x1 * c)
proof
let c be quaternion number ; ::_thesis: for x1 being Element of REAL holds (- x1) * c = - (x1 * c)
let x1 be Element of REAL ; ::_thesis: (- x1) * c = - (x1 * c)
consider x, y, w, z being Element of REAL  such that
A1: c = [*x,y,w,z*] by Lm1;
A2: (- x1) * c = [*((- x1) * x),((- x1) * y),((- x1) * w),((- x1) * z)*] by A1, QUATERNI:def_21
.= [*(- (x1 * x)),(- (x1 * y)),(- (x1 * w)),(- (x1 * z))*] ;
A3: - (x1 * c) = - [*(x1 * x),(x1 * y),(x1 * w),(x1 * z)*] by A1, QUATERNI:def_21;
[*(x1 * x),(x1 * y),(x1 * w),(x1 * z)*] + [*(- (x1 * x)),(- (x1 * y)),(- (x1 * w)),(- (x1 * z))*] = [*((x1 * x) + (- (x1 * x))),((x1 * y) + (- (x1 * y))),((x1 * w) + (- (x1 * w))),((x1 * z) + (- (x1 * z)))*] by QUATERNI:def_7
.= [*0,0*] by QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  (- x1) * c = - (x1 * c) by A2, A3, QUATERNI:def_8; ::_thesis: verum
end;

definition
let q be quaternion number ;
:: original: |.
redefine func|.q.| ->  Element of REAL ;
coherence
 |.q.| is Element of REAL ;
end;

definition
:: original: <i>
redefine func <i>  ->  Element of QUATERNION ;
coherence
 <i> is Element of QUATERNION by QUATERNI:def_2;
end;

Lm4:  for r being quaternion number st |.r.| = 0 holds
r = 0
by QUATERNI:66;

theorem Th10: :: QUATERN2:10
for r being quaternion number st r <> 0 holds
|.r.| > 0
proof
let r be quaternion number ; ::_thesis: ( r <> 0 implies |.r.| > 0 )
assume  r <> 0 ; ::_thesis: |.r.| > 0
then  |.r.| <> 0 by Lm4;
hence  |.r.| > 0 by QUATERNI:67; ::_thesis: verum
end;

theorem Th11: :: QUATERN2:11
0q = [*0,0,0,0*]
proof
thus  0q = [*0,0*] by ARYTM_0:def_5
.= [*0,0,0,0*] by QUATERNI:91 ; ::_thesis: verum
end;

theorem :: QUATERN2:12
for r being quaternion number holds 0q * r = 0
proof
let r be quaternion number ; ::_thesis: 0q * r = 0
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL  such that
A1: 0 = [*x1,x2,x3,x4*] and
 r = [*y1,y2,y3,y4*] and
A2: 0q * r = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by QUATERNI:def_10;
A3: x1 = 0 by A1, Th11, QUATERNI:12;
A4: x2 = 0 by A1, Th11, QUATERNI:12;
A5: x3 = 0 by A1, Th11, QUATERNI:12;
 x4 = 0 by A1, Th11, QUATERNI:12;
hence  0q * r = 0 by A2, A3, A4, A5, Th11; ::_thesis: verum
end;

theorem :: QUATERN2:13
for r being quaternion number holds r * 0q = 0
proof
let r be quaternion number ; ::_thesis: r * 0q = 0
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL  such that
 r = [*x1,x2,x3,x4*] and
A1: 0 = [*y1,y2,y3,y4*] and
A2: r * 0q = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by QUATERNI:def_10;
A3: y1 = 0 by A1, Th11, QUATERNI:12;
A4: y2 = 0 by A1, Th11, QUATERNI:12;
A5: y3 = 0 by A1, Th11, QUATERNI:12;
 y4 = 0 by A1, Th11, QUATERNI:12;
hence  r * 0q = 0 by A2, A3, A4, A5, Th11; ::_thesis: verum
end;

theorem Th14: :: QUATERN2:14
for c being quaternion number holds c * 1q = c
proof
let c be quaternion number ; ::_thesis: c * 1q = c
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
consider x, y, w, z being Element of REAL  such that
A2: c = [*x,y,w,z*] by Lm1;
c * 1q = [*((((x * 1) - (y * 0)) - (w * 0)) - (z * 0)),((((x * 0) + (y * 1)) + (w * 0)) - (z * 0)),((((x * 0) + (1 * w)) + (0 * z)) - (0 * y)),((((x * 0) + (z * 1)) + (y * 0)) - (w * 0))*] by A1, A2, QUATERNI:def_10
.= [*x,y,w,z*] ;
hence  c * 1q = c by A2; ::_thesis: verum
end;

theorem Th15: :: QUATERN2:15
for c being quaternion number holds 1q * c = c
proof
let c be quaternion number ; ::_thesis: 1q * c = c
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
consider x, y, w, z being Element of REAL  such that
A2: c = [*x,y,w,z*] by Lm1;
1q * c = [*((((x * 1) - (y * 0)) - (w * 0)) - (z * 0)),((((x * 0) + (y * 1)) + (w * 0)) - (z * 0)),((((x * 0) + (1 * w)) + (0 * z)) - (0 * y)),((((x * 0) + (z * 1)) + (y * 0)) - (w * 0))*] by A1, A2, QUATERNI:def_10
.= [*x,y,w,z*] ;
hence  1q * c = c by A2; ::_thesis: verum
end;

theorem Th16: :: QUATERN2:16
for c1, c2, c3 being quaternion number holds (c1 * c2) * c3 = c1 * (c2 * c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: (c1 * c2) * c3 = c1 * (c2 * c3)
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;
consider x3, y3, w3, z3 being Element of REAL  such that
A3: c3 = [*x3,y3,w3,z3*] by Lm1;
A4: (c1 * c2) * c3 = [*((((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))*] * c3 by A1, A2, QUATERNI:def_10
.= [*((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * x3) - (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * y3)) - (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * w3)) - (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * z3)),((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * y3) + (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * x3)) + (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * z3)) - (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * w3)),((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * w3) + (x3 * ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)))) + (y3 * ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))) - (z3 * ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)))),((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * z3) + (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * x3)) + (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * w3)) - (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * y3))*] by A3, QUATERNI:def_10
.= [*((((((((x1 * x2) * x3) - ((y1 * y2) * x3)) - ((w1 * w2) * x3)) - ((z1 * z2) * x3)) - (((((x1 * y2) * y3) + ((y1 * x2) * y3)) + ((w1 * z2) * y3)) - ((z1 * w2) * y3))) - (((((x1 * w2) * w3) + ((x2 * w1) * w3)) + ((y2 * z1) * w3)) - ((z2 * y1) * w3))) - (((((x1 * z2) * z3) + ((z1 * x2) * z3)) + ((y1 * w2) * z3)) - ((w1 * y2) * z3))),((((((((x1 * x2) * y3) - ((y1 * y2) * y3)) - ((w1 * w2) * y3)) - ((z1 * z2) * y3)) + (((((x1 * y2) * x3) + ((y1 * x2) * x3)) + ((w1 * z2) * x3)) - ((z1 * w2) * x3))) + (((((x1 * w2) * z3) + ((x2 * w1) * z3)) + ((y2 * z1) * z3)) - ((z2 * y1) * z3))) - (((((x1 * z2) * w3) + ((z1 * x2) * w3)) + ((y1 * w2) * w3)) - ((w1 * y2) * w3))),((((((((x1 * x2) * w3) - ((y1 * y2) * w3)) - ((w1 * w2) * w3)) - ((z1 * z2) * w3)) + (((((x3 * x1) * w2) + ((x3 * x2) * w1)) + ((x3 * y2) * z1)) - ((x3 * z2) * y1))) + (((((y3 * x1) * z2) + ((y3 * z1) * x2)) + ((y3 * y1) * w2)) - ((y3 * w1) * y2))) - (((((z3 * x1) * y2) + ((z3 * y1) * x2)) + ((z3 * w1) * z2)) - ((z3 * z1) * w2))),((((((((x1 * x2) * z3) - ((y1 * y2) * z3)) - ((w1 * w2) * z3)) - ((z1 * z2) * z3)) + (((((x1 * z2) * x3) + ((z1 * x2) * x3)) + ((y1 * w2) * x3)) - ((w1 * y2) * x3))) + (((((x1 * y2) * w3) + ((y1 * x2) * w3)) + ((w1 * z2) * w3)) - ((z1 * w2) * w3))) - (((((x1 * w2) * y3) + ((x2 * w1) * y3)) + ((y2 * z1) * y3)) - ((z2 * y1) * y3)))*] ;
c1 * (c2 * c3) = c1 * [*((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)),((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)),((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)),((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))*] by A2, A3, QUATERNI:def_10
.= [*((((x1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3))) - (y1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)))) - (w1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))) - (z1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))),((((x1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))) + (y1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)))) + (w1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))) - (z1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))),((((x1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2))) + (((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)) * w1)) + (((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)) * z1)) - (((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)) * y1)),((((x1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))) + (z1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)))) + (y1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))) - (w1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))))*] by A1, QUATERNI:def_10
.= (c1 * c2) * c3 by A4 ;
hence  (c1 * c2) * c3 = c1 * (c2 * c3) ; ::_thesis: verum
end;

theorem Th17: :: QUATERN2:17
for c1, c2, c3 being quaternion number holds c1 * (c2 + c3) = (c1 * c2) + (c1 * c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: c1 * (c2 + c3) = (c1 * c2) + (c1 * c3)
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;
consider x3, y3, w3, z3 being Element of REAL  such that
A3: c3 = [*x3,y3,w3,z3*] by Lm1;
A4: c1 * (c2 + c3) = c1 * [*(x2 + x3),(y2 + y3),(w2 + w3),(z2 + z3)*] by A2, A3, QUATERNI:def_7
.= [*((((x1 * (x2 + x3)) - (y1 * (y2 + y3))) - (w1 * (w2 + w3))) - (z1 * (z2 + z3))),((((x1 * (y2 + y3)) + (y1 * (x2 + x3))) + (w1 * (z2 + z3))) - (z1 * (w2 + w3))),((((x1 * (w2 + w3)) + ((x2 + x3) * w1)) + ((y2 + y3) * z1)) - ((z2 + z3) * y1)),((((x1 * (z2 + z3)) + (z1 * (x2 + x3))) + (y1 * (w2 + w3))) - (w1 * (y2 + y3)))*] by A1, QUATERNI:def_10
.= [*(((((x1 * x2) + (x1 * x3)) - ((y1 * y2) + (y1 * y3))) - ((w1 * w2) + (w1 * w3))) - ((z1 * z2) + (z1 * z3))),(((((x1 * y2) + (x1 * y3)) + ((y1 * x2) + (y1 * x3))) + ((w1 * z2) + (w1 * z3))) - ((z1 * w2) + (z1 * w3))),(((((x1 * w2) + (x1 * w3)) + ((x2 * w1) + (x3 * w1))) + ((y2 * z1) + (y3 * z1))) - ((z2 * y1) + (z3 * y1))),(((((x1 * z2) + (x1 * z3)) + ((z1 * x2) + (z1 * x3))) + ((y1 * w2) + (y1 * w3))) - ((w1 * y2) + (w1 * y3)))*] ;
(c1 * c2) + (c1 * c3) = [*((((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 * c3) by A1, A2, 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))*] + [*((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)),((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)),((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)),((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3))*] by A1, A3, QUATERNI:def_10
.= [*(((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) + ((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3))),(((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) + ((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3))),(((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) + ((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1))),(((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) + ((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3)))*] by QUATERNI:def_7 ;
hence  c1 * (c2 + c3) = (c1 * c2) + (c1 * c3) by A4; ::_thesis: verum
end;

theorem Th18: :: QUATERN2:18
for c1, c2, c3 being quaternion number holds (c1 + c2) * c3 = (c1 * c3) + (c2 * c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: (c1 + c2) * c3 = (c1 * c3) + (c2 * c3)
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;
consider x3, y3, w3, z3 being Element of REAL  such that
A3: c3 = [*x3,y3,w3,z3*] by Lm1;
A4: (c1 + c2) * c3 = [*(x1 + x2),(y1 + y2),(w1 + w2),(z1 + z2)*] * c3 by A1, A2, QUATERNI:def_7
.= [*(((((x1 + x2) * x3) - ((y1 + y2) * y3)) - ((w1 + w2) * w3)) - ((z1 + z2) * z3)),(((((x1 + x2) * y3) + ((y1 + y2) * x3)) + ((w1 + w2) * z3)) - ((z1 + z2) * w3)),(((((x1 + x2) * w3) + (x3 * (w1 + w2))) + (y3 * (z1 + z2))) - (z3 * (y1 + y2))),(((((x1 + x2) * z3) + ((z1 + z2) * x3)) + ((y1 + y2) * w3)) - ((w1 + w2) * y3))*] by A3, QUATERNI:def_10
.= [*(((((x1 * x3) + (x2 * x3)) - ((y1 * y3) + (y2 * y3))) - ((w1 * w3) + (w2 * w3))) - ((z1 * z3) + (z2 * z3))),(((((x1 * y3) + (x2 * y3)) + ((y1 * x3) + (y2 * x3))) + ((w1 * z3) + (w2 * z3))) - ((z1 * w3) + (z2 * w3))),(((((x1 * w3) + (x2 * w3)) + ((x3 * w1) + (x3 * w2))) + ((y3 * z1) + (y3 * z2))) - ((z3 * y1) + (z3 * y2))),(((((x1 * z3) + (x2 * z3)) + ((z1 * x3) + (z2 * x3))) + ((y1 * w3) + (y2 * w3))) - ((w1 * y3) + (w2 * y3)))*] ;
(c1 * c3) + (c2 * c3) = [*((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)),((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)),((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)),((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3))*] + (c2 * c3) by A1, A3, QUATERNI:def_10
.= [*((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)),((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)),((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)),((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3))*] + [*((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)),((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)),((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)),((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))*] by A2, A3, QUATERNI:def_10
.= [*(((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)) + ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3))),(((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)) + ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))),(((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)) + ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2))),(((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3)) + ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))*] by QUATERNI:def_7 ;
hence  (c1 + c2) * c3 = (c1 * c3) + (c2 * c3) by A4; ::_thesis: verum
end;

theorem Th19: :: QUATERN2:19
for c being quaternion number holds - c = (- 1q) * c
proof
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_5 ;
1q = [*1,0*] by ARYTM_0:def_5
.= [*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_5 ;
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
end;

theorem Th20: :: QUATERN2:20
for c1, c2 being quaternion number holds (- c1) * c2 = - (c1 * c2)
proof
let c1, c2 be quaternion number ; ::_thesis: (- 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
.= [*0,0*] by QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  (- c1) * c2 = - (c1 * c2) by QUATERNI:def_8; ::_thesis: verum
end;

theorem Th21: :: QUATERN2:21
for c1, c2 being quaternion number holds c1 * (- c2) = - (c1 * c2)
proof
let c1, c2 be quaternion number ; ::_thesis: 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
.= [*0,0*] by QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  c1 * (- c2) = - (c1 * c2) by QUATERNI:def_8; ::_thesis: verum
end;

theorem Th22: :: QUATERN2:22
for c1, c2 being quaternion number holds (- c1) * (- c2) = c1 * c2
proof
let c1, c2 be quaternion number ; ::_thesis: (- 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;
 - c1 = [*(- x1),(- y1),(- w1),(- z1)*] by A1, Th4;
then (- c1) * (- c2) = [*(- x1),(- y1),(- w1),(- z1)*] * [*(- x2),(- y2),(- w2),(- z2)*] by 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 by A1, A2, QUATERNI:def_10 ;
hence  (- c1) * (- c2) = c1 * c2 ; ::_thesis: verum
end;

theorem Th23: :: QUATERN2:23
for c1, c2, c3 being quaternion number holds (c1 - c2) * c3 = (c1 * c3) - (c2 * c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: (c1 - c2) * c3 = (c1 * c3) - (c2 * c3)
 (c1 - c2) * c3 = (c1 * c3) + ((- c2) * c3) by Th18;
hence  (c1 - c2) * c3 = (c1 * c3) - (c2 * c3) by Th20; ::_thesis: verum
end;

theorem Th24: :: QUATERN2:24
for c1, c2, c3 being quaternion number holds c1 * (c2 - c3) = (c1 * c2) - (c1 * c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: c1 * (c2 - c3) = (c1 * c2) - (c1 * c3)
 c1 * (c2 - c3) = (c1 * c2) + (c1 * (- c3)) by Th17;
hence  c1 * (c2 - c3) = (c1 * c2) - (c1 * c3) by Th21; ::_thesis: verum
end;

theorem Th25: :: QUATERN2:25
for x1, x2, x3, x4 being Element of REAL holds [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*]
proof
let x1, x2, x3, x4 be Element of REAL ; ::_thesis: [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*]
set c = [*x1,x2,x3,x4*];
A1: Rea [*x1,x2,x3,x4*] = x1 by QUATERNI:23;
A2: Im1 [*x1,x2,x3,x4*] = x2 by QUATERNI:23;
A3: Im2 [*x1,x2,x3,x4*] = x3 by QUATERNI:23;
 Im3 [*x1,x2,x3,x4*] = x4 by QUATERNI:23;
hence  [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*] by A1, A2, A3, QUATERNI:43; ::_thesis: verum
end;

theorem :: QUATERN2:26
for c being quaternion number holds (c *') *' = c
proof
let c be quaternion number ; ::_thesis: (c *') *' = c
A1: Rea (c *') = Rea c by QUATERNI:44;
A2: Im1 (c *') = - (Im1 c) by QUATERNI:44;
A3: Im2 (c *') = - (Im2 c) by QUATERNI:44;
 Im3 (c *') = - (Im3 c) by QUATERNI:44;
then (c *') *' = [*(Rea c),(- (- (Im1 c))),(- (- (Im2 c))),(- (- (Im3 c)))*] by A1, A2, A3, QUATERNI:43
.= c by QUATERNI:24 ;
hence  (c *') *' = c ; ::_thesis: verum
end;

definition
let q, r be quaternion number ;
consider q0, q1, q2, q3 being Element of REAL  such that
A1: q = [*q0,q1,q2,q3*] by Lm1;
consider r0, r1, r2, r3 being Element of REAL  such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
funcq / r ->  set  means :Def1: :: QUATERN2:def 1
 ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & it = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] );
existence
 ex b1 being set ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] )
proof
take  [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ; ::_thesis: ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] )
thus  ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) holds
b1 = b2
proof
let c1, c2 be number ; ::_thesis: ( ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & c1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & c2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) implies c1 = c2 )
given q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL  such that A3: q = [*q0,q1,q2,q3*] and
A4: r = [*r0,r1,r2,r3*] and
A5: c1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ; ::_thesis: ( for q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL holds
( not q = [*q0,q1,q2,q3*] or not r = [*r0,r1,r2,r3*] or not c2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) or c1 = c2 )
given q09, q19, q29, q39, r09, r19, r29, r39 being Element of REAL  such that A6: q = [*q09,q19,q29,q39*] and
A7: r = [*r09,r19,r29,r39*] and
A8: c2 = [*(((((r09 * q09) + (r19 * q19)) + (r29 * q29)) + (r39 * q39)) / (|.r.| ^2)),(((((r09 * q19) - (r19 * q09)) - (r29 * q39)) + (r39 * q29)) / (|.r.| ^2)),(((((r09 * q29) + (r19 * q39)) - (r29 * q09)) - (r39 * q19)) / (|.r.| ^2)),(((((r09 * q39) - (r19 * q29)) + (r29 * q19)) - (r39 * q09)) / (|.r.| ^2))*] ; ::_thesis: c1 = c2
A9: q0 = q09 by A3, A6, QUATERNI:12;
A10: q1 = q19 by A3, A6, QUATERNI:12;
A11: q2 = q29 by A3, A6, QUATERNI:12;
A12: q3 = q39 by A3, A6, QUATERNI:12;
A13: r0 = r09 by A4, A7, QUATERNI:12;
A14: r1 = r19 by A4, A7, QUATERNI:12;
A15: r2 = r29 by A4, A7, QUATERNI:12;
 r3 = r39 by A4, A7, QUATERNI:12;
hence  c1 = c2 by A5, A8, A9, A10, A11, A12, A13, A14, A15; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines / QUATERN2:def_1_:_
 for q, r being quaternion number
for b3 being set holds
( b3 = q / r iff ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b3 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) );

registration
let q, r be quaternion number ;
clusterq / r ->  quaternion ;
coherence
 q / r is quaternion
proof
 ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & q / r = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) by Def1;
hence  q / r is quaternion ; ::_thesis: verum
end;
end;

definition
let q, r be quaternion number ;
:: original: /
redefine funcq / r ->  Element of QUATERNION ;
coherence
 q / r is Element of QUATERNION by QUATERNI:def_2;
end;

theorem :: QUATERN2:27
for q, r being quaternion number holds q / r = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2)) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2)) * <i>)) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2)) * <j>)) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2)) * <k>)
proof
let q, r be quaternion number ; ::_thesis: q / r = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2)) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2)) * <i>)) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2)) * <j>)) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2)) * <k>)
consider q0, q1, q2, q3 being Element of REAL  such that
A1: q = [*q0,q1,q2,q3*] by Lm1;
consider r0, r1, r2, r3 being Element of REAL  such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
A3: Rea q = q0 by A1, QUATERNI:23;
A4: Im1 q = q1 by A1, QUATERNI:23;
A5: Im2 q = q2 by A1, QUATERNI:23;
A6: Im3 q = q3 by A1, QUATERNI:23;
A7: Rea r = r0 by A2, QUATERNI:23;
A8: Im1 r = r1 by A2, QUATERNI:23;
A9: Im2 r = r2 by A2, QUATERNI:23;
A10: Im3 r = r3 by A2, QUATERNI:23;
q / r = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] by A1, A2, Def1
.= (((((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)) + ((((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)) * <i>)) + ((((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)) * <j>)) + ((((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2)) * <k>) by Th1 ;
hence  q / r = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2)) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2)) * <i>)) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2)) * <j>)) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2)) * <k>) by A3, A4, A5, A6, A7, A8, A9, A10; ::_thesis: verum
end;

definition
let c be quaternion number ;
funcc "  ->  quaternion number  equals :: QUATERN2:def 2
1q / c;
coherence
 1q / c is quaternion number ;
end;

:: deftheorem  defines " QUATERN2:def_2_:_
 for c being quaternion number holds c " = 1q / c;

definition
let r be quaternion number ;
:: original: "
redefine funcr "  ->  Element of QUATERNION ;
coherence
 r " is Element of QUATERNION ;
end;

theorem :: QUATERN2:28
for r being quaternion number holds r " = ((((Rea r) / (|.r.| ^2)) - (((Im1 r) / (|.r.| ^2)) * <i>)) - (((Im2 r) / (|.r.| ^2)) * <j>)) - (((Im3 r) / (|.r.| ^2)) * <k>)
proof
let r be quaternion number ; ::_thesis: r " = ((((Rea r) / (|.r.| ^2)) - (((Im1 r) / (|.r.| ^2)) * <i>)) - (((Im2 r) / (|.r.| ^2)) * <j>)) - (((Im3 r) / (|.r.| ^2)) * <k>)
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
consider q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL  such that
A2: 1q = [*q0,q1,q2,q3*] and
A3: r = [*r0,r1,r2,r3*] and
A4: r " = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] by Def1;
A5: Rea r = r0 by A3, QUATERNI:23;
A6: Im1 r = r1 by A3, QUATERNI:23;
A7: Im2 r = r2 by A3, QUATERNI:23;
A8: q0 = 1 by A1, A2, QUATERNI:12;
A9: q1 = 0 by A1, A2, QUATERNI:12;
A10: q2 = 0 by A1, A2, QUATERNI:12;
 q3 = 0 by A1, A2, QUATERNI:12;
then r " = (((r0 / (|.r.| ^2)) + ((- (r1 / (|.r.| ^2))) * <i>)) + ((- (r2 / (|.r.| ^2))) * <j>)) + ((- (r3 / (|.r.| ^2))) * <k>) by Th1, A4, A8, A9, A10
.= (((r0 / (|.r.| ^2)) + (- ((r1 / (|.r.| ^2)) * <i>))) + ((- (r2 / (|.r.| ^2))) * <j>)) + ((- (r3 / (|.r.| ^2))) * <k>) by Th9
.= (((r0 / (|.r.| ^2)) - ((r1 / (|.r.| ^2)) * <i>)) + (- ((r2 / (|.r.| ^2)) * <j>))) + ((- (r3 / (|.r.| ^2))) * <k>) by Th9
.= (((r0 / (|.r.| ^2)) - ((r1 / (|.r.| ^2)) * <i>)) - ((r2 / (|.r.| ^2)) * <j>)) + (- ((r3 / (|.r.| ^2)) * <k>)) by Th9 ;
hence  r " = ((((Rea r) / (|.r.| ^2)) - (((Im1 r) / (|.r.| ^2)) * <i>)) - (((Im2 r) / (|.r.| ^2)) * <j>)) - (((Im3 r) / (|.r.| ^2)) * <k>) by A3, A5, A6, A7, QUATERNI:23; ::_thesis: verum
end;

theorem :: QUATERN2:29
for r being quaternion number holds
( Rea (r ") = (Rea r) / (|.r.| ^2) & Im1 (r ") = - ((Im1 r) / (|.r.| ^2)) & Im2 (r ") = - ((Im2 r) / (|.r.| ^2)) & Im3 (r ") = - ((Im3 r) / (|.r.| ^2)) )
proof
let r be quaternion number ; ::_thesis: ( Rea (r ") = (Rea r) / (|.r.| ^2) & Im1 (r ") = - ((Im1 r) / (|.r.| ^2)) & Im2 (r ") = - ((Im2 r) / (|.r.| ^2)) & Im3 (r ") = - ((Im3 r) / (|.r.| ^2)) )
consider q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL  such that
A1: 1q = [*q0,q1,q2,q3*] and
A2: r = [*r0,r1,r2,r3*] and
A3: r " = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] by Def1;
A4: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
then A5: q0 = 1 by A1, QUATERNI:12;
A6: q1 = 0 by A1, A4, QUATERNI:12;
A7: q2 = 0 by A1, A4, QUATERNI:12;
A8: q3 = 0 by A1, A4, QUATERNI:12;
A9: Rea r = r0 by A2, QUATERNI:23;
A10: Im1 r = r1 by A2, QUATERNI:23;
A11: Im2 r = r2 by A2, QUATERNI:23;
A12: Im3 r = r3 by A2, QUATERNI:23;
 r " = [*(r0 / (|.r.| ^2)),(- (r1 / (|.r.| ^2))),(- (r2 / (|.r.| ^2))),(- (r3 / (|.r.| ^2)))*] by A3, A5, A6, A7, A8;
hence  ( Rea (r ") = (Rea r) / (|.r.| ^2) & Im1 (r ") = - ((Im1 r) / (|.r.| ^2)) & Im2 (r ") = - ((Im2 r) / (|.r.| ^2)) & Im3 (r ") = - ((Im3 r) / (|.r.| ^2)) ) by A9, A10, A11, A12, QUATERNI:23; ::_thesis: verum
end;

theorem :: QUATERN2:30
for q, r being quaternion number holds
( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) )
proof
let q, r be quaternion number ; ::_thesis: ( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) )
consider q0, q1, q2, q3 being Element of REAL  such that
A1: q = [*q0,q1,q2,q3*] by Lm1;
consider r0, r1, r2, r3 being Element of REAL  such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
A3: Rea q = q0 by A1, QUATERNI:23;
A4: Im1 q = q1 by A1, QUATERNI:23;
A5: Im2 q = q2 by A1, QUATERNI:23;
A6: Im3 q = q3 by A1, QUATERNI:23;
A7: Rea r = r0 by A2, QUATERNI:23;
A8: Im1 r = r1 by A2, QUATERNI:23;
A9: Im2 r = r2 by A2, QUATERNI:23;
A10: Im3 r = r3 by A2, QUATERNI:23;
 q / r = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] by A1, A2, Def1;
hence  ( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) ) by A3, A4, A5, A6, A7, A8, A9, A10, QUATERNI:23; ::_thesis: verum
end;

theorem Th31: :: QUATERN2:31
for r being quaternion number st r <> 0 holds
r * (r ") = 1
proof
let r be quaternion number ; ::_thesis: ( r <> 0 implies r * (r ") = 1 )
assume A1: r <> 0 ; ::_thesis: r * (r ") = 1
consider r0, r1, r2, r3 being Element of REAL  such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
A3: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
A4: Rea r = r0 by A2, QUATERNI:23;
A5: Im1 r = r1 by A2, QUATERNI:23;
A6: Im2 r = r2 by A2, QUATERNI:23;
A7: Im3 r = r3 by A2, QUATERNI:23;
 0 <= ((((Rea r) ^2) + ((Im1 r) ^2)) + ((Im2 r) ^2)) + ((Im3 r) ^2) by QUATERNI:74;
then A8: |.r.| ^2 = (((r0 ^2) + (r1 ^2)) + (r2 ^2)) + (r3 ^2) by A4, A5, A6, A7, SQUARE_1:def_2;
A9: r " = [*(((((r0 * 1) + (r1 * 0)) + (r2 * 0)) + (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) - (r1 * 1)) - (r2 * 0)) + (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) + (r1 * 0)) - (r2 * 1)) - (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) - (r1 * 0)) + (r2 * 0)) - (r3 * 1)) / (|.r.| ^2))*] by A2, A3, Def1
.= [*(r0 / (|.r.| ^2)),((- r1) / (|.r.| ^2)),((- r2) / (|.r.| ^2)),((- r3) / (|.r.| ^2))*] ;
 |.r.| <> 0 by A1, Th10;
then A10: |.r.| ^2 > 0 by SQUARE_1:12;
r * (r ") = [*((((r0 * (r0 / (|.r.| ^2))) - (r1 * ((- r1) / (|.r.| ^2)))) - (r2 * ((- r2) / (|.r.| ^2)))) - (r3 * ((- r3) / (|.r.| ^2)))),((((r0 * ((- r1) / (|.r.| ^2))) + (r1 * (r0 / (|.r.| ^2)))) + (r2 * ((- r3) / (|.r.| ^2)))) - (r3 * ((- r2) / (|.r.| ^2)))),((((r0 * ((- r2) / (|.r.| ^2))) + ((r0 / (|.r.| ^2)) * r2)) + (((- r1) / (|.r.| ^2)) * r3)) - (((- r3) / (|.r.| ^2)) * r1)),((((r0 * ((- r3) / (|.r.| ^2))) + (r3 * (r0 / (|.r.| ^2)))) + (r1 * ((- r2) / (|.r.| ^2)))) - (r2 * ((- r1) / (|.r.| ^2))))*] by A2, A9, QUATERNI:def_10
.= [*((|.r.| ^2) / (|.r.| ^2)),0,0,0*] by A8
.= [*1,0,0,0*] by A10, XCMPLX_1:60
.= [*1,0*] by QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
hence  r * (r ") = 1 ; ::_thesis: verum
end;

theorem :: QUATERN2:32
for r being quaternion number st r <> 0 holds
(r ") * r = 1
proof
let r be quaternion number ; ::_thesis: ( r <> 0 implies (r ") * r = 1 )
assume A1: r <> 0 ; ::_thesis: (r ") * r = 1
consider r0, r1, r2, r3 being Element of REAL  such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
A3: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
A4: Rea r = r0 by A2, QUATERNI:23;
A5: Im1 r = r1 by A2, QUATERNI:23;
A6: Im2 r = r2 by A2, QUATERNI:23;
A7: Im3 r = r3 by A2, QUATERNI:23;
 0 <= ((((Rea r) ^2) + ((Im1 r) ^2)) + ((Im2 r) ^2)) + ((Im3 r) ^2) by QUATERNI:74;
then A8: |.r.| ^2 = (((r0 ^2) + (r1 ^2)) + (r2 ^2)) + (r3 ^2) by A4, A5, A6, A7, SQUARE_1:def_2;
A9: r " = [*(((((r0 * 1) + (r1 * 0)) + (r2 * 0)) + (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) - (r1 * 1)) - (r2 * 0)) + (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) + (r1 * 0)) - (r2 * 1)) - (r3 * 0)) / (|.r.| ^2)),(((((r0 * 0) - (r1 * 0)) + (r2 * 0)) - (r3 * 1)) / (|.r.| ^2))*] by A2, A3, Def1
.= [*(r0 / (|.r.| ^2)),((- r1) / (|.r.| ^2)),((- r2) / (|.r.| ^2)),((- r3) / (|.r.| ^2))*] ;
 |.r.| <> 0 by A1, Th10;
then A10: |.r.| ^2 > 0 by SQUARE_1:12;
(r ") * r = [*((((r0 * (r0 / (|.r.| ^2))) - (r1 * ((- r1) / (|.r.| ^2)))) - (r2 * ((- r2) / (|.r.| ^2)))) - (r3 * ((- r3) / (|.r.| ^2)))),((((r0 * ((- r1) / (|.r.| ^2))) + (r1 * (r0 / (|.r.| ^2)))) + (r2 * ((- r3) / (|.r.| ^2)))) - (r3 * ((- r2) / (|.r.| ^2)))),((((r0 * ((- r2) / (|.r.| ^2))) + ((r0 / (|.r.| ^2)) * r2)) + (((- r1) / (|.r.| ^2)) * r3)) - (((- r3) / (|.r.| ^2)) * r1)),((((r0 * ((- r3) / (|.r.| ^2))) + (r3 * (r0 / (|.r.| ^2)))) + (r1 * ((- r2) / (|.r.| ^2)))) - (r2 * ((- r1) / (|.r.| ^2))))*] by A2, A9, QUATERNI:def_10
.= [*((|.r.| ^2) / (|.r.| ^2)),0,0,0*] by A8
.= [*1,0,0,0*] by A10, XCMPLX_1:60
.= [*1,0*] by QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
hence  (r ") * r = 1 ; ::_thesis: verum
end;

theorem Th33: :: QUATERN2:33
for c being quaternion number st c <> 0q holds
c / c = 1q
proof
let c be quaternion number ; ::_thesis: ( c <> 0q implies c / c = 1q )
assume A1: c <> 0q ; ::_thesis: c / c = 1q
consider x1, x2, x3, x4 being Element of REAL  such that
A2: c = [*x1,x2,x3,x4*] by Lm1;
 |.c.| > 0 by A1, Th10;
then A3: |.c.| ^2 > 0 by SQUARE_1:12;
A4: Rea c = x1 by A2, QUATERNI:23;
A5: Im1 c = x2 by A2, QUATERNI:23;
A6: Im2 c = x3 by A2, QUATERNI:23;
A7: Im3 c = x4 by A2, QUATERNI:23;
A8: (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) >= 0 by Lm2;
c / c = [*(((((x1 * x1) + (x2 * x2)) + (x3 * x3)) + (x4 * x4)) / (|.c.| ^2)),(((((x1 * x2) - (x2 * x1)) - (x3 * x4)) + (x4 * x3)) / (|.c.| ^2)),(((((x1 * x3) + (x2 * x4)) - (x3 * x1)) - (x4 * x2)) / (|.c.| ^2)),(((((x1 * x4) - (x2 * x3)) + (x3 * x2)) - (x4 * x1)) / (|.c.| ^2))*] by A2, Def1
.= [*((|.c.| ^2) / (|.c.| ^2)),0,0,0*] by A4, A5, A6, A7, A8, SQUARE_1:def_2
.= [*1,0,0,0*] by A3, XCMPLX_1:60
.= [*1,0*] by QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
hence  c / c = 1q ; ::_thesis: verum
end;

theorem :: QUATERN2:34
for c being quaternion number holds (- c) " = - (c ")
proof
let c be quaternion number ; ::_thesis: (- c) " = - (c ")
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
consider x1, x2, x3, x4 being Element of REAL  such that
A2: c = [*x1,x2,x3,x4*] by Lm1;
A3: - c = [*(- x1),(- x2),(- x3),(- x4)*] by A2, Th4;
A4: |.(- c).| = |.c.| by QUATERNI:72;
A5: 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 A5, QUATERNI:def_7
.= [*0,0*] by QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  (- c) " = - (c ") by QUATERNI:def_8; ::_thesis: verum
end;

definition
func compquaternion  ->  UnOp of QUATERNION means :: QUATERN2:def 3
 for c being Element of QUATERNION holds it . c = - c;
existence
 ex b1 being UnOp of QUATERNION st
for c being Element of QUATERNION holds b1 . c = - c from FUNCT_2:sch_4();
uniqueness
 for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = - c ) & ( for c being Element of QUATERNION holds b2 . c = - c ) holds
b1 = b2 from BINOP_2:sch_1();
func addquaternion  ->  BinOp of QUATERNION means :Def4: :: QUATERN2:def 4
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 + c2;
existence
 ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 from BINOP_1:sch_4();
uniqueness
 for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 + c2 ) holds
b1 = b2 from BINOP_2:sch_2();
func diffquaternion  ->  BinOp of QUATERNION means :: QUATERN2:def 5
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 - c2;
existence
 ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 from BINOP_1:sch_4();
uniqueness
 for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 - c2 ) holds
b1 = b2 from BINOP_2:sch_2();
func multquaternion  ->  BinOp of QUATERNION means :Def6: :: QUATERN2:def 6
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 * c2;
existence
 ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 from BINOP_1:sch_4();
uniqueness
 for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 * c2 ) holds
b1 = b2 from BINOP_2:sch_2();
func divquaternion  ->  BinOp of QUATERNION means :: QUATERN2:def 7
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 / c2;
existence
 ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 from BINOP_1:sch_4();
uniqueness
 for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 / c2 ) holds
b1 = b2 from BINOP_2:sch_2();
func invquaternion  ->  UnOp of QUATERNION means :: QUATERN2:def 8
 for c being Element of QUATERNION holds it . c = c " ;
existence
 ex b1 being UnOp of QUATERNION st
for c being Element of QUATERNION holds b1 . c = c " from FUNCT_2:sch_4();
uniqueness
 for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = c " ) & ( for c being Element of QUATERNION holds b2 . c = c " ) holds
b1 = b2 from BINOP_2:sch_1();
end;

:: deftheorem  defines compquaternion QUATERN2:def_3_:_
 for b1 being UnOp of QUATERNION holds
( b1 = compquaternion iff for c being Element of QUATERNION holds b1 . c = - c );

:: deftheorem Def4 defines addquaternion QUATERN2:def_4_:_
 for b1 being BinOp of QUATERNION holds
( b1 = addquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 );

:: deftheorem  defines diffquaternion QUATERN2:def_5_:_
 for b1 being BinOp of QUATERNION holds
( b1 = diffquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 );

:: deftheorem Def6 defines multquaternion QUATERN2:def_6_:_
 for b1 being BinOp of QUATERNION holds
( b1 = multquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 );

:: deftheorem  defines divquaternion QUATERN2:def_7_:_
 for b1 being BinOp of QUATERNION holds
( b1 = divquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 );

:: deftheorem  defines invquaternion QUATERN2:def_8_:_
 for b1 being UnOp of QUATERNION holds
( b1 = invquaternion iff for c being Element of QUATERNION holds b1 . c = c " );

definition
func G_Quaternion  ->  strict addLoopStr  means :Def9: :: QUATERN2:def 9
( the carrier of it = QUATERNION & the addF of it = addquaternion & 0. it = 0q );
existence
 ex b1 being strict addLoopStr st
( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q )
proof
take  addLoopStr(# QUATERNION,addquaternion,0q #) ; ::_thesis: ( the carrier of addLoopStr(# QUATERNION,addquaternion,0q #) = QUATERNION & the addF of addLoopStr(# QUATERNION,addquaternion,0q #) = addquaternion & 0. addLoopStr(# QUATERNION,addquaternion,0q #) = 0q )
thus  ( the carrier of addLoopStr(# QUATERNION,addquaternion,0q #) = QUATERNION & the addF of addLoopStr(# QUATERNION,addquaternion,0q #) = addquaternion & 0. addLoopStr(# QUATERNION,addquaternion,0q #) = 0q ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict addLoopStr st the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q & the carrier of b2 = QUATERNION & the addF of b2 = addquaternion & 0. b2 = 0q holds
b1 = b2 ;
end;

:: deftheorem Def9 defines G_Quaternion QUATERN2:def_9_:_
 for b1 being strict addLoopStr holds
( b1 = G_Quaternion iff ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q ) );

registration
cluster G_Quaternion  ->  non empty strict ;
coherence
 not G_Quaternion is empty by Def9;
end;

registration
cluster  ->  quaternion for Element of the carrier of G_Quaternion;
coherence
 for b1 being Element of G_Quaternion holds b1 is quaternion
proof
let c be Element of G_Quaternion; ::_thesis: c is quaternion
 c in the carrier of G_Quaternion ;
then  c in QUATERNION by Def9;
hence  c is quaternion ; ::_thesis: verum
end;
end;

registration
let x, y be Element of G_Quaternion;
let a, b be quaternion number ;
identifyx + y with a + b when x = a, y = b;
compatibility
 ( x = a & y = b implies x + y = a + b )
proof
assume that
A1: x = a and
A2: y = b ; ::_thesis: x + y = a + b
reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def_2;
thus x + y = addquaternion . (a9,b9) by A1, A2, Def9
.= a + b by Def4 ; ::_thesis: verum
end;
end;

theorem Th35: :: QUATERN2:35
0. G_Quaternion = 0q by Def9;

registration
cluster G_Quaternion  ->  strict right_complementable Abelian add-associative right_zeroed ;
coherence
 ( G_Quaternion is Abelian & G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable )
proof
thus  for x, y being Element of G_Quaternion holds x + y = y + x ; :: according to RLVECT_1:def_2 ::_thesis: ( G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable )
thus  for x, y, z being Element of G_Quaternion holds (x + y) + z = x + (y + z) by Th2; :: according to RLVECT_1:def_3 ::_thesis: ( G_Quaternion is right_zeroed & G_Quaternion is right_complementable )
thus  for x being Element of G_Quaternion holds x + (0. G_Quaternion) = x :: according to RLVECT_1:def_4 ::_thesis: G_Quaternion is right_complementable
proof
let x be Element of G_Quaternion; ::_thesis: x + (0. G_Quaternion) = x
reconsider x1 = x as Element of QUATERNION by Def9;
thus x + (0. G_Quaternion) = the addF of G_Quaternion . (x1,0q) by Def9
.= addquaternion . (x1,0q) by Def9
.= x1 + 0q by Def4
.= x by Th3 ; ::_thesis: verum
end;
thus  G_Quaternion is right_complementable ::_thesis: verum
proof
let x be Element of G_Quaternion; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of QUATERNION by Def9;
reconsider y = - x1 as Element of G_Quaternion by Def9;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. G_Quaternion
thus  x + y = 0. G_Quaternion by Th35, QUATERNI:def_8; ::_thesis: verum
end;
end;
end;

registration
let x be Element of G_Quaternion;
let a be quaternion number ;
identify - x with  - a when x = a;
compatibility
 ( x = a implies - x = - a )
proof
assume A1: x = a ; ::_thesis: - x = - a
reconsider x1 = x as Element of QUATERNION by Def9;
reconsider b = - x1 as Element of G_Quaternion by Def9;
 b + x = 0. G_Quaternion by Th35, QUATERNI:def_8;
hence  - x = - a by A1, RLVECT_1:6; ::_thesis: verum
end;
end;

registration
let x, y be Element of G_Quaternion;
let a, b be quaternion number ;
identifyx - y with a - b when x = a, y = b;
compatibility
 ( x = a & y = b implies x - y = a - b ) ;
end;

theorem :: QUATERN2:36
for x, y, z being Element of G_Quaternion holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Quaternion) = x ) by RLVECT_1:def_3, RLVECT_1:def_4;

definition
func R_Quaternion  ->  strict doubleLoopStr  means :Def10: :: QUATERN2:def 10
( the carrier of it = QUATERNION & the addF of it = addquaternion & the multF of it = multquaternion & 1. it = 1q & 0. it = 0q );
existence
 ex b1 being strict doubleLoopStr st
( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q )
proof
take  doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) ; ::_thesis: ( the carrier of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = QUATERNION & the addF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = addquaternion & the multF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = multquaternion & 1. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 1q & 0. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 0q )
thus  ( the carrier of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = QUATERNION & the addF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = addquaternion & the multF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = multquaternion & 1. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 1q & 0. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 0q ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict doubleLoopStr st the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q & the carrier of b2 = QUATERNION & the addF of b2 = addquaternion & the multF of b2 = multquaternion & 1. b2 = 1q & 0. b2 = 0q holds
b1 = b2 ;
end;

:: deftheorem Def10 defines R_Quaternion QUATERN2:def_10_:_
 for b1 being strict doubleLoopStr holds
( b1 = R_Quaternion iff ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q ) );

registration
cluster R_Quaternion  ->  non empty strict ;
coherence
 not R_Quaternion is empty by Def10;
end;

registration
cluster  ->  quaternion for Element of the carrier of R_Quaternion;
coherence
 for b1 being Element of R_Quaternion holds b1 is quaternion
proof
let c be Element of R_Quaternion; ::_thesis: c is quaternion
 c in the carrier of R_Quaternion ;
then  c in QUATERNION by Def10;
hence  c is quaternion ; ::_thesis: verum
end;
end;

registration
let a, b be quaternion number ;
let x, y be Element of R_Quaternion;
identifyx + y with a + b when x = a, y = b;
compatibility
 ( x = a & y = b implies x + y = a + b )
proof
assume that
A1: x = a and
A2: y = b ; ::_thesis: x + y = a + b
reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def_2;
thus x + y = addquaternion . (a9,b9) by A1, A2, Def10
.= a + b by Def4 ; ::_thesis: verum
end;
identifyx * y with a * b when x = a, y = b;
compatibility
 ( x = a & y = b implies x * y = a * b )
proof
assume that
A3: x = a and
A4: y = b ; ::_thesis: x * y = a * b
reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def_2;
thus x * y = multquaternion . (a9,b9) by A3, A4, Def10
.= a * b by Def6 ; ::_thesis: verum
end;
end;

registration
cluster R_Quaternion  ->  strict well-unital ;
coherence
 R_Quaternion is well-unital
proof
let x be Element of R_Quaternion; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. R_Quaternion) = x & (1. R_Quaternion) * x = x )
 1. R_Quaternion = 1q by Def10;
hence  ( x * (1. R_Quaternion) = x & (1. R_Quaternion) * x = x ) by Th14, Th15; ::_thesis: verum
end;
end;

theorem :: QUATERN2:37
1. R_Quaternion = 1q by Def10;

theorem :: QUATERN2:38
1_ R_Quaternion = 1q by Def10;

theorem Th39: :: QUATERN2:39
0. R_Quaternion = 0q by Def10;

registration
cluster R_Quaternion  ->  non degenerated right_complementable almost_right_invertible strict Abelian add-associative right_zeroed associative right_unital distributive left_unital ;
coherence
 ( R_Quaternion is add-associative & R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
thus  R_Quaternion is add-associative ::_thesis: ( R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
let x, y, z be Element of R_Quaternion; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def10;
thus (x + y) + z = addquaternion . [( the addF of R_Quaternion . [x1,y1]),z1] by Def10
.= addquaternion . ((addquaternion . (x1,y1)),z1) by Def10
.= addquaternion . ((x1 + y1),z1) by Def4
.= (x1 + y1) + z1 by Def4
.= x1 + (y1 + z1) by Th2
.= addquaternion . (x1,(y1 + z1)) by Def4
.= addquaternion . [x1,(addquaternion . (y1,z1))] by Def4
.= addquaternion . [x1,( the addF of R_Quaternion . [y1,z1])] by Def10
.= x + (y + z) by Def10 ; ::_thesis: verum
end;
thus  R_Quaternion is right_zeroed ::_thesis: ( R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
let x be Element of R_Quaternion; :: according to RLVECT_1:def_4 ::_thesis: x + (0. R_Quaternion) = x
reconsider x1 = x as Element of QUATERNION by Def10;
thus x + (0. R_Quaternion) = the addF of R_Quaternion . (x1,0q) by Def10
.= addquaternion . (x1,0q) by Def10
.= x1 + 0q by Def4
.= x by Th3 ; ::_thesis: verum
end;
thus  R_Quaternion is right_complementable ::_thesis: ( R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
let x be Element of R_Quaternion; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of QUATERNION by Def10;
reconsider y = - x1 as Element of R_Quaternion by Def10;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. R_Quaternion
thus  x + y = 0. R_Quaternion by Th39, QUATERNI:def_8; ::_thesis: verum
end;
thus  R_Quaternion is Abelian ::_thesis: ( R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
let x, y be Element of R_Quaternion; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of QUATERNION by Def10;
thus  x + y = y + x ; ::_thesis: verum
end;
thus  R_Quaternion is associative ::_thesis: ( R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
let x, y, z be Element of R_Quaternion; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def10;
thus (x * y) * z = multquaternion . (( the multF of R_Quaternion . (x1,y1)),z1) by Def10
.= multquaternion . ((multquaternion . (x1,y1)),z1) by Def10
.= multquaternion . ((x1 * y1),z1) by Def6
.= (x1 * y1) * z1 by Def6
.= x1 * (y1 * z1) by Th16
.= multquaternion . (x1,(y1 * z1)) by Def6
.= multquaternion . (x1,(multquaternion . (y1,z1))) by Def6
.= multquaternion . (x1,( the multF of R_Quaternion . (y1,z1))) by Def10
.= x * (y * z) by Def10 ; ::_thesis: verum
end;
thus  ( R_Quaternion is left_unital & R_Quaternion is right_unital ) ; ::_thesis: ( R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
thus  R_Quaternion is distributive ::_thesis: ( R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof
let x, y, z be Element of R_Quaternion; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def10;
thus x * (y + z) = multquaternion . (x1,( the addF of R_Quaternion . (y1,z1))) by Def10
.= multquaternion . (x1,(addquaternion . (y1,z1))) by Def10
.= multquaternion . (x1,(y1 + z1)) by Def4
.= x1 * (y1 + z1) by Def6
.= (x1 * y1) + (x1 * z1) by Th17
.= addquaternion . ((x1 * y1),(x1 * z1)) by Def4
.= addquaternion . ((multquaternion . (x1,y1)),(x1 * z1)) by Def6
.= addquaternion . ((multquaternion . (x1,y1)),(multquaternion . (x1,z1))) by Def6
.= the addF of R_Quaternion . ((multquaternion . (x1,y1)),(multquaternion . (x1,z1))) by Def10
.= the addF of R_Quaternion . (( the multF of R_Quaternion . (x1,y1)),(multquaternion . (x1,z1))) by Def10
.= (x * y) + (x * z) by Def10 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = multquaternion . (( the addF of R_Quaternion . (y1,z1)),x1) by Def10
.= multquaternion . ((addquaternion . (y1,z1)),x1) by Def10
.= multquaternion . ((y1 + z1),x1) by Def4
.= (y1 + z1) * x1 by Def6
.= (y1 * x1) + (z1 * x1) by Th18
.= addquaternion . ((y1 * x1),(z1 * x1)) by Def4
.= addquaternion . ((multquaternion . (y1,x1)),(z1 * x1)) by Def6
.= addquaternion . ((multquaternion . (y1,x1)),(multquaternion . (z1,x1))) by Def6
.= the addF of R_Quaternion . ((multquaternion . (y1,x1)),(multquaternion . (z1,x1))) by Def10
.= the addF of R_Quaternion . (( the multF of R_Quaternion . (y1,x1)),(multquaternion . (z1,x1))) by Def10
.= (y * x) + (z * x) by Def10 ; ::_thesis: verum
end;
thus  R_Quaternion is almost_right_invertible ::_thesis: not R_Quaternion is degenerated
proof
let x be Element of R_Quaternion; :: according to ALGSTR_0:def_40 ::_thesis: ( x = 0. R_Quaternion or x is right_invertible )
assume A1: x <> 0. R_Quaternion ; ::_thesis: x is right_invertible
reconsider x1 = x as Element of QUATERNION by Def10;
reconsider y = x1 " as Element of R_Quaternion by Def10;
take  y ; :: according to ALGSTR_0:def_28 ::_thesis: x * y = 1. R_Quaternion
 x1 <> 0q by A1, Def10;
then x * y = 1 by Th31
.= 1. R_Quaternion by Def10 ;
hence  x * y = 1. R_Quaternion ; ::_thesis: verum
end;
 1. R_Quaternion = 1q by Def10;
then  0. R_Quaternion <> 1. R_Quaternion by Def10;
hence  not R_Quaternion is degenerated by STRUCT_0:def_8; ::_thesis: verum
end;
end;

registration
let x be Element of R_Quaternion;
let a be quaternion number ;
identify - x with  - a when x = a;
compatibility
 ( x = a implies - x = - a )
proof
assume A1: x = a ; ::_thesis: - x = - a
reconsider x1 = x as Element of QUATERNION by Def10;
reconsider b = - x1 as Element of R_Quaternion by Def10;
 b + x = 0. R_Quaternion by Th39, QUATERNI:def_8;
hence  - x = - a by A1, RLVECT_1:6; ::_thesis: verum
end;
end;

registration
let x, y be Element of R_Quaternion;
let a, b be quaternion number ;
identifyx - y with a - b when x = a, y = b;
compatibility
 ( x = a & y = b implies x - y = a - b ) ;
end;

definition
let z be Element of R_Quaternion;
:: original: *'
redefine funcz *'  ->  Element of R_Quaternion;
coherence
 z *' is Element of R_Quaternion by Def10;
end;

theorem :: QUATERN2:40
for z being Element of R_Quaternion holds - z = (- (1_ R_Quaternion)) * z
proof
let z be Element of R_Quaternion; ::_thesis: - z = (- (1_ R_Quaternion)) * z
reconsider z9 = z as Element of QUATERNION by Def10;
thus  - z = (- 1q) * z9 by Th19
.= (- (1_ R_Quaternion)) * z by Def10 ; ::_thesis: verum
end;

theorem :: QUATERN2:41
(0. R_Quaternion) *' = 0. R_Quaternion
proof
 0. R_Quaternion = 0q by Def10;
hence  (0. R_Quaternion) *' = 0. R_Quaternion by QUATERNI:45; ::_thesis: verum
end;

theorem :: QUATERN2:42
for z being Element of R_Quaternion st z *' = 0. R_Quaternion holds
z = 0. R_Quaternion
proof
let z be Element of R_Quaternion; ::_thesis: ( z *' = 0. R_Quaternion implies z = 0. R_Quaternion )
assume  z *' = 0. R_Quaternion ; ::_thesis: z = 0. R_Quaternion
then  z *' = 0q by Def10;
then  z = 0q by QUATERNI:46;
hence  z = 0. R_Quaternion by Def10; ::_thesis: verum
end;

theorem :: QUATERN2:43
(1. R_Quaternion) *' = 1. R_Quaternion
proof
 1. R_Quaternion = 1r by Def10;
hence  (1. R_Quaternion) *' = 1. R_Quaternion by QUATERNI:47; ::_thesis: verum
end;

theorem :: QUATERN2:44
|.(0. R_Quaternion).| = 0 by Def10, QUATERNI:65;

theorem :: QUATERN2:45
for z being Element of R_Quaternion st |.z.| = 0 holds
z = 0. R_Quaternion by Th39, QUATERNI:66;

theorem :: QUATERN2:46
|.(1. R_Quaternion).| = 1 by Def10, QUATERNI:68;

theorem :: QUATERN2:47
(1. R_Quaternion) " = 1. R_Quaternion
proof
1q " = 1q by Th33
.= 1. R_Quaternion by Def10 ;
hence  (1. R_Quaternion) " = 1. R_Quaternion by Def10; ::_thesis: verum
end;

definition
let x, y be quaternion number ;
funcx .|. y ->  Element of QUATERNION  equals :: QUATERN2:def 11
x * (y *');
coherence
 x * (y *') is Element of QUATERNION ;
end;

:: deftheorem  defines .|. QUATERN2:def_11_:_
 for x, y being quaternion number holds x .|. y = x * (y *');

theorem Th48: :: QUATERN2:48
for c1, c2 being quaternion number holds c1 .|. c2 = [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*]
proof
let c1, c2 be quaternion number ; ::_thesis: c1 .|. c2 = [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 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: Rea c1 = x1 by A1, QUATERNI:23;
A4: Im1 c1 = y1 by A1, QUATERNI:23;
A5: Im2 c1 = w1 by A1, QUATERNI:23;
A6: Im3 c1 = z1 by A1, QUATERNI:23;
A7: Rea c2 = x2 by A2, QUATERNI:23;
A8: Im1 c2 = y2 by A2, QUATERNI:23;
A9: Im2 c2 = w2 by A2, QUATERNI:23;
A10: Im3 c2 = z2 by A2, QUATERNI:23;
c1 .|. c2 = [*x1,y1,w1,z1*] * [*x2,(- y2),(- w2),(- z2)*] by A1, A2, Th25
.= [*((((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
.= [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*] by A3, A4, A5, A6, A7, A8, A9, A10 ;
hence  c1 .|. c2 = [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*] ; ::_thesis: verum
end;

theorem Th49: :: QUATERN2:49
for c being quaternion number holds c .|. c = |.c.| ^2
proof
let c be quaternion number ; ::_thesis: c .|. c = |.c.| ^2
A1: ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) >= 0 by Lm2;
c .|. c = [*(((((Rea c) * (Rea c)) + ((Im1 c) * (Im1 c))) + ((Im2 c) * (Im2 c))) + ((Im3 c) * (Im3 c))),(((((Rea c) * (- (Im1 c))) + ((Im1 c) * (Rea c))) - ((Im2 c) * (Im3 c))) + ((Im3 c) * (Im2 c))),(((((Rea c) * (- (Im2 c))) + ((Rea c) * (Im2 c))) - ((Im1 c) * (Im3 c))) + ((Im3 c) * (Im1 c))),(((((Rea c) * (- (Im3 c))) + ((Im3 c) * (Rea c))) - ((Im1 c) * (Im2 c))) + ((Im2 c) * (Im1 c)))*] by Th48
.= [*(((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2)),0*] by QUATERNI:91
.= ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) by ARYTM_0:def_5
.= |.c.| ^2 by A1, SQUARE_1:def_2 ;
hence  c .|. c = |.c.| ^2 ; ::_thesis: verum
end;

theorem :: QUATERN2:50
for c being quaternion number holds
( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 )
proof
let c be quaternion number ; ::_thesis: ( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 )
A1: ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) >= 0 by Lm2;
c .|. c = [*(((((Rea c) * (Rea c)) + ((Im1 c) * (Im1 c))) + ((Im2 c) * (Im2 c))) + ((Im3 c) * (Im3 c))),(((((Rea c) * (- (Im1 c))) + ((Im1 c) * (Rea c))) - ((Im2 c) * (Im3 c))) + ((Im3 c) * (Im2 c))),(((((Rea c) * (- (Im2 c))) + ((Rea c) * (Im2 c))) - ((Im1 c) * (Im3 c))) + ((Im3 c) * (Im1 c))),(((((Rea c) * (- (Im3 c))) + ((Im3 c) * (Rea c))) - ((Im1 c) * (Im2 c))) + ((Im2 c) * (Im1 c)))*] by Th48
.= [*(|.c.| ^2),0,0,0*] by A1, SQUARE_1:def_2 ;
hence  ( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 ) by QUATERNI:23; ::_thesis: verum
end;

theorem :: QUATERN2:51
for c1, c2 being quaternion number holds |.(c1 .|. c2).| = |.c1.| * |.c2.|
proof
let c1, c2 be quaternion number ; ::_thesis: |.(c1 .|. c2).| = |.c1.| * |.c2.|
thus |.(c1 .|. c2).| = |.c1.| * |.(c2 *').| by QUATERNI:87
.= |.c1.| * |.c2.| by QUATERNI:73 ; ::_thesis: verum
end;

theorem :: QUATERN2:52
for c being quaternion number st c .|. c = 0 holds
c = 0
proof
let c be quaternion number ; ::_thesis: ( c .|. c = 0 implies c = 0 )
assume  c .|. c = 0 ; ::_thesis: c = 0
then A1: |.c.| ^2 = 0 by Th49;
 ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) >= 0 by Lm2;
then A2: |.c.| ^2 = ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) by SQUARE_1:def_2;
then A3: Rea c = 0 by A1, Lm3;
A4: Im1 c = 0 by A1, A2, Lm3;
A5: Im2 c = 0 by A1, A2, Lm3;
 Im3 c = 0 by A1, A2, Lm3;
then c = [*0,0,0,0*] by A3, A4, A5, QUATERNI:24
.= [*0,0*] by QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  c = 0 ; ::_thesis: verum
end;

theorem :: QUATERN2:53
for c1, c2, c3 being quaternion number holds (c1 + c2) .|. c3 = (c1 .|. c3) + (c2 .|. c3) by Th18;

theorem :: QUATERN2:54
for c1, c2, c3 being quaternion number holds c1 .|. (c2 + c3) = (c1 .|. c2) + (c1 .|. c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: c1 .|. (c2 + c3) = (c1 .|. c2) + (c1 .|. c3)
thus c1 .|. (c2 + c3) = c1 * ((c2 *') + (c3 *')) by QUATERNI:54
.= (c1 .|. c2) + (c1 .|. c3) by Th17 ; ::_thesis: verum
end;

theorem :: QUATERN2:55
for c1, c2 being quaternion number holds (- c1) .|. c2 = - (c1 .|. c2) by Th20;

theorem :: QUATERN2:56
for c1, c2 being quaternion number holds - (c1 .|. c2) = c1 .|. (- c2)
proof
let c1, c2 be quaternion number ; ::_thesis: - (c1 .|. c2) = c1 .|. (- c2)
c1 .|. (- c2) = c1 * (- (c2 *')) by QUATERNI:55
.= - (c1 * (c2 *')) by Th21 ;
hence  - (c1 .|. c2) = c1 .|. (- c2) ; ::_thesis: verum
end;

theorem :: QUATERN2:57
for c1, c2 being quaternion number holds (- c1) .|. (- c2) = c1 .|. c2
proof
let c1, c2 be quaternion number ; ::_thesis: (- c1) .|. (- c2) = c1 .|. c2
(- c1) .|. (- c2) = (- c1) * (- (c2 *')) by QUATERNI:55
.= c1 * (c2 *') by Th22 ;
hence  (- c1) .|. (- c2) = c1 .|. c2 ; ::_thesis: verum
end;

theorem :: QUATERN2:58
for c1, c2, c3 being quaternion number holds (c1 - c2) .|. c3 = (c1 .|. c3) - (c2 .|. c3) by Th23;

theorem :: QUATERN2:59
for c1, c2, c3 being quaternion number holds c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3)
proof
let c1, c2, c3 be quaternion number ; ::_thesis: c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3)
c1 .|. (c2 - c3) = c1 * ((c2 *') - (c3 *')) by QUATERNI:56
.= (c1 * (c2 *')) - (c1 * (c3 *')) by Th24 ;
hence  c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3) ; ::_thesis: verum
end;

theorem :: QUATERN2:60
for c1, c2 being quaternion number holds (c1 + c2) .|. (c1 + c2) = (((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2)
proof
let c1, c2 be quaternion number ; ::_thesis: (c1 + c2) .|. (c1 + c2) = (((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2)
(c1 + c2) .|. (c1 + c2) = (c1 + c2) * ((c1 *') + (c2 *')) by QUATERNI:54
.= ((c1 + c2) * (c1 *')) + ((c1 + c2) * (c2 *')) by Th17
.= ((c1 * (c1 *')) + (c2 * (c1 *'))) + ((c1 + c2) * (c2 *')) by Th18
.= ((c1 .|. c1) + (c2 .|. c1)) + ((c1 .|. c2) + (c2 .|. c2)) by Th18
.= (((c1 .|. c1) + (c2 .|. c1)) + (c1 .|. c2)) + (c2 .|. c2) by Th2 ;
hence  (c1 + c2) .|. (c1 + c2) = (((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2) by Th2; ::_thesis: verum
end;

theorem :: QUATERN2:61
for c1, c2 being quaternion number holds (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2)
proof
let c1, c2 be quaternion number ; ::_thesis: (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2)
(c1 - c2) .|. (c1 - c2) = (c1 - c2) * ((c1 *') - (c2 *')) by QUATERNI:56
.= ((c1 + (- c2)) * (c1 *')) + ((c1 + (- c2)) * (- (c2 *'))) by Th17
.= ((c1 * (c1 *')) + ((- c2) * (c1 *'))) + ((c1 + (- c2)) * (- (c2 *'))) by Th18
.= ((c1 .|. c1) + ((- c2) * (c1 *'))) + ((c1 * (- (c2 *'))) + ((- c2) * (- (c2 *')))) by Th18
.= ((c1 .|. c1) + (- (c2 * (c1 *')))) + ((c1 * (- (c2 *'))) + ((- c2) * (- (c2 *')))) by Th20
.= ((c1 .|. c1) + (- (c2 * (c1 *')))) + ((- (c1 * (c2 *'))) + ((- c2) * (- (c2 *')))) by Th21
.= ((c1 .|. c1) + (- (c2 .|. c1))) + ((- (c1 .|. c2)) + (c2 .|. c2)) by Th22
.= (((c1 .|. c1) + (- (c2 .|. c1))) + (- (c1 .|. c2))) + (c2 .|. c2) by Th2
.= (((c1 .|. c1) + (- (c1 .|. c2))) + (- (c2 .|. c1))) + (c2 .|. c2) by Th2 ;
hence  (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2) ; ::_thesis: verum
end;