:: QUATERN3 semantic presentation

begin


theorem Th1: :: QUATERN3:1
for z1, z2 being quaternion number holds Rea (z1 * z2) = Rea (z2 * z1)
proof
let z1, z2 be quaternion number ; ::_thesis: Rea (z1 * z2) = Rea (z2 * z1)
 Rea (z2 * z1) = ((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1)) by QUATERNI:97;
hence  Rea (z1 * z2) = Rea (z2 * z1) by QUATERNI:97; ::_thesis: verum
end;

Lm1:  for z being quaternion number st z is Real holds
( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
proof
let z be quaternion number ; ::_thesis: ( z is Real implies ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) )
assume  z is Real ; ::_thesis: ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
then reconsider x = z as Real ;
 ( x = [*x,0*] & [*x,0*] = [*x,0,0,0*] ) by ARYTM_0:def_5, QUATERNI:91;
hence  ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by QUATERNI:23; ::_thesis: verum
end;

theorem :: QUATERN3:2
for z, z3 being quaternion number st z is Real holds
z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>)
proof
let z, z3 be quaternion number ; ::_thesis: ( z is Real implies z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>) )
reconsider z1 = z + z3 as quaternion number ;
assume A1: z is Real ; ::_thesis: z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>)
then A2: Im3 z = 0 by Lm1;
set z2 = [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*];
A3: Rea [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Rea z) + (Rea z3) by QUATERNI:23
.= Rea z1 by QUATERNI:36 ;
A4: Im1 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im1 z) + (Im1 z3) by QUATERNI:23
.= Im1 z1 by QUATERNI:36 ;
A5: Im3 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im3 z) + (Im3 z3) by QUATERNI:23
.= Im3 z1 by QUATERNI:36 ;
A6: Im2 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im2 z) + (Im2 z3) by QUATERNI:23
.= Im2 z1 by QUATERNI:36 ;
 ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1;
then  z + z3 = [*((Rea z) + (Rea z3)),(Im1 z3),(Im2 z3),(Im3 z3)*] by A2, A3, A4, A6, A5, QUATERNI:25;
hence  z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>) by QUATERN2:1; ::_thesis: verum
end;

theorem :: QUATERN3:3
for z, z3 being quaternion number st z is Real holds
z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]
proof
let z, z3 be quaternion number ; ::_thesis: ( z is Real implies z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] )
reconsider z1 = z + (- z3) as quaternion number ;
assume A1: z is Real ; ::_thesis: z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]
then A2: Im3 z = 0 by Lm1;
set z2 = [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*];
A3: Rea [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Rea z) + (- (Rea z3)) by QUATERNI:23
.= (Rea z) + (Rea (- z3)) by QUATERNI:41
.= Rea z1 by QUATERNI:36 ;
A4: Im1 [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Im1 z) + (- (Im1 z3)) by QUATERNI:23
.= (Im1 z) + (Im1 (- z3)) by QUATERNI:41
.= Im1 z1 by QUATERNI:36 ;
A5: Im3 [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Im3 z) + (- (Im3 z3)) by QUATERNI:23
.= (Im3 z) + (Im3 (- z3)) by QUATERNI:41
.= Im3 z1 by QUATERNI:36 ;
A6: Im2 [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Im2 z) + (- (Im2 z3)) by QUATERNI:23
.= (Im2 z) + (Im2 (- z3)) by QUATERNI:41
.= Im2 z1 by QUATERNI:36 ;
 ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1;
hence  z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] by A2, A3, A4, A6, A5, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:4
for z, z3 being quaternion number st z is Real holds
z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*]
proof
let z, z3 be quaternion number ; ::_thesis: ( z is Real implies z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] )
assume A1: z is Real ; ::_thesis: z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*]
then A2: Im3 z = 0 by Lm1;
A3: z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*]
proof
reconsider z9 = z * z3 as quaternion number ;
set z1 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*];
A4: Im1 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3)) by QUATERNI:23
.= Im1 z9 by QUATERNI:97 ;
A5: Im2 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3)) by QUATERNI:23
.= Im2 z9 by QUATERNI:97 ;
A6: Im3 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)) by QUATERNI:23
.= Im3 z9 by QUATERNI:97 ;
Rea [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3)) by QUATERNI:23
.= Rea z9 by QUATERNI:97 ;
hence  z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] by A4, A5, A6, QUATERNI:25; ::_thesis: verum
end;
 ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1;
hence  z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] by A2, A3; ::_thesis: verum
end;

theorem :: QUATERN3:5
for z being quaternion number st z is Real holds
z * <i> = [*0,(Rea z),0,0*]
proof
let z be quaternion number ; ::_thesis: ( z is Real implies z * <i> = [*0,(Rea z),0,0*] )
assume A1: z is Real ; ::_thesis: z * <i> = [*0,(Rea z),0,0*]
then reconsider x = z as Real ;
A2: x = Rea z by Lm1;
z * <i> = [*(Rea (z * <i>)),(Im1 (z * <i>)),(Im2 (z * <i>)),(Im3 (z * <i>))*] by QUATERNI:24
.= [*0,(Im1 (z * <i>)),(Im2 (z * <i>)),(Im3 (z * <i>))*] by A1, QUATERNI:33
.= [*0,x,(Im2 (z * <i>)),(Im3 (z * <i>))*] by QUATERNI:33
.= [*0,x,0,(Im3 (z * <i>))*] by QUATERNI:33
.= [*0,(Rea z),0,0*] by A2, QUATERNI:33 ;
hence  z * <i> = [*0,(Rea z),0,0*] ; ::_thesis: verum
end;

theorem :: QUATERN3:6
for z being quaternion number st z is Real holds
z * <j> = [*0,0,(Rea z),0*]
proof
let z be quaternion number ; ::_thesis: ( z is Real implies z * <j> = [*0,0,(Rea z),0*] )
assume A1: z is Real ; ::_thesis: z * <j> = [*0,0,(Rea z),0*]
then reconsider x = z as Real ;
A2: x = Rea z by Lm1;
z * <j> = [*(Rea (z * <j>)),(Im1 (z * <j>)),(Im2 (z * <j>)),(Im3 (z * <j>))*] by QUATERNI:24
.= [*0,(Im1 (z * <j>)),(Im2 (z * <j>)),(Im3 (z * <j>))*] by A1, QUATERNI:34
.= [*0,0,(Im2 (z * <j>)),(Im3 (z * <j>))*] by A1, QUATERNI:34
.= [*0,0,x,(Im3 (z * <j>))*] by QUATERNI:34
.= [*0,0,(Rea z),0*] by A2, QUATERNI:34 ;
hence  z * <j> = [*0,0,(Rea z),0*] ; ::_thesis: verum
end;

theorem :: QUATERN3:7
for z being quaternion number st z is Real holds
z * <k> = [*0,0,0,(Rea z)*]
proof
let z be quaternion number ; ::_thesis: ( z is Real implies z * <k> = [*0,0,0,(Rea z)*] )
assume A1: z is Real ; ::_thesis: z * <k> = [*0,0,0,(Rea z)*]
then reconsider x = z as Real ;
A2: x = Rea z by Lm1;
z * <k> = [*(Rea (z * <k>)),(Im1 (z * <k>)),(Im2 (z * <k>)),(Im3 (z * <k>))*] by QUATERNI:24
.= [*0,(Im1 (z * <k>)),(Im2 (z * <k>)),(Im3 (z * <k>))*] by A1, QUATERNI:35
.= [*0,0,(Im2 (z * <k>)),(Im3 (z * <k>))*] by A1, QUATERNI:35
.= [*0,0,0,(Im3 (z * <k>))*] by A1, QUATERNI:35
.= [*0,0,0,(Rea z)*] by A2, QUATERNI:35 ;
hence  z * <k> = [*0,0,0,(Rea z)*] ; ::_thesis: verum
end;

theorem :: QUATERN3:8
for z being quaternion number holds z - 0q = z
proof
let z be quaternion number ; ::_thesis: z - 0q = z
consider x, y, w, v being Element of REAL  such that
A1: z = [*x,y,w,v*] by QUATERNI:7;
0q = [*0,0*] by ARYTM_0:def_5
.= [*0,0,0,0*] by QUATERNI:91 ;
then  - 0q = [*(- 0),(- 0),(- 0),(- 0)*] by QUATERN2:4;
then z - 0q = [*(x + (- 0)),(y + (- 0)),(w + (- 0)),(v + (- 0))*] by A1, QUATERNI:def_7
.= [*x,y,w,v*] ;
hence  z - 0q = z by A1; ::_thesis: verum
end;

theorem :: QUATERN3:9
for z, z1 being quaternion number st z is Real holds
z * z1 = z1 * z
proof
let z, z1 be quaternion number ; ::_thesis: ( z is Real implies z * z1 = z1 * z )
assume A1: z is Real ; ::_thesis: z * z1 = z1 * z
then A2: Im3 z = 0 by Lm1;
A3: ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1;
 z1 * z = (((((((Rea z1) * (Rea z)) - ((Im1 z1) * (Im1 z))) - ((Im2 z1) * (Im2 z))) - ((Im3 z1) * (Im3 z))) + ((((((Rea z1) * (Im1 z)) + ((Im1 z1) * (Rea z))) + ((Im2 z1) * (Im3 z))) - ((Im3 z1) * (Im2 z))) * <i>)) + ((((((Rea z1) * (Im2 z)) + ((Im2 z1) * (Rea z))) + ((Im3 z1) * (Im1 z))) - ((Im1 z1) * (Im3 z))) * <j>)) + ((((((Rea z1) * (Im3 z)) + ((Im3 z1) * (Rea z))) + ((Im1 z1) * (Im2 z))) - ((Im2 z1) * (Im1 z))) * <k>) by QUATERNI:93;
hence  z * z1 = z1 * z by A2, A3, QUATERNI:93; ::_thesis: verum
end;

theorem :: QUATERN3:10
for z being quaternion number st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds
z = Rea z
proof
let z be quaternion number ; ::_thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = Rea z )
set x = Rea z;
assume  ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ; ::_thesis: z = Rea z
then A1: z = [*(Rea z),0,0,0*] by QUATERNI:24;
 [*(Rea z),0,0,0*] = [*(Rea z),0*] by QUATERNI:91;
hence  z = Rea z by A1, ARYTM_0:def_5; ::_thesis: verum
end;

theorem Th11: :: QUATERN3:11
for z being quaternion number holds |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)
proof
let z be quaternion number ; ::_thesis: |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)
 ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) >= 0 by QUATERNI:74;
then |.z.| ^2 = sqrt ((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) ^2) by SQUARE_1:29
.= ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by QUATERNI:74, SQUARE_1:22 ;
hence  |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) ; ::_thesis: verum
end;

theorem :: QUATERN3:12
for z being quaternion number holds |.z.| ^2 = |.(z * (z *')).|
proof
let z be quaternion number ; ::_thesis: |.z.| ^2 = |.(z * (z *')).|
 ( |.(z * z).| = |.(z * (z *')).| & |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) ) by Th11, QUATERNI:89;
hence  |.z.| ^2 = |.(z * (z *')).| by QUATERNI:88; ::_thesis: verum
end;

theorem :: QUATERN3:13
for z being quaternion number holds |.z.| ^2 = Rea (z * (z *'))
proof
let z be quaternion number ; ::_thesis: |.z.| ^2 = Rea (z * (z *'))
 Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by QUATERNI:60;
hence  |.z.| ^2 = Rea (z * (z *')) by Th11; ::_thesis: verum
end;

theorem :: QUATERN3:14
for z being quaternion number holds 2 * (Rea z) = Rea (z + (z *'))
proof
let z be quaternion number ; ::_thesis: 2 * (Rea z) = Rea (z + (z *'))
 ( z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] & z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] ) by QUATERNI:24, QUATERNI:43;
then z + (z *') = [*((Rea z) + (Rea z)),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] by QUATERNI:def_7
.= [*(2 * (Rea z)),0,0,0*] ;
hence  2 * (Rea z) = Rea (z + (z *')) by QUATERNI:23; ::_thesis: verum
end;

theorem :: QUATERN3:15
for z, z1 being quaternion number st z is Real holds
(z * z1) *' = (z *') * (z1 *')
proof
let z, z1 be quaternion number ; ::_thesis: ( z is Real implies (z * z1) *' = (z *') * (z1 *') )
A1: ( Im1 (z1 *') = - (Im1 z1) & Im2 (z1 *') = - (Im2 z1) ) by QUATERNI:44;
A2: ( Im3 (z1 *') = - (Im3 z1) & Rea (z *') = Rea z ) by QUATERNI:44;
A3: Rea (z * z1) = ((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1)) by QUATERNI:97;
assume A4: z is Real ; ::_thesis: (z * z1) *' = (z *') * (z1 *')
then reconsider x = z as Real ;
A5: ( Im1 z = 0 & Im2 z = 0 ) by A4, Lm1;
A6: Im3 z = 0 by A4, Lm1;
A7: Im3 (z *') = - (Im3 z) by QUATERNI:44;
A8: ( Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) ) by QUATERNI:44;
A9: Im3 (z * z1) = ((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)) by QUATERNI:97;
A10: Im2 (z * z1) = ((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)) by QUATERNI:97;
A11: Im1 (z * z1) = ((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)) by QUATERNI:97;
set z3 = z *' ;
set z2 = z1 *' ;
A12: (z *') * (z1 *') = (((((((Rea (z *')) * (Rea (z1 *'))) - ((Im1 (z *')) * (Im1 (z1 *')))) - ((Im2 (z *')) * (Im2 (z1 *')))) - ((Im3 (z *')) * (Im3 (z1 *')))) + ((((((Rea (z *')) * (Im1 (z1 *'))) + ((Im1 (z *')) * (Rea (z1 *')))) + ((Im2 (z *')) * (Im3 (z1 *')))) - ((Im3 (z *')) * (Im2 (z1 *')))) * <i>)) + ((((((Rea (z *')) * (Im2 (z1 *'))) + ((Im2 (z *')) * (Rea (z1 *')))) + ((Im3 (z *')) * (Im1 (z1 *')))) - ((Im1 (z *')) * (Im3 (z1 *')))) * <j>)) + ((((((Rea (z *')) * (Im3 (z1 *'))) + ((Im3 (z *')) * (Rea (z1 *')))) + ((Im1 (z *')) * (Im2 (z1 *')))) - ((Im2 (z *')) * (Im1 (z1 *')))) * <k>) by QUATERNI:93;
(z * z1) *' = (((Rea ((z * z1) *')) + ((Im1 ((z * z1) *')) * <i>)) + ((Im2 ((z * z1) *')) * <j>)) + ((Im3 ((z * z1) *')) * <k>) by QUATERNI:37
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((Im1 ((z * z1) *')) * <i>)) + ((Im2 ((z * z1) *')) * <j>)) + ((Im3 ((z * z1) *')) * <k>) by A3, QUATERNI:44
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * <i>)) + ((Im2 ((z * z1) *')) * <j>)) + ((Im3 ((z * z1) *')) * <k>) by A11, QUATERNI:44
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * <i>)) + ((- (((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)))) * <j>)) + ((Im3 ((z * z1) *')) * <k>) by A10, QUATERNI:44
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * <i>)) + ((- (((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)))) * <j>)) + ((- (((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)))) * <k>) by A9, QUATERNI:44 ;
hence  (z * z1) *' = (z *') * (z1 *') by A5, A6, A1, A2, A8, A7, A12, QUATERNI:44; ::_thesis: verum
end;

theorem :: QUATERN3:16
for z1, z2 being quaternion number holds (z1 * z2) *' = (z2 *') * (z1 *')
proof
let z1, z2 be quaternion number ; ::_thesis: (z1 * z2) *' = (z2 *') * (z1 *')
A1: ( Rea (z2 *') = Rea z2 & Im1 (z2 *') = - (Im1 z2) ) by QUATERNI:44;
A2: ( Im2 (z2 *') = - (Im2 z2) & Im3 (z2 *') = - (Im3 z2) ) by QUATERNI:44;
A3: Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) by QUATERNI:97;
A4: Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) by QUATERNI:97;
A5: ( Im2 (z1 *') = - (Im2 z1) & Im3 (z1 *') = - (Im3 z1) ) by QUATERNI:44;
A6: ( Rea (z1 *') = Rea z1 & Im1 (z1 *') = - (Im1 z1) ) by QUATERNI:44;
A7: Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) by QUATERNI:97;
A8: Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by QUATERNI:97;
set z3 = z2 *' ;
set z4 = z1 *' ;
A9: (z2 *') * (z1 *') = (((((((Rea (z2 *')) * (Rea (z1 *'))) - ((Im1 (z2 *')) * (Im1 (z1 *')))) - ((Im2 (z2 *')) * (Im2 (z1 *')))) - ((Im3 (z2 *')) * (Im3 (z1 *')))) + ((((((Rea (z2 *')) * (Im1 (z1 *'))) + ((Im1 (z2 *')) * (Rea (z1 *')))) + ((Im2 (z2 *')) * (Im3 (z1 *')))) - ((Im3 (z2 *')) * (Im2 (z1 *')))) * <i>)) + ((((((Rea (z2 *')) * (Im2 (z1 *'))) + ((Im2 (z2 *')) * (Rea (z1 *')))) + ((Im3 (z2 *')) * (Im1 (z1 *')))) - ((Im1 (z2 *')) * (Im3 (z1 *')))) * <j>)) + ((((((Rea (z2 *')) * (Im3 (z1 *'))) + ((Im3 (z2 *')) * (Rea (z1 *')))) + ((Im1 (z2 *')) * (Im2 (z1 *')))) - ((Im2 (z2 *')) * (Im1 (z1 *')))) * <k>) by QUATERNI:93;
(z1 * z2) *' = (((Rea ((z1 * z2) *')) + ((Im1 ((z1 * z2) *')) * <i>)) + ((Im2 ((z1 * z2) *')) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>) by QUATERNI:37
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((Im1 ((z1 * z2) *')) * <i>)) + ((Im2 ((z1 * z2) *')) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>) by A3, QUATERNI:44
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i>)) + ((Im2 ((z1 * z2) *')) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>) by A8, QUATERNI:44
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i>)) + ((- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>) by A7, QUATERNI:44
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i>)) + ((- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))) * <j>)) + ((- (((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))) * <k>) by A4, QUATERNI:44 ;
hence  (z1 * z2) *' = (z2 *') * (z1 *') by A1, A2, A6, A5, A9; ::_thesis: verum
end;

theorem Th17: :: QUATERN3:17
for z1, z2 being quaternion number holds |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2)
proof
let z1, z2 be quaternion number ; ::_thesis: |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2)
set z3 = z1 * z2;
A1: ( Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) ) by QUATERNI:97;
A2: ( Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) ) by QUATERNI:97;
 ( |.z1.| ^2 = ((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2) & |.z2.| ^2 = ((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2) ) by Th11;
hence  |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2) by A1, A2, Th11; ::_thesis: verum
end;

theorem :: QUATERN3:18
for z1 being quaternion number holds (<i> * z1) - (z1 * <i>) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*]
proof
let z1 be quaternion number ; ::_thesis: (<i> * z1) - (z1 * <i>) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*]
set z = <i> ;
set s = (<i> * z1) - (z1 * <i>);
A1: ( Rea (z1 * <i>) = ((((Rea z1) * (Rea <i>)) - ((Im1 z1) * (Im1 <i>))) - ((Im2 z1) * (Im2 <i>))) - ((Im3 z1) * (Im3 <i>)) & Im1 (z1 * <i>) = ((((Rea z1) * (Im1 <i>)) + ((Im1 z1) * (Rea <i>))) + ((Im2 z1) * (Im3 <i>))) - ((Im3 z1) * (Im2 <i>)) & Im2 (z1 * <i>) = ((((Rea z1) * (Im2 <i>)) + ((Im2 z1) * (Rea <i>))) + ((Im3 z1) * (Im1 <i>))) - ((Im1 z1) * (Im3 <i>)) & Im3 (z1 * <i>) = ((((Rea z1) * (Im3 <i>)) + ((Im3 z1) * (Rea <i>))) + ((Im1 z1) * (Im2 <i>))) - ((Im2 z1) * (Im1 <i>)) ) by QUATERNI:97;
A2: ( Im2 (<i> * z1) = ((((Rea <i>) * (Im2 z1)) + ((Im2 <i>) * (Rea z1))) + ((Im3 <i>) * (Im1 z1))) - ((Im1 <i>) * (Im3 z1)) & Im3 (<i> * z1) = ((((Rea <i>) * (Im3 z1)) + ((Im3 <i>) * (Rea z1))) + ((Im1 <i>) * (Im2 z1))) - ((Im2 <i>) * (Im1 z1)) ) by QUATERNI:97;
 ( Rea (<i> * z1) = - (Im1 z1) & Im1 (<i> * z1) = Rea z1 ) by A1, QUATERNI:30, QUATERNI:97;
then A3: ( Rea ((<i> * z1) - (z1 * <i>)) = (- (Im1 z1)) - (- (Im1 z1)) & Im1 ((<i> * z1) - (z1 * <i>)) = (Rea z1) - (Rea z1) ) by A1, QUATERNI:30, QUATERNI:42;
 ( Im2 ((<i> * z1) - (z1 * <i>)) = (- (Im3 z1)) - (Im3 z1) & Im3 ((<i> * z1) - (z1 * <i>)) = (Im2 z1) - (- (Im2 z1)) ) by A2, A1, QUATERNI:30, QUATERNI:42;
hence  (<i> * z1) - (z1 * <i>) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*] by A3, QUATERNI:24; ::_thesis: verum
end;

theorem :: QUATERN3:19
for z1 being quaternion number holds (<i> * z1) + (z1 * <i>) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*]
proof
let z1 be quaternion number ; ::_thesis: (<i> * z1) + (z1 * <i>) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*]
set z = <i> ;
A1: <i> * z1 = (((((((Rea <i>) * (Rea z1)) - ((Im1 <i>) * (Im1 z1))) - ((Im2 <i>) * (Im2 z1))) - ((Im3 <i>) * (Im3 z1))) + ((((((Rea <i>) * (Im1 z1)) + ((Im1 <i>) * (Rea z1))) + ((Im2 <i>) * (Im3 z1))) - ((Im3 <i>) * (Im2 z1))) * <i>)) + ((((((Rea <i>) * (Im2 z1)) + ((Im2 <i>) * (Rea z1))) + ((Im3 <i>) * (Im1 z1))) - ((Im1 <i>) * (Im3 z1))) * <j>)) + ((((((Rea <i>) * (Im3 z1)) + ((Im3 <i>) * (Rea z1))) + ((Im1 <i>) * (Im2 z1))) - ((Im2 <i>) * (Im1 z1))) * <k>) by QUATERNI:93
.= [*(- (Im1 z1)),(Rea z1),(- (Im3 z1)),(Im2 z1)*] by QUATERN2:1, QUATERNI:30 ;
then A2: ( Im2 (<i> * z1) = - (Im3 z1) & Im3 (<i> * z1) = Im2 z1 ) by QUATERNI:23;
A3: z1 * <i> = (((((((Rea z1) * (Rea <i>)) - ((Im1 z1) * (Im1 <i>))) - ((Im2 z1) * (Im2 <i>))) - ((Im3 z1) * (Im3 <i>))) + ((((((Rea z1) * (Im1 <i>)) + ((Im1 z1) * (Rea <i>))) + ((Im2 z1) * (Im3 <i>))) - ((Im3 z1) * (Im2 <i>))) * <i>)) + ((((((Rea z1) * (Im2 <i>)) + ((Im2 z1) * (Rea <i>))) + ((Im3 z1) * (Im1 <i>))) - ((Im1 z1) * (Im3 <i>))) * <j>)) + ((((((Rea z1) * (Im3 <i>)) + ((Im3 z1) * (Rea <i>))) + ((Im1 z1) * (Im2 <i>))) - ((Im2 z1) * (Im1 <i>))) * <k>) by QUATERNI:93
.= [*(- (Im1 z1)),(Rea z1),(Im3 z1),(- (Im2 z1))*] by QUATERN2:1, QUATERNI:30 ;
then A4: ( Rea (z1 * <i>) = - (Im1 z1) & Im1 (z1 * <i>) = Rea z1 ) by QUATERNI:23;
A5: ( Im2 (z1 * <i>) = Im3 z1 & Im3 (z1 * <i>) = - (Im2 z1) ) by A3, QUATERNI:23;
 ( Rea (<i> * z1) = - (Im1 z1) & Im1 (<i> * z1) = Rea z1 ) by A1, QUATERNI:23;
then  (<i> * z1) + (z1 * <i>) = ((((- (Im1 z1)) + (- (Im1 z1))) + (((Rea z1) + (Rea z1)) * <i>)) + (((- (Im3 z1)) + (Im3 z1)) * <j>)) + (((Im2 z1) + (- (Im2 z1))) * <k>) by A2, A4, A5, QUATERNI:92;
hence  (<i> * z1) + (z1 * <i>) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*] by QUATERN2:1; ::_thesis: verum
end;

theorem :: QUATERN3:20
for z1 being quaternion number holds (<j> * z1) - (z1 * <j>) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*]
proof
let z1 be quaternion number ; ::_thesis: (<j> * z1) - (z1 * <j>) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*]
set z = <j> ;
A1: <j> * z1 = (((((((Rea <j>) * (Rea z1)) - ((Im1 <j>) * (Im1 z1))) - ((Im2 <j>) * (Im2 z1))) - ((Im3 <j>) * (Im3 z1))) + ((((((Rea <j>) * (Im1 z1)) + ((Im1 <j>) * (Rea z1))) + ((Im2 <j>) * (Im3 z1))) - ((Im3 <j>) * (Im2 z1))) * <i>)) + ((((((Rea <j>) * (Im2 z1)) + ((Im2 <j>) * (Rea z1))) + ((Im3 <j>) * (Im1 z1))) - ((Im1 <j>) * (Im3 z1))) * <j>)) + ((((((Rea <j>) * (Im3 z1)) + ((Im3 <j>) * (Rea z1))) + ((Im1 <j>) * (Im2 z1))) - ((Im2 <j>) * (Im1 z1))) * <k>) by QUATERNI:93
.= [*(- (Im2 z1)),(Im3 z1),(Rea z1),(- (Im1 z1))*] by QUATERN2:1, QUATERNI:31 ;
z1 * <j> = (((((((Rea z1) * (Rea <j>)) - ((Im1 z1) * (Im1 <j>))) - ((Im2 z1) * (Im2 <j>))) - ((Im3 z1) * (Im3 <j>))) + ((((((Rea z1) * (Im1 <j>)) + ((Im1 z1) * (Rea <j>))) + ((Im2 z1) * (Im3 <j>))) - ((Im3 z1) * (Im2 <j>))) * <i>)) + ((((((Rea z1) * (Im2 <j>)) + ((Im2 z1) * (Rea <j>))) + ((Im3 z1) * (Im1 <j>))) - ((Im1 z1) * (Im3 <j>))) * <j>)) + ((((((Rea z1) * (Im3 <j>)) + ((Im3 z1) * (Rea <j>))) + ((Im1 z1) * (Im2 <j>))) - ((Im2 z1) * (Im1 <j>))) * <k>) by QUATERNI:93
.= [*(- (Im2 z1)),(- (Im3 z1)),(Rea z1),(Im1 z1)*] by QUATERN2:1, QUATERNI:31 ;
then (<j> * z1) - (z1 * <j>) = [*((- (Im2 z1)) - (- (Im2 z1))),((Im3 z1) - (- (Im3 z1))),((Rea z1) - (Rea z1)),((- (Im1 z1)) - (Im1 z1))*] by A1, QUATERN2:5
.= [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] ;
hence  (<j> * z1) - (z1 * <j>) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] ; ::_thesis: verum
end;

theorem :: QUATERN3:21
for z1 being quaternion number holds (<j> * z1) + (z1 * <j>) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*]
proof
let z1 be quaternion number ; ::_thesis: (<j> * z1) + (z1 * <j>) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*]
set z = <j> ;
A1: <j> * z1 = (((((((Rea <j>) * (Rea z1)) - ((Im1 <j>) * (Im1 z1))) - ((Im2 <j>) * (Im2 z1))) - ((Im3 <j>) * (Im3 z1))) + ((((((Rea <j>) * (Im1 z1)) + ((Im1 <j>) * (Rea z1))) + ((Im2 <j>) * (Im3 z1))) - ((Im3 <j>) * (Im2 z1))) * <i>)) + ((((((Rea <j>) * (Im2 z1)) + ((Im2 <j>) * (Rea z1))) + ((Im3 <j>) * (Im1 z1))) - ((Im1 <j>) * (Im3 z1))) * <j>)) + ((((((Rea <j>) * (Im3 z1)) + ((Im3 <j>) * (Rea z1))) + ((Im1 <j>) * (Im2 z1))) - ((Im2 <j>) * (Im1 z1))) * <k>) by QUATERNI:93
.= [*(- (Im2 z1)),(Im3 z1),(Rea z1),(- (Im1 z1))*] by QUATERN2:1, QUATERNI:31 ;
then A2: ( Im2 (<j> * z1) = Rea z1 & Im3 (<j> * z1) = - (Im1 z1) ) by QUATERNI:23;
A3: z1 * <j> = (((((((Rea z1) * (Rea <j>)) - ((Im1 z1) * (Im1 <j>))) - ((Im2 z1) * (Im2 <j>))) - ((Im3 z1) * (Im3 <j>))) + ((((((Rea z1) * (Im1 <j>)) + ((Im1 z1) * (Rea <j>))) + ((Im2 z1) * (Im3 <j>))) - ((Im3 z1) * (Im2 <j>))) * <i>)) + ((((((Rea z1) * (Im2 <j>)) + ((Im2 z1) * (Rea <j>))) + ((Im3 z1) * (Im1 <j>))) - ((Im1 z1) * (Im3 <j>))) * <j>)) + ((((((Rea z1) * (Im3 <j>)) + ((Im3 z1) * (Rea <j>))) + ((Im1 z1) * (Im2 <j>))) - ((Im2 z1) * (Im1 <j>))) * <k>) by QUATERNI:93
.= [*(- (Im2 z1)),(- (Im3 z1)),(Rea z1),(Im1 z1)*] by QUATERN2:1, QUATERNI:31 ;
then A4: ( Rea (z1 * <j>) = - (Im2 z1) & Im1 (z1 * <j>) = - (Im3 z1) ) by QUATERNI:23;
A5: ( Im2 (z1 * <j>) = Rea z1 & Im3 (z1 * <j>) = Im1 z1 ) by A3, QUATERNI:23;
 ( Rea (<j> * z1) = - (Im2 z1) & Im1 (<j> * z1) = Im3 z1 ) by A1, QUATERNI:23;
then  (z1 * <j>) + (<j> * z1) = ((((- (Im2 z1)) + (- (Im2 z1))) + (((Im3 z1) - (Im3 z1)) * <i>)) + (((Rea z1) + (Rea z1)) * <j>)) + (((- (Im1 z1)) + (Im1 z1)) * <k>) by A2, A4, A5, QUATERNI:92;
hence  (<j> * z1) + (z1 * <j>) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*] by QUATERN2:1; ::_thesis: verum
end;

theorem :: QUATERN3:22
for z1 being quaternion number holds (<k> * z1) - (z1 * <k>) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*]
proof
let z1 be quaternion number ; ::_thesis: (<k> * z1) - (z1 * <k>) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*]
set z = <k> ;
A1: <k> * z1 = (((((((Rea <k>) * (Rea z1)) - ((Im1 <k>) * (Im1 z1))) - ((Im2 <k>) * (Im2 z1))) - ((Im3 <k>) * (Im3 z1))) + ((((((Rea <k>) * (Im1 z1)) + ((Im1 <k>) * (Rea z1))) + ((Im2 <k>) * (Im3 z1))) - ((Im3 <k>) * (Im2 z1))) * <i>)) + ((((((Rea <k>) * (Im2 z1)) + ((Im2 <k>) * (Rea z1))) + ((Im3 <k>) * (Im1 z1))) - ((Im1 <k>) * (Im3 z1))) * <j>)) + ((((((Rea <k>) * (Im3 z1)) + ((Im3 <k>) * (Rea z1))) + ((Im1 <k>) * (Im2 z1))) - ((Im2 <k>) * (Im1 z1))) * <k>) by QUATERNI:93
.= [*(- (Im3 z1)),(- (Im2 z1)),(Im1 z1),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ;
z1 * <k> = (((((((Rea z1) * (Rea <k>)) - ((Im1 z1) * (Im1 <k>))) - ((Im2 z1) * (Im2 <k>))) - ((Im3 z1) * (Im3 <k>))) + ((((((Rea z1) * (Im1 <k>)) + ((Im1 z1) * (Rea <k>))) + ((Im2 z1) * (Im3 <k>))) - ((Im3 z1) * (Im2 <k>))) * <i>)) + ((((((Rea z1) * (Im2 <k>)) + ((Im2 z1) * (Rea <k>))) + ((Im3 z1) * (Im1 <k>))) - ((Im1 z1) * (Im3 <k>))) * <j>)) + ((((((Rea z1) * (Im3 <k>)) + ((Im3 z1) * (Rea <k>))) + ((Im1 z1) * (Im2 <k>))) - ((Im2 z1) * (Im1 <k>))) * <k>) by QUATERNI:93
.= [*(- (Im3 z1)),(Im2 z1),(- (Im1 z1)),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ;
then (<k> * z1) - (z1 * <k>) = [*((- (Im3 z1)) - (- (Im3 z1))),((- (Im2 z1)) - (Im2 z1)),((Im1 z1) - (- (Im1 z1))),((Rea z1) - (Rea z1))*] by A1, QUATERN2:5
.= [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] ;
hence  (<k> * z1) - (z1 * <k>) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] ; ::_thesis: verum
end;

theorem :: QUATERN3:23
for z1 being quaternion number holds (<k> * z1) + (z1 * <k>) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*]
proof
let z1 be quaternion number ; ::_thesis: (<k> * z1) + (z1 * <k>) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*]
set z = <k> ;
A1: <k> * z1 = (((((((Rea <k>) * (Rea z1)) - ((Im1 <k>) * (Im1 z1))) - ((Im2 <k>) * (Im2 z1))) - ((Im3 <k>) * (Im3 z1))) + ((((((Rea <k>) * (Im1 z1)) + ((Im1 <k>) * (Rea z1))) + ((Im2 <k>) * (Im3 z1))) - ((Im3 <k>) * (Im2 z1))) * <i>)) + ((((((Rea <k>) * (Im2 z1)) + ((Im2 <k>) * (Rea z1))) + ((Im3 <k>) * (Im1 z1))) - ((Im1 <k>) * (Im3 z1))) * <j>)) + ((((((Rea <k>) * (Im3 z1)) + ((Im3 <k>) * (Rea z1))) + ((Im1 <k>) * (Im2 z1))) - ((Im2 <k>) * (Im1 z1))) * <k>) by QUATERNI:93
.= [*(- (Im3 z1)),(- (Im2 z1)),(Im1 z1),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ;
then A2: ( Im2 (<k> * z1) = Im1 z1 & Im3 (<k> * z1) = Rea z1 ) by QUATERNI:23;
A3: z1 * <k> = (((((((Rea z1) * (Rea <k>)) - ((Im1 z1) * (Im1 <k>))) - ((Im2 z1) * (Im2 <k>))) - ((Im3 z1) * (Im3 <k>))) + ((((((Rea z1) * (Im1 <k>)) + ((Im1 z1) * (Rea <k>))) + ((Im2 z1) * (Im3 <k>))) - ((Im3 z1) * (Im2 <k>))) * <i>)) + ((((((Rea z1) * (Im2 <k>)) + ((Im2 z1) * (Rea <k>))) + ((Im3 z1) * (Im1 <k>))) - ((Im1 z1) * (Im3 <k>))) * <j>)) + ((((((Rea z1) * (Im3 <k>)) + ((Im3 z1) * (Rea <k>))) + ((Im1 z1) * (Im2 <k>))) - ((Im2 z1) * (Im1 <k>))) * <k>) by QUATERNI:93
.= [*(- (Im3 z1)),(Im2 z1),(- (Im1 z1)),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ;
then A4: ( Rea (z1 * <k>) = - (Im3 z1) & Im1 (z1 * <k>) = Im2 z1 ) by QUATERNI:23;
A5: ( Im2 (z1 * <k>) = - (Im1 z1) & Im3 (z1 * <k>) = Rea z1 ) by A3, QUATERNI:23;
 ( Rea (<k> * z1) = - (Im3 z1) & Im1 (<k> * z1) = - (Im2 z1) ) by A1, QUATERNI:23;
then  (z1 * <k>) + (<k> * z1) = ((((- (Im3 z1)) + (- (Im3 z1))) + (((- (Im2 z1)) + (Im2 z1)) * <i>)) + (((Im1 z1) - (Im1 z1)) * <j>)) + (((Rea z1) + (Rea z1)) * <k>) by A2, A4, A5, QUATERNI:92;
hence  (<k> * z1) + (z1 * <k>) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*] by QUATERN2:1; ::_thesis: verum
end;

theorem Th24: :: QUATERN3:24
for z being quaternion number holds Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z)
proof
let z be quaternion number ; ::_thesis: Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z)
 z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21;
hence  Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z) by QUATERNI:23; ::_thesis: verum
end;

theorem Th25: :: QUATERN3:25
for z being quaternion number holds Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z))
proof
let z be quaternion number ; ::_thesis: Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z))
 z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21;
hence  Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z)) by QUATERNI:23; ::_thesis: verum
end;

theorem Th26: :: QUATERN3:26
for z being quaternion number holds Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z))
proof
let z be quaternion number ; ::_thesis: Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z))
 z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21;
hence  Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z)) by QUATERNI:23; ::_thesis: verum
end;

theorem Th27: :: QUATERN3:27
for z being quaternion number holds Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z))
proof
let z be quaternion number ; ::_thesis: Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z))
 z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21;
hence  Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z)) by QUATERNI:23; ::_thesis: verum
end;

theorem :: QUATERN3:28
for z being quaternion number holds (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*]
proof
let z be quaternion number ; ::_thesis: (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*]
set zz = |.z.| ^2 ;
 (1 / (|.z.| ^2)) * (z *') = [*(Rea ((1 / (|.z.| ^2)) * (z *'))),(Im1 ((1 / (|.z.| ^2)) * (z *'))),(Im2 ((1 / (|.z.| ^2)) * (z *'))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by QUATERNI:24;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(Im1 ((1 / (|.z.| ^2)) * (z *'))),(Im2 ((1 / (|.z.| ^2)) * (z *'))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by Th24;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(Im2 ((1 / (|.z.| ^2)) * (z *'))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by Th25;
then  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by Th26;
hence  (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*] by Th27; ::_thesis: verum
end;

theorem :: QUATERN3:29
for z being quaternion number holds z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*]
proof
let z be quaternion number ; ::_thesis: z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*]
set zz = |.z.| ^2 ;
set z3 = (1 / (|.z.| ^2)) * (z *');
z * ((1 / (|.z.| ^2)) * (z *')) = (((((((Rea z) * (Rea ((1 / (|.z.| ^2)) * (z *')))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) + ((((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) * <i>)) + ((((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) * <j>)) + ((((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) * <k>) by QUATERNI:93
.= [*(((((Rea z) * (Rea ((1 / (|.z.| ^2)) * (z *')))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by QUATERN2:1
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th25
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th25
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th25
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26
.= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))))*] by Th25
.= [*((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) / (|.z.| ^2)),0,0,0*]
.= [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] by Th11 ;
hence  z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] ; ::_thesis: verum
end;

theorem :: QUATERN3:30
for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2)
proof
let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2)
|.((z1 * z2) * z3).| ^2 = |.(z1 * (z2 * z3)).| ^2 by QUATERN2:16
.= (|.z1.| ^2) * (|.(z2 * z3).| ^2) by Th17
.= (|.z1.| ^2) * ((|.z2.| ^2) * (|.z3.| ^2)) by Th17
.= ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) ;
hence  |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) ; ::_thesis: verum
end;

theorem :: QUATERN3:31
for z1, z2, z3 being quaternion number holds Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2)
proof
let z1, z2, z3 be quaternion number ; ::_thesis: Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2)
Rea ((z1 * z2) * z3) = Rea (z1 * (z2 * z3)) by QUATERN2:16
.= Rea ((z2 * z3) * z1) by Th1
.= Rea (z2 * (z3 * z1)) by QUATERN2:16
.= Rea ((z3 * z1) * z2) by Th1 ;
hence  Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2) ; ::_thesis: verum
end;

theorem Th32: :: QUATERN3:32
for z being quaternion number holds |.(z * z).| = |.((z *') * (z *')).|
proof
let z be quaternion number ; ::_thesis: |.(z * z).| = |.((z *') * (z *')).|
|.((z *') * (z *')).| = |.(z *').| * |.(z *').| by QUATERNI:87
.= |.z.| * |.(z *').| by QUATERNI:73
.= |.z.| * |.z.| by QUATERNI:73 ;
hence  |.(z * z).| = |.((z *') * (z *')).| by QUATERNI:87; ::_thesis: verum
end;

theorem :: QUATERN3:33
for z being quaternion number holds |.((z *') * (z *')).| = |.z.| ^2
proof
let z be quaternion number ; ::_thesis: |.((z *') * (z *')).| = |.z.| ^2
 |.((z *') * (z *')).| = |.(z * z).| by Th32;
hence  |.((z *') * (z *')).| = |.z.| ^2 by QUATERNI:87; ::_thesis: verum
end;

theorem :: QUATERN3:34
for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.|
proof
let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.|
|.((z1 * z2) * z3).| = |.(z1 * (z2 * z3)).| by QUATERN2:16
.= |.z1.| * |.(z2 * z3).| by QUATERNI:87
.= |.z1.| * (|.z2.| * |.z3.|) by QUATERNI:87
.= (|.z1.| * |.z2.|) * |.z3.| ;
hence  |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.| ; ::_thesis: verum
end;

theorem :: QUATERN3:35
for z1, z2, z3 being quaternion number holds |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.|
proof
let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.|
 |.((z1 + z2) + z3).| = |.(z1 + (z2 + z3)).| by QUATERN2:2;
then  |.((z1 + z2) + z3).| <= |.z1.| + |.(z2 + z3).| by QUATERNI:79;
then A1: |.((z1 + z2) + z3).| - |.z1.| <= |.(z2 + z3).| by XREAL_1:20;
 |.(z2 + z3).| <= |.z2.| + |.z3.| by QUATERNI:79;
then  (|.((z1 + z2) + z3).| - |.z1.|) + |.(z2 + z3).| <= |.(z2 + z3).| + (|.z2.| + |.z3.|) by A1, XREAL_1:7;
then  |.((z1 + z2) + z3).| - |.z1.| <= (|.(z2 + z3).| + (|.z2.| + |.z3.|)) - |.(z2 + z3).| by XREAL_1:19;
then  |.((z1 + z2) + z3).| <= (|.z2.| + |.z3.|) + |.z1.| by XREAL_1:20;
hence  |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; ::_thesis: verum
end;

theorem :: QUATERN3:36
for z1, z2, z3 being quaternion number holds |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
proof
let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
 |.((z1 + z2) - z3).| = |.(z1 + (z2 - z3)).| by QUATERN2:2;
then  |.((z1 + z2) - z3).| <= |.z1.| + |.(z2 - z3).| by QUATERNI:79;
then A1: |.((z1 + z2) - z3).| - |.z1.| <= |.(z2 - z3).| by XREAL_1:20;
 |.(z2 - z3).| <= |.z2.| + |.z3.| by QUATERNI:80;
then  (|.((z1 + z2) - z3).| - |.z1.|) + |.(z2 - z3).| <= |.(z2 - z3).| + (|.z2.| + |.z3.|) by A1, XREAL_1:7;
then  |.((z1 + z2) - z3).| - |.z1.| <= (|.(z2 - z3).| + (|.z2.| + |.z3.|)) - |.(z2 - z3).| by XREAL_1:19;
then  |.((z1 + z2) - z3).| <= (|.z2.| + |.z3.|) + |.z1.| by XREAL_1:20;
hence  |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; ::_thesis: verum
end;

theorem :: QUATERN3:37
for z1, z2, z3 being quaternion number holds |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
proof
let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
 ( |.((z1 - z2) - z3).| <= |.(z1 - z2).| + |.z3.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:80;
then  |.((z1 - z2) - z3).| + |.(z1 - z2).| <= (|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|) by XREAL_1:7;
then  |.((z1 - z2) - z3).| <= ((|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|)) - |.(z1 - z2).| by XREAL_1:19;
hence  |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; ::_thesis: verum
end;

theorem :: QUATERN3:38
for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2
proof
let z1, z2 be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2
 ( |.z1.| - |.z2.| <= |.(z1 + z2).| & |.z1.| - |.z2.| <= |.(z1 - z2).| ) by QUATERNI:81, QUATERNI:82;
then  (|.z1.| - |.z2.|) + (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by XREAL_1:7;
then  2 * (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| ;
hence  |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 by XREAL_1:77; ::_thesis: verum
end;

theorem :: QUATERN3:39
for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2
proof
let z1, z2 be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2
 ( |.z1.| - |.z2.| <= |.(z1 + z2).| & |.z1.| - |.z2.| <= |.(z1 - z2).| ) by QUATERNI:81, QUATERNI:82;
then  (|.z1.| - |.z2.|) + (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by XREAL_1:7;
then  2 * (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z2 - z1).| by QUATERNI:83;
hence  |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 by XREAL_1:77; ::_thesis: verum
end;

theorem :: QUATERN3:40
for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).|
proof
let z1, z2 be quaternion number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).|
 |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by QUATERNI:86;
hence  |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| by QUATERNI:83; ::_thesis: verum
end;

theorem :: QUATERN3:41
for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.|
proof
let z1, z2 be quaternion number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.|
 ( |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:80, QUATERNI:86;
then  |.(|.z1.| - |.z2.|).| + |.(z1 - z2).| <= |.(z1 - z2).| + (|.z1.| + |.z2.|) by XREAL_1:7;
then  |.(|.z1.| - |.z2.|).| <= ((|.(z1 - z2).| + |.z1.|) + |.z2.|) - |.(z1 - z2).| by XREAL_1:19;
hence  |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.| ; ::_thesis: verum
end;

theorem :: QUATERN3:42
for z1, z2, z being quaternion number holds |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).|
proof
let z1, z2, z be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).|
 ( |.z1.| - |.z2.| <= |.(z1 - z2).| & |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| ) by QUATERNI:82, QUATERNI:85;
then  (|.z1.| - |.z2.|) + |.(z1 - z2).| <= |.(z1 - z2).| + (|.(z1 - z).| + |.(z - z2).|) by XREAL_1:7;
then  |.z1.| - |.z2.| <= ((|.(z1 - z2).| + |.(z1 - z).|) + |.(z - z2).|) - |.(z1 - z2).| by XREAL_1:19;
hence  |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| ; ::_thesis: verum
end;

theorem :: QUATERN3:43
for z1, z2 being quaternion number st |.z1.| - |.z2.| <> 0 holds
((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0
proof
let z1, z2 be quaternion number ; ::_thesis: ( |.z1.| - |.z2.| <> 0 implies ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 )
assume  |.z1.| - |.z2.| <> 0 ; ::_thesis: ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0
then  (|.z1.| - |.z2.|) ^2 > 0 by SQUARE_1:12;
hence  ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 ; ::_thesis: verum
end;

theorem :: QUATERN3:44
for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2
proof
let z1, z2 be quaternion number ; ::_thesis: |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2
 ( |.(z1 + z2).| <= |.z1.| + |.z2.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:79, QUATERNI:80;
then  |.(z1 + z2).| + |.(z1 - z2).| <= (|.z1.| + |.z2.|) + (|.z1.| + |.z2.|) by XREAL_1:7;
then  |.(z1 + z2).| + |.(z2 - z1).| <= 2 * (|.z1.| + |.z2.|) by QUATERNI:83;
hence  |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 by XREAL_1:79; ::_thesis: verum
end;

theorem :: QUATERN3:45
for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2
proof
let z1, z2 be quaternion number ; ::_thesis: |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2
 ( |.(z1 + z2).| <= |.z1.| + |.z2.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:79, QUATERNI:80;
then  |.(z1 + z2).| + |.(z1 - z2).| <= (|.z1.| + |.z2.|) + (|.z1.| + |.z2.|) by XREAL_1:7;
then  |.(z1 + z2).| + |.(z1 - z2).| <= 2 * (|.z1.| + |.z2.|) ;
hence  |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 by XREAL_1:79; ::_thesis: verum
end;

theorem :: QUATERN3:46
for z1, z2 being quaternion number holds (z1 * z2) " = (z2 ") * (z1 ")
proof
let z1, z2 be quaternion number ; ::_thesis: (z1 * z2) " = (z2 ") * (z1 ")
set z3 = z1 * z2;
A1: ((((Rea (z2 ")) * (Im1 (z1 "))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Im1 (z1 "))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (Im2 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((- (Im1 z1)) / (|.z1.| ^2))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2)))) by QUATERN2:29
.= (((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2)))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im2 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2)))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im2 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) - ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2) ;
A2: ((((Rea (z2 ")) * (Im2 (z1 "))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Im2 (z1 "))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2)))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((- (Im2 z1)) / (|.z1.| ^2))) + (((- (Im2 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
.= (((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im3 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) - ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2) ;
A3: ((((Rea (z2 ")) * (Im3 (z1 "))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Im3 (z1 "))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (Im1 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2)))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((- (Im3 z1)) / (|.z1.| ^2))) - (((Im3 z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))
.= (((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im1 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im2 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) - ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2) ;
((((Rea (z2 ")) * (Rea (z1 "))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Rea (z1 "))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (Im3 (z1 "))) by QUATERN2:29
.= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2)))) by QUATERN2:29
.= (((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76
.= (((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2) ;
then A4: (z2 ") * (z1 ") = ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + ((- ((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2))) * <i>)) + ((- ((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2))) * <j>)) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * <k>) by A1, A2, A3, QUATERNI:93
.= ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + (- (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * <i>))) + ((- ((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2))) * <j>)) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * <k>) by QUATERN2:9
.= ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + (- (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * <i>))) + (- (((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) * <j>))) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * <k>) by QUATERN2:9
.= ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) - (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * <i>)) - (((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) * <j>)) - (((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2)) * <k>) by QUATERN2:9 ;
(z1 * z2) " = ((((Rea (z1 * z2)) / (|.(z1 * z2).| ^2)) - (((Im1 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <i>)) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>) by QUATERN2:28
.= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <i>)) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>) by QUATERNI:87
.= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>) by QUATERNI:87
.= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>) by QUATERNI:87
.= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>) by QUATERNI:87
.= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>) by QUATERNI:97
.= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>) by QUATERNI:97
.= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>) by QUATERNI:97
.= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) / ((|.z1.| * |.z2.|) ^2)) * <k>) by QUATERNI:97 ;
hence  (z1 * z2) " = (z2 ") * (z1 ") by A4; ::_thesis: verum
end;

theorem :: QUATERN3:47
for z being quaternion number holds (z *') " = (z ") *'
proof
let z be quaternion number ; ::_thesis: (z *') " = (z ") *'
 Im1 ((z *') ") = - ((Im1 (z *')) / (|.(z *').| ^2)) by QUATERN2:29;
then A1: Im1 ((z *') ") = - ((- (Im1 z)) / (|.(z *').| ^2)) by QUATERNI:44;
 Im2 ((z *') ") = - ((Im2 (z *')) / (|.(z *').| ^2)) by QUATERN2:29;
then A2: Im2 ((z *') ") = - ((- (Im2 z)) / (|.(z *').| ^2)) by QUATERNI:44;
 Im2 ((z ") *') = - (Im2 (z ")) by QUATERNI:44;
then  Im2 ((z ") *') = - (- ((Im2 z) / (|.z.| ^2))) by QUATERN2:29;
then A3: Im2 ((z ") *') = - (- ((Im2 z) / (|.(z *').| ^2))) by QUATERNI:73;
 Im1 ((z ") *') = - (Im1 (z ")) by QUATERNI:44;
then  Im1 ((z ") *') = - (- ((Im1 z) / (|.z.| ^2))) by QUATERN2:29;
then A4: Im1 ((z ") *') = - (- ((Im1 z) / (|.(z *').| ^2))) by QUATERNI:73;
 Im3 ((z ") *') = - (Im3 (z ")) by QUATERNI:44;
then  Im3 ((z ") *') = - (- ((Im3 z) / (|.z.| ^2))) by QUATERN2:29;
then A5: Im3 ((z ") *') = - (- ((Im3 z) / (|.(z *').| ^2))) by QUATERNI:73;
 Rea ((z ") *') = Rea (z ") by QUATERNI:44;
then  Rea ((z ") *') = (Rea z) / (|.z.| ^2) by QUATERN2:29;
then A6: Rea ((z ") *') = (Rea z) / (|.(z *').| ^2) by QUATERNI:73;
 Im3 ((z *') ") = - ((Im3 (z *')) / (|.(z *').| ^2)) by QUATERN2:29;
then A7: Im3 ((z *') ") = - ((- (Im3 z)) / (|.(z *').| ^2)) by QUATERNI:44;
 Rea ((z *') ") = (Rea (z *')) / (|.(z *').| ^2) by QUATERN2:29;
then  Rea ((z *') ") = (Rea z) / (|.(z *').| ^2) by QUATERNI:44;
hence  (z *') " = (z ") *' by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:48
1q " = 1q
proof
A1: Im3 (1q ") = - ((Im3 1q) / (|.1q.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:29 ;
A2: Im2 (1q ") = - ((Im2 1q) / (|.1q.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:29 ;
A3: Im1 (1q ") = - ((Im1 1q) / (|.1q.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:29 ;
Rea (1q ") = (Rea 1q) / (|.1q.| ^2) by QUATERN2:29
.= 1 by QUATERNI:29, QUATERNI:68 ;
then  1q " = [*1,0,0,0*] by A3, A2, A1, QUATERNI:24;
hence  1q " = 1q by QUATERNI:24, QUATERNI:29; ::_thesis: verum
end;

theorem :: QUATERN3:49
for z1, z2 being quaternion number st |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " holds
z1 = z2
proof
let z1, z2 be quaternion number ; ::_thesis: ( |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " implies z1 = z2 )
assume that
A1: |.z1.| = |.z2.| and
A2: |.z1.| <> 0 and
A3: z1 " = z2 " ; ::_thesis: z1 = z2
A4: |.z1.| ^2 <> 0 by A2, XCMPLX_1:6;
 Im3 (z1 ") = - ((Im3 z1) / (|.z1.| ^2)) by QUATERN2:29;
then  - ((Im3 z1) / (|.z1.| ^2)) = - ((Im3 z2) / (|.z2.| ^2)) by A3, QUATERN2:29;
then A5: Im3 z1 = Im3 z2 by A1, A4, XCMPLX_1:53;
 Im2 (z1 ") = - ((Im2 z1) / (|.z1.| ^2)) by QUATERN2:29;
then  - ((Im2 z1) / (|.z1.| ^2)) = - ((Im2 z2) / (|.z2.| ^2)) by A3, QUATERN2:29;
then A6: Im2 z1 = Im2 z2 by A1, A4, XCMPLX_1:53;
 Im1 (z1 ") = - ((Im1 z1) / (|.z1.| ^2)) by QUATERN2:29;
then  - ((Im1 z1) / (|.z1.| ^2)) = - ((Im1 z2) / (|.z2.| ^2)) by A3, QUATERN2:29;
then A7: Im1 z1 = Im1 z2 by A1, A4, XCMPLX_1:53;
 Rea (z1 ") = (Rea z1) / (|.z1.| ^2) by QUATERN2:29;
then  (Rea z1) / (|.z1.| ^2) = (Rea z2) / (|.z2.| ^2) by A3, QUATERN2:29;
then  Rea z1 = Rea z2 by A1, A4, XCMPLX_1:53;
hence  z1 = z2 by A7, A6, A5, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:50
for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4)
(z1 - z2) * (z3 + z4) = ((z1 - z2) * z3) + ((z1 - z2) * z4) by QUATERN2:17
.= ((z1 * z3) - (z2 * z3)) + ((z1 - z2) * z4) by QUATERN2:23
.= ((z1 * z3) - (z2 * z3)) + ((z1 * z4) - (z2 * z4)) by QUATERN2:23
.= (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) by QUATERN2:2 ;
hence  (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) ; ::_thesis: verum
end;

theorem :: QUATERN3:51
for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4)
(z1 + z2) * (z3 + z4) = ((z1 + z2) * z3) + ((z1 + z2) * z4) by QUATERN2:17
.= ((z1 * z3) + (z2 * z3)) + ((z1 + z2) * z4) by QUATERN2:18
.= ((z1 * z3) + (z2 * z3)) + ((z1 * z4) + (z2 * z4)) by QUATERN2:18
.= (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) by QUATERN2:2 ;
hence  (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) ; ::_thesis: verum
end;

theorem Th52: :: QUATERN3:52
for z1, z2 being quaternion number holds - (z1 + z2) = (- z1) - z2
proof
let z1, z2 be quaternion number ; ::_thesis: - (z1 + z2) = (- z1) - z2
A1: (- z1) - z2 = ((- 1q) * z1) - z2 by QUATERN2:19
.= ((- 1q) * z1) + ((- 1q) * z2) by QUATERN2:19 ;
- (z1 + z2) = (- 1q) * (z1 + z2) by QUATERN2:19
.= ((- 1q) * z1) + ((- 1q) * z2) by QUATERN2:17 ;
hence  - (z1 + z2) = (- z1) - z2 by A1; ::_thesis: verum
end;

theorem Th53: :: QUATERN3:53
for z1, z2 being quaternion number holds - (z1 - z2) = (- z1) + z2
proof
let z1, z2 be quaternion number ; ::_thesis: - (z1 - z2) = (- z1) + z2
- (z1 - z2) = (- 1q) * (z1 - z2) by QUATERN2:19
.= ((- 1q) * z1) - ((- 1q) * z2) by QUATERN2:24
.= ((- 1q) * z1) - (- z2) by QUATERN2:19 ;
hence  - (z1 - z2) = (- z1) + z2 by QUATERN2:19; ::_thesis: verum
end;

theorem Th54: :: QUATERN3:54
for z, z1, z2 being quaternion number holds z - (z1 + z2) = (z - z1) - z2
proof
let z, z1, z2 be quaternion number ; ::_thesis: z - (z1 + z2) = (z - z1) - z2
A1: (z - z1) - z2 = (z + ((- 1q) * z1)) + (- z2) by QUATERN2:19
.= (z + ((- 1q) * z1)) + ((- 1q) * z2) by QUATERN2:19 ;
- (z1 + z2) = (- 1q) * (z1 + z2) by QUATERN2:19
.= ((- 1q) * z1) + ((- 1q) * z2) by QUATERN2:17 ;
hence  z - (z1 + z2) = (z - z1) - z2 by A1, QUATERN2:2; ::_thesis: verum
end;

theorem Th55: :: QUATERN3:55
for z, z1, z2 being quaternion number holds z - (z1 - z2) = (z - z1) + z2
proof
let z, z1, z2 be quaternion number ; ::_thesis: z - (z1 - z2) = (z - z1) + z2
- (z1 - z2) = (- 1q) * (z1 - z2) by QUATERN2:19
.= ((- 1q) * z1) - ((- 1q) * z2) by QUATERN2:24 ;
then z - (z1 - z2) = z + (((- 1q) * z1) - (- z2)) by QUATERN2:19
.= (z + ((- 1q) * z1)) + z2 by QUATERN2:2 ;
hence  z - (z1 - z2) = (z - z1) + z2 by QUATERN2:19; ::_thesis: verum
end;

theorem :: QUATERN3:56
for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4)
(z1 + z2) * (z3 - z4) = ((z1 + z2) * z3) - ((z1 + z2) * z4) by QUATERN2:24
.= ((z1 * z3) + (z2 * z3)) - ((z1 + z2) * z4) by QUATERN2:18
.= ((z1 * z3) + (z2 * z3)) - ((z1 * z4) + (z2 * z4)) by QUATERN2:18
.= (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) by Th54 ;
hence  (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) ; ::_thesis: verum
end;

theorem Th57: :: QUATERN3:57
for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4)
(z1 - z2) * (z3 - z4) = ((z1 - z2) * z3) - ((z1 - z2) * z4) by QUATERN2:24
.= ((z1 * z3) - (z2 * z3)) - ((z1 - z2) * z4) by QUATERN2:23
.= ((z1 * z3) - (z2 * z3)) - ((z1 * z4) - (z2 * z4)) by QUATERN2:23
.= (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) by Th55 ;
hence  (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) ; ::_thesis: verum
end;

theorem :: QUATERN3:58
for z1, z2, z3 being quaternion number holds - ((z1 + z2) + z3) = ((- z1) - z2) - z3
proof
let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 + z2) + z3) = ((- z1) - z2) - z3
- ((z1 + z2) + z3) = - (z1 + (z2 + z3)) by QUATERN2:2
.= (- z1) - (z2 + z3) by Th52
.= ((- z1) - z2) - z3 by Th54 ;
hence  - ((z1 + z2) + z3) = ((- z1) - z2) - z3 ; ::_thesis: verum
end;

theorem :: QUATERN3:59
for z1, z2, z3 being quaternion number holds - ((z1 - z2) - z3) = ((- z1) + z2) + z3
proof
let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 - z2) - z3) = ((- z1) + z2) + z3
- ((z1 - z2) - z3) = (- (z1 - z2)) + z3 by Th53
.= ((- z1) + z2) + z3 by Th53 ;
hence  - ((z1 - z2) - z3) = ((- z1) + z2) + z3 ; ::_thesis: verum
end;

theorem :: QUATERN3:60
for z1, z2, z3 being quaternion number holds - ((z1 - z2) + z3) = ((- z1) + z2) - z3
proof
let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 - z2) + z3) = ((- z1) + z2) - z3
- ((z1 - z2) + z3) = (- (z1 - z2)) - z3 by Th52
.= ((- z1) + z2) - z3 by Th53 ;
hence  - ((z1 - z2) + z3) = ((- z1) + z2) - z3 ; ::_thesis: verum
end;

theorem :: QUATERN3:61
for z1, z2, z3 being quaternion number holds - ((z1 + z2) - z3) = ((- z1) - z2) + z3
proof
let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 + z2) - z3) = ((- z1) - z2) + z3
- ((z1 + z2) - z3) = (- (z1 + z2)) + z3 by Th53
.= ((- z1) - z2) + z3 by Th52 ;
hence  - ((z1 + z2) - z3) = ((- z1) - z2) + z3 ; ::_thesis: verum
end;

theorem :: QUATERN3:62
for z1, z, z2 being quaternion number st z1 + z = z2 + z holds
z1 = z2
proof
let z1, z, z2 be quaternion number ; ::_thesis: ( z1 + z = z2 + z implies z1 = z2 )
A1: ( Rea (z1 + z) = (Rea z1) + (Rea z) & Im1 (z1 + z) = (Im1 z1) + (Im1 z) ) by QUATERNI:36;
A2: ( Im2 (z1 + z) = (Im2 z1) + (Im2 z) & Im3 (z1 + z) = (Im3 z1) + (Im3 z) ) by QUATERNI:36;
A3: ( Im2 (z2 + z) = (Im2 z2) + (Im2 z) & Im3 (z2 + z) = (Im3 z2) + (Im3 z) ) by QUATERNI:36;
A4: ( Rea (z2 + z) = (Rea z2) + (Rea z) & Im1 (z2 + z) = (Im1 z2) + (Im1 z) ) by QUATERNI:36;
assume  z1 + z = z2 + z ; ::_thesis: z1 = z2
hence  z1 = z2 by A1, A2, A4, A3, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:63
for z1, z, z2 being quaternion number st z1 - z = z2 - z holds
z1 = z2
proof
let z1, z, z2 be quaternion number ; ::_thesis: ( z1 - z = z2 - z implies z1 = z2 )
A1: ( Rea (z1 - z) = (Rea z1) - (Rea z) & Im1 (z1 - z) = (Im1 z1) - (Im1 z) ) by QUATERNI:42;
A2: ( Im2 (z1 - z) = (Im2 z1) - (Im2 z) & Im3 (z1 - z) = (Im3 z1) - (Im3 z) ) by QUATERNI:42;
A3: ( Im2 (z2 - z) = (Im2 z2) - (Im2 z) & Im3 (z2 - z) = (Im3 z2) - (Im3 z) ) by QUATERNI:42;
A4: ( Rea (z2 - z) = (Rea z2) - (Rea z) & Im1 (z2 - z) = (Im1 z2) - (Im1 z) ) by QUATERNI:42;
assume  z1 - z = z2 - z ; ::_thesis: z1 = z2
hence  z1 = z2 by A1, A2, A4, A3, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:64
for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4)
((z1 + z2) - z3) * z4 = ((z1 + z2) * z4) - (z3 * z4) by QUATERN2:23
.= ((z1 * z4) + (z2 * z4)) - (z3 * z4) by QUATERN2:18 ;
hence  ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4) ; ::_thesis: verum
end;

theorem :: QUATERN3:65
for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4)
((z1 - z2) + z3) * z4 = ((z1 - z2) * z4) + (z3 * z4) by QUATERN2:18
.= ((z1 * z4) - (z2 * z4)) + (z3 * z4) by QUATERN2:23 ;
hence  ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4) ; ::_thesis: verum
end;

theorem :: QUATERN3:66
for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4)
((z1 - z2) - z3) * z4 = ((z1 - z2) * z4) - (z3 * z4) by QUATERN2:23
.= ((z1 * z4) - (z2 * z4)) - (z3 * z4) by QUATERN2:23 ;
hence  ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4) ; ::_thesis: verum
end;

theorem :: QUATERN3:67
for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4)
((z1 + z2) + z3) * z4 = ((z1 + z2) * z4) + (z3 * z4) by QUATERN2:18
.= ((z1 * z4) + (z2 * z4)) + (z3 * z4) by QUATERN2:18 ;
hence  ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4) ; ::_thesis: verum
end;

theorem :: QUATERN3:68
for z1, z2, z3 being quaternion number holds (z1 - z2) * z3 = (z2 - z1) * (- z3)
proof
let z1, z2, z3 be quaternion number ; ::_thesis: (z1 - z2) * z3 = (z2 - z1) * (- z3)
(z2 - z1) * (- z3) = (z2 * (- z3)) - (z1 * (- z3)) by QUATERN2:23
.= (- (z2 * z3)) - (z1 * (- z3)) by QUATERN2:21
.= (- (z2 * z3)) - (- (z1 * z3)) by QUATERN2:21
.= (z1 * z3) - (z2 * z3) ;
hence  (z1 - z2) * z3 = (z2 - z1) * (- z3) by QUATERN2:23; ::_thesis: verum
end;

theorem :: QUATERN3:69
for z3, z1, z2 being quaternion number holds z3 * (z1 - z2) = (- z3) * (z2 - z1)
proof
let z3, z1, z2 be quaternion number ; ::_thesis: z3 * (z1 - z2) = (- z3) * (z2 - z1)
(- z3) * (z2 - z1) = ((- z3) * z2) - ((- z3) * z1) by QUATERN2:24
.= (- (z3 * z2)) - ((- z3) * z1) by QUATERN2:20
.= (- (z3 * z2)) - (- (z3 * z1)) by QUATERN2:20
.= (z3 * z1) - (z3 * z2) ;
hence  z3 * (z1 - z2) = (- z3) * (z2 - z1) by QUATERN2:24; ::_thesis: verum
end;

theorem Th70: :: QUATERN3:70
for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1
 Im1 (((z1 - z2) - z3) + z4) = (Im1 ((z1 - z2) - z3)) + (Im1 z4) by QUATERNI:36;
then  Im1 (((z1 - z2) - z3) + z4) = ((Im1 (z1 - z2)) - (Im1 z3)) + (Im1 z4) by QUATERNI:42;
then A1: Im1 (((z1 - z2) - z3) + z4) = (((Im1 z1) - (Im1 z2)) - (Im1 z3)) + (Im1 z4) by QUATERNI:42;
 Im2 (((z1 - z2) - z3) + z4) = (Im2 ((z1 - z2) - z3)) + (Im2 z4) by QUATERNI:36;
then  Im2 (((z1 - z2) - z3) + z4) = ((Im2 (z1 - z2)) - (Im2 z3)) + (Im2 z4) by QUATERNI:42;
then A2: Im2 (((z1 - z2) - z3) + z4) = (((Im2 z1) - (Im2 z2)) - (Im2 z3)) + (Im2 z4) by QUATERNI:42;
 Im2 (((z4 - z3) - z2) + z1) = (Im2 ((z4 - z3) - z2)) + (Im2 z1) by QUATERNI:36;
then  Im2 (((z4 - z3) - z2) + z1) = ((Im2 (z4 - z3)) - (Im2 z2)) + (Im2 z1) by QUATERNI:42;
then A3: Im2 (((z4 - z3) - z2) + z1) = (((Im2 z4) - (Im2 z3)) - (Im2 z2)) + (Im2 z1) by QUATERNI:42;
 Im1 (((z4 - z3) - z2) + z1) = (Im1 ((z4 - z3) - z2)) + (Im1 z1) by QUATERNI:36;
then  Im1 (((z4 - z3) - z2) + z1) = ((Im1 (z4 - z3)) - (Im1 z2)) + (Im1 z1) by QUATERNI:42;
then A4: Im1 (((z4 - z3) - z2) + z1) = (((Im1 z4) - (Im1 z3)) - (Im1 z2)) + (Im1 z1) by QUATERNI:42;
 Im3 (((z4 - z3) - z2) + z1) = (Im3 ((z4 - z3) - z2)) + (Im3 z1) by QUATERNI:36;
then  Im3 (((z4 - z3) - z2) + z1) = ((Im3 (z4 - z3)) - (Im3 z2)) + (Im3 z1) by QUATERNI:42;
then A5: Im3 (((z4 - z3) - z2) + z1) = (((Im3 z4) - (Im3 z3)) - (Im3 z2)) + (Im3 z1) by QUATERNI:42;
 Rea (((z4 - z3) - z2) + z1) = (Rea ((z4 - z3) - z2)) + (Rea z1) by QUATERNI:36;
then  Rea (((z4 - z3) - z2) + z1) = ((Rea (z4 - z3)) - (Rea z2)) + (Rea z1) by QUATERNI:42;
then A6: Rea (((z4 - z3) - z2) + z1) = (((Rea z4) - (Rea z3)) - (Rea z2)) + (Rea z1) by QUATERNI:42;
 Im3 (((z1 - z2) - z3) + z4) = (Im3 ((z1 - z2) - z3)) + (Im3 z4) by QUATERNI:36;
then  Im3 (((z1 - z2) - z3) + z4) = ((Im3 (z1 - z2)) - (Im3 z3)) + (Im3 z4) by QUATERNI:42;
then A7: Im3 (((z1 - z2) - z3) + z4) = (((Im3 z1) - (Im3 z2)) - (Im3 z3)) + (Im3 z4) by QUATERNI:42;
 Rea (((z1 - z2) - z3) + z4) = (Rea ((z1 - z2) - z3)) + (Rea z4) by QUATERNI:36;
then  Rea (((z1 - z2) - z3) + z4) = ((Rea (z1 - z2)) - (Rea z3)) + (Rea z4) by QUATERNI:42;
then  Rea (((z1 - z2) - z3) + z4) = (((Rea z1) - (Rea z2)) - (Rea z3)) + (Rea z4) by QUATERNI:42;
hence  ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1 by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:71
for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3)
proof
let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3)
(z2 - z1) * (z4 - z3) = ((z2 - z1) * z4) - ((z2 - z1) * z3) by QUATERN2:24
.= ((z2 * z4) - (z1 * z4)) - ((z2 - z1) * z3) by QUATERN2:23
.= ((z2 * z4) - (z1 * z4)) - ((z2 * z3) - (z1 * z3)) by QUATERN2:23
.= (((z2 * z4) - (z1 * z4)) - (z2 * z3)) + (z1 * z3) by Th55
.= (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) by Th70 ;
hence  (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3) by Th57; ::_thesis: verum
end;

theorem :: QUATERN3:72
for z, z1, z2 being quaternion number holds (z - z1) - z2 = (z - z2) - z1
proof
let z, z1, z2 be quaternion number ; ::_thesis: (z - z1) - z2 = (z - z2) - z1
 Im1 ((z - z1) - z2) = (Im1 (z - z1)) - (Im1 z2) by QUATERNI:42;
then A1: Im1 ((z - z1) - z2) = ((Im1 z) - (Im1 z1)) - (Im1 z2) by QUATERNI:42;
 Im2 ((z - z1) - z2) = (Im2 (z - z1)) - (Im2 z2) by QUATERNI:42;
then A2: Im2 ((z - z1) - z2) = ((Im2 z) - (Im2 z1)) - (Im2 z2) by QUATERNI:42;
 Im2 ((z - z2) - z1) = (Im2 (z - z2)) - (Im2 z1) by QUATERNI:42;
then A3: Im2 ((z - z2) - z1) = ((Im2 z) - (Im2 z2)) - (Im2 z1) by QUATERNI:42;
 Im1 ((z - z2) - z1) = (Im1 (z - z2)) - (Im1 z1) by QUATERNI:42;
then A4: Im1 ((z - z2) - z1) = ((Im1 z) - (Im1 z2)) - (Im1 z1) by QUATERNI:42;
 Im3 ((z - z2) - z1) = (Im3 (z - z2)) - (Im3 z1) by QUATERNI:42;
then A5: Im3 ((z - z2) - z1) = ((Im3 z) - (Im3 z2)) - (Im3 z1) by QUATERNI:42;
 Rea ((z - z2) - z1) = (Rea (z - z2)) - (Rea z1) by QUATERNI:42;
then A6: Rea ((z - z2) - z1) = ((Rea z) - (Rea z2)) - (Rea z1) by QUATERNI:42;
 Im3 ((z - z1) - z2) = (Im3 (z - z1)) - (Im3 z2) by QUATERNI:42;
then A7: Im3 ((z - z1) - z2) = ((Im3 z) - (Im3 z1)) - (Im3 z2) by QUATERNI:42;
 Rea ((z - z1) - z2) = (Rea (z - z1)) - (Rea z2) by QUATERNI:42;
then  Rea ((z - z1) - z2) = ((Rea z) - (Rea z1)) - (Rea z2) by QUATERNI:42;
hence  (z - z1) - z2 = (z - z2) - z1 by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; ::_thesis: verum
end;

theorem :: QUATERN3:73
for z being quaternion number holds z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*]
proof
let z be quaternion number ; ::_thesis: z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*]
z " = [*(Rea (z ")),(Im1 (z ")),(Im2 (z ")),(Im3 (z "))*] by QUATERNI:24
.= [*((Rea z) / (|.z.| ^2)),(Im1 (z ")),(Im2 (z ")),(Im3 (z "))*] by QUATERN2:29
.= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(Im2 (z ")),(Im3 (z "))*] by QUATERN2:29
.= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(Im3 (z "))*] by QUATERN2:29
.= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] by QUATERN2:29 ;
hence  z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] ; ::_thesis: verum
end;

theorem :: QUATERN3:74
for z1, z2 being quaternion number holds z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*]
proof
let z1, z2 be quaternion number ; ::_thesis: z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*]
z1 / z2 = [*(Rea (z1 / z2)),(Im1 (z1 / z2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERNI:24
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),(Im1 (z1 / z2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERN2:30
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERN2:30
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),(Im3 (z1 / z2))*] by QUATERN2:30
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] by QUATERN2:30 ;
hence  z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] ; ::_thesis: verum
end;

Lm2:  <i> = [*0,1*]
by ARYTM_0:def_5;

theorem :: QUATERN3:75
<i> " = - <i>
proof
A1: Im3 (<i> ") = - ((Im3 <i>) / (|.<i>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:30 ;
A2: Im2 (<i> ") = - ((Im2 <i>) / (|.<i>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:30 ;
A3: Im1 (<i> ") = - ((Im1 <i>) / (|.<i>.| ^2)) by QUATERN2:29
.= - 1 by QUATERNI:30, QUATERNI:69 ;
Rea (<i> ") = (Rea <i>) / (|.<i>.| ^2) by QUATERN2:29
.= 0 by QUATERNI:30 ;
then <i> " = [*(- 0),(- 1),(- 0),(- 0)*] by A3, A2, A1, QUATERNI:24
.= - [*0,1,0,0*] by QUATERN2:4
.= - <i> by Lm2, QUATERNI:def_6 ;
hence  <i> " = - <i> ; ::_thesis: verum
end;

theorem :: QUATERN3:76
<j> " = - <j>
proof
A1: Im3 (<j> ") = - ((Im3 <j>) / (|.<j>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:31 ;
A2: Im2 (<j> ") = - ((Im2 <j>) / (|.<j>.| ^2)) by QUATERN2:29
.= - 1 by QUATERNI:31, QUATERNI:70 ;
A3: Im1 (<j> ") = - ((Im1 <j>) / (|.<j>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:31 ;
Rea (<j> ") = (Rea <j>) / (|.<j>.| ^2) by QUATERN2:29
.= 0 by QUATERNI:31 ;
then <j> " = [*(- 0),(- 0),(- 1),(- 0)*] by A3, A2, A1, QUATERNI:24
.= - <j> by QUATERN2:4 ;
hence  <j> " = - <j> ; ::_thesis: verum
end;

theorem :: QUATERN3:77
<k> " = - <k>
proof
A1: Im3 (<k> ") = - ((Im3 <k>) / (|.<k>.| ^2)) by QUATERN2:29
.= - 1 by QUATERNI:31, QUATERNI:71 ;
A2: Im2 (<k> ") = - ((Im2 <k>) / (|.<k>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:31 ;
A3: Im1 (<k> ") = - ((Im1 <k>) / (|.<k>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:31 ;
Rea (<k> ") = (Rea <k>) / (|.<k>.| ^2) by QUATERN2:29
.= 0 by QUATERNI:31 ;
then <k> " = [*(- 0),(- 0),(- 0),(- 1)*] by A3, A2, A1, QUATERNI:24
.= - <k> by QUATERN2:4 ;
hence  <k> " = - <k> ; ::_thesis: verum
end;

definition
let z be quaternion number ;
funcz ^2  ->  set  equals :: QUATERN3:def 1
z * z;
correctness
coherence
z * z is set ;
;
end;

:: deftheorem  defines ^2 QUATERN3:def_1_:_
 for z being quaternion number holds z ^2 = z * z;

registration
let z be quaternion number ;
clusterz ^2  ->  quaternion ;
coherence
 z ^2 is quaternion ;
end;

definition
let z be Element of QUATERNION ;
:: original: ^2
redefine funcz ^2  ->  Element of QUATERNION ;
correctness
coherence
z ^2 is Element of QUATERNION ;
;
end;

theorem Th78: :: QUATERN3:78
for z being quaternion number holds z ^2 = [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*]
proof
let z be quaternion number ; ::_thesis: z ^2 = [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*]
z ^2 = [*(Rea (z ^2)),(Im1 (z ^2)),(Im2 (z ^2)),(Im3 (z ^2))*] by QUATERNI:24
.= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(Im1 (z ^2)),(Im2 (z ^2)),(Im3 (z ^2))*] by QUATERNI:40
.= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(Im2 (z ^2)),(Im3 (z ^2))*] by QUATERNI:40
.= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(Im3 (z ^2))*] by QUATERNI:40
.= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] by QUATERNI:40 ;
hence  z ^2 = [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] ; ::_thesis: verum
end;

theorem :: QUATERN3:79
0q ^2 = 0
proof
A1: 0q = [*0,0*] by ARYTM_0:def_5
.= [*0,0,0,0*] by QUATERNI:91 ;
then A2: ( Rea 0q = 0 & Im1 0q = 0 ) by QUATERNI:23;
A3: ( Im2 0q = 0 & Im3 0q = 0 ) by A1, QUATERNI:23;
0q ^2 = [*(((((Rea 0q) ^2) - ((Im1 0q) ^2)) - ((Im2 0q) ^2)) - ((Im3 0q) ^2)),(2 * ((Rea 0q) * (Im1 0q))),(2 * ((Rea 0q) * (Im2 0q))),(2 * ((Rea 0q) * (Im3 0q)))*] by Th78
.= [*0,0*] by A2, A3, QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  0q ^2 = 0 ; ::_thesis: verum
end;

theorem :: QUATERN3:80
1q ^2 = 1
proof
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
then A2: ( Rea 1q = 1 & Im1 1q = 0 ) by QUATERNI:23;
A3: ( Im2 1q = 0 & Im3 1q = 0 ) by A1, QUATERNI:23;
1q ^2 = [*(((((Rea 1q) ^2) - ((Im1 1q) ^2)) - ((Im2 1q) ^2)) - ((Im3 1q) ^2)),(2 * ((Rea 1q) * (Im1 1q))),(2 * ((Rea 1q) * (Im2 1q))),(2 * ((Rea 1q) * (Im3 1q)))*] by Th78
.= [*1,0*] by A2, A3, QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
hence  1q ^2 = 1 ; ::_thesis: verum
end;

theorem Th81: :: QUATERN3:81
for z being quaternion number holds z ^2 = (- z) ^2
proof
let z be quaternion number ; ::_thesis: z ^2 = (- z) ^2
(- z) ^2 = [*(((((Rea (- z)) ^2) - ((Im1 (- z)) ^2)) - ((Im2 (- z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by Th78
.= [*(((((- (Rea z)) ^2) - ((Im1 (- z)) ^2)) - ((Im2 (- z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((Im2 (- z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (- (Im2 z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (- (Im2 z)))),(2 * ((- (Rea z)) * (Im3 (- z))))*] by QUATERNI:41
.= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (- (Im2 z)))),(2 * ((- (Rea z)) * (- (Im3 z))))*] by QUATERNI:41
.= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] ;
hence  z ^2 = (- z) ^2 by Th78; ::_thesis: verum
end;

definition
let z be quaternion number ;
funcz ^3  ->  set  equals :: QUATERN3:def 2
(z * z) * z;
coherence
 (z * z) * z is set ;
end;

:: deftheorem  defines ^3 QUATERN3:def_2_:_
 for z being quaternion number holds z ^3 = (z * z) * z;

registration
let z be quaternion number ;
clusterz ^3  ->  quaternion ;
coherence
 z ^3 is quaternion ;
end;

definition
let z be Element of QUATERNION ;
:: original: ^3
redefine funcz ^3  ->  Element of QUATERNION ;
correctness
coherence
z ^3 is Element of QUATERNION ;
;
end;

theorem :: QUATERN3:82
0q ^3 = 0
proof
A1: 0q = [*0,0*] by ARYTM_0:def_5
.= [*0,0,0,0*] by QUATERNI:91 ;
then A2: ( Rea 0q = 0 & Im1 0q = 0 ) by QUATERNI:23;
A3: ( Im2 0q = 0 & Im3 0q = 0 ) by A1, QUATERNI:23;
0q ^2 = [*(((((Rea 0q) ^2) - ((Im1 0q) ^2)) - ((Im2 0q) ^2)) - ((Im3 0q) ^2)),(2 * ((Rea 0q) * (Im1 0q))),(2 * ((Rea 0q) * (Im2 0q))),(2 * ((Rea 0q) * (Im3 0q)))*] by Th78
.= [*0,0*] by A2, A3, QUATERNI:91
.= 0 by ARYTM_0:def_5 ;
hence  0q ^3 = 0 ; ::_thesis: verum
end;

theorem :: QUATERN3:83
1q ^3 = 1
proof
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
then A2: ( Rea 1q = 1 & Im1 1q = 0 ) by QUATERNI:23;
A3: ( Im2 1q = 0 & Im3 1q = 0 ) by A1, QUATERNI:23;
1q ^2 = [*(((((Rea 1q) ^2) - ((Im1 1q) ^2)) - ((Im2 1q) ^2)) - ((Im3 1q) ^2)),(2 * ((Rea 1q) * (Im1 1q))),(2 * ((Rea 1q) * (Im2 1q))),(2 * ((Rea 1q) * (Im3 1q)))*] by Th78
.= [*1,0*] by A2, A3, QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
hence  1q ^3 = 1 ; ::_thesis: verum
end;

theorem :: QUATERN3:84
<i> ^3 = - <i>
proof
 <i> = [*0,1,0,0*] by Lm2, QUATERNI:def_6;
then (<i> * <i>) * <i> = [*((((0 * 0) - (1 * 1)) - (0 * 0)) - (0 * 0)),((((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1))*] * [*0,1,0,0*] by QUATERNI:def_10
.= [*(((((- 1) * 0) - (0 * 1)) - (0 * 0)) - (0 * 0)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (1 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (0 * 1))*] by QUATERNI:def_10
.= - [*0,1,0,0*] by QUATERN2:4 ;
hence  <i> ^3 = - <i> by Lm2, QUATERNI:def_6; ::_thesis: verum
end;

theorem :: QUATERN3:85
<j> ^3 = - <j>
proof
(<j> * <j>) * <j> = [*((((0 * 0) - (0 * 0)) - (1 * 1)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 0)) - (0 * 1)),((((0 * 1) + (0 * 1)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0))*] * [*0,0,1,0*] by QUATERNI:def_10
.= [*(((((- 1) * 0) - (0 * 0)) - (0 * 1)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (0 * 1)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 1)) - (0 * 0))*] by QUATERNI:def_10
.= - [*0,0,1,0*] by QUATERN2:4 ;
hence  <j> ^3 = - <j> ; ::_thesis: verum
end;

theorem :: QUATERN3:86
<k> ^3 = - <k>
proof
(<k> * <k>) * <k> = [*((((0 * 0) - (0 * 0)) - (0 * 0)) - (1 * 1)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0)),((((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0))*] * [*0,0,0,1*] by QUATERNI:def_10
.= [*(((((- 1) * 0) - (0 * 0)) - (0 * 0)) - (0 * 1)),(((((- 1) * 0) + (0 * 0)) + (0 * 1)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (1 * 0)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0))*] by QUATERNI:def_10
.= - [*0,0,0,1*] by QUATERN2:4 ;
hence  <k> ^3 = - <k> ; ::_thesis: verum
end;

theorem :: QUATERN3:87
(- 1q) ^2 = 1
proof
1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
then A1: - 1q = [*(- 1),(- 0),(- 0),(- 0)*] by QUATERN2:4;
then A2: ( Rea (- 1q) = - 1 & Im1 (- 1q) = 0 ) by QUATERNI:23;
A3: ( Im2 (- 1q) = 0 & Im3 (- 1q) = 0 ) by A1, QUATERNI:23;
(- 1q) ^2 = [*(((((Rea (- 1q)) ^2) - ((Im1 (- 1q)) ^2)) - ((Im2 (- 1q)) ^2)) - ((Im3 (- 1q)) ^2)),(2 * ((Rea (- 1q)) * (Im1 (- 1q)))),(2 * ((Rea (- 1q)) * (Im2 (- 1q)))),(2 * ((Rea (- 1q)) * (Im3 (- 1q))))*] by Th78
.= [*1,0*] by A2, A3, QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
hence  (- 1q) ^2 = 1 ; ::_thesis: verum
end;

theorem :: QUATERN3:88
(- 1q) ^3 = - 1
proof
A1: 1q = [*1,0*] by ARYTM_0:def_5
.= [*1,0,0,0*] by QUATERNI:91 ;
then A2: - 1q = [*(- 1),(- 0),(- 0),(- 0)*] by QUATERN2:4;
then A3: ( Rea (- 1q) = - 1 & Im1 (- 1q) = 0 ) by QUATERNI:23;
A4: ( Im2 (- 1q) = 0 & Im3 (- 1q) = 0 ) by A2, QUATERNI:23;
(- 1q) ^2 = [*(((((Rea (- 1q)) ^2) - ((Im1 (- 1q)) ^2)) - ((Im2 (- 1q)) ^2)) - ((Im3 (- 1q)) ^2)),(2 * ((Rea (- 1q)) * (Im1 (- 1q)))),(2 * ((Rea (- 1q)) * (Im2 (- 1q)))),(2 * ((Rea (- 1q)) * (Im3 (- 1q))))*] by Th78
.= [*1,0*] by A3, A4, QUATERNI:91
.= 1 by ARYTM_0:def_5 ;
then (- 1q) ^3 = - 1q by QUATERN2:15
.= [*(- 1),(- 0),(- 0),(- 0)*] by A1, QUATERN2:4
.= [*(- 1),(- 0)*] by QUATERNI:91
.= - 1 by ARYTM_0:def_5 ;
hence  (- 1q) ^3 = - 1 ; ::_thesis: verum
end;

theorem :: QUATERN3:89
for z being quaternion number holds z ^3 = - ((- z) ^3)
proof
let z be quaternion number ; ::_thesis: z ^3 = - ((- z) ^3)
A1: z ^3 = z * (z ^2) by QUATERN2:16;
(- z) ^3 = (- z) * ((- z) ^2) by QUATERN2:16
.= (- z) * (z ^2) by Th81
.= ((- 1q) * z) * (z ^2) by QUATERN2:19
.= (- 1q) * (z * (z ^2)) by QUATERN2:16
.= - (z ^3) by A1, QUATERN2:19 ;
hence  z ^3 = - ((- z) ^3) ; ::_thesis: verum
end;