:: Some Operations on Quaternion Numbers
:: by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, QUATERNI, ORDINAL1, SUBSET_1, RELAT_1, ARYTM_1, ARYTM_3,
ARYTM_0, REAL_1, CARD_1, XCMPLX_0, COMPLEX1, SQUARE_1, XXREAL_0,
POLYEQ_3, FUNCT_7;
notations SUBSET_1, ORDINAL1, FUNCT_7, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1,
XREAL_0, ARYTM_0, QUATERNI, REAL_1, SQUARE_1, QUATERN2;
constructors FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, COMPLEX1, RFUNCT_1, QUATERN2,
FUNCT_7, NUMBERS;
registrations MEMBERED, QUATERNI, XREAL_0, SQUARE_1;
requirements NUMERALS, SUBSET, REAL, ARITHM;
equalities SQUARE_1, XCMPLX_0, QUATERNI;
theorems ARYTM_0, SQUARE_1, XREAL_1, QUATERNI, QUATERN2, XCMPLX_1, XREAL_0;
begin
reserve z1,z2,z3,z4,z for Quaternion;
theorem Th1:
Rea (z1*z2) = Rea (z2*z1)
proof
Rea(z2*z1) = (Rea z2 * Rea z1 - Im1 z2 * Im1 z1 - Im2 z2 * Im2 z1 -
Im3 z2 * Im3 z1) by QUATERNI:97;
hence thesis by QUATERNI:97;
end;
Lm1: z is Real implies z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0
proof
assume z is Real;
then reconsider x = z as Element of REAL by XREAL_0:def 1;
x = [*x,In(0,REAL)*] & [*x,In(0,REAL)*] = [*x,0,0,0*]
by ARYTM_0:def 5,QUATERNI:91;
hence thesis by QUATERNI:23;
end;
theorem
z is Real implies z+z3 = Rea z + Rea z3+Im1 z3 *<i>+Im2 z3 *<j>+Im3 z3 *<k>
proof
reconsider z1 = z + z3 as Quaternion;
assume
A1: z is Real; 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 z2 = Rea z + Rea z3 by QUATERNI:23
.= Rea z1 by QUATERNI:36;
A4: Im1 z2 = Im1 z+ Im1 z3 by QUATERNI:23
.= Im1 z1 by QUATERNI:36;
A5: Im3 z2 = Im3 z + Im3 z3 by QUATERNI:23
.= Im3 z1 by QUATERNI:36;
A6: Im2 z2 = 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 thesis by QUATERN2:1;
end;
theorem
z is Real implies z-z3 = [* Rea z -Rea z3,-Im1 z3,-Im2 z3,-Im3 z3*]
proof
reconsider z1 = z+(-z3) as Quaternion;
assume
A1: z is Real; 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 z2 = Rea z +(-Rea z3) by QUATERNI:23
.= Rea z + Rea (-z3) by QUATERNI:41
.= Rea z1 by QUATERNI:36;
A4: Im1 z2 = Im1 z+(-Im1 z3) by QUATERNI:23
.=Im1 z+Im1 (- z3) by QUATERNI:41
.= Im1 z1 by QUATERNI:36;
A5: Im3 z2 = Im3 z +(-Im3 z3) by QUATERNI:23
.=Im3 z+Im3 (- z3) by QUATERNI:41
.= Im3 z1 by QUATERNI:36;
A6: Im2 z2 = 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 thesis by A2,A3,A4,A6,A5,QUATERNI:25;
end;
theorem
z is Real implies z*z3 = [* Rea z*Rea z3,Rea z*Im1 z3,Rea z*Im2 z3,Rea
z*Im3 z3*]
proof
assume
A1: z is Real; 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;
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 z1 = 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 z1 = 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 z1 = 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 z1 = 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 thesis by A4,A5,A6,QUATERNI:25;
end;
Im1 z = 0 & Im2 z = 0 by A1,Lm1;
hence thesis by A2,A3;
end;
theorem
z is Real implies z*<i>=[*0,Rea z,0,0*]
proof
assume
A1: z is Real;
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 thesis;
end;
theorem
z is Real implies z*<j>=[*0,0,Rea z,0*]
proof
assume
A1: z is Real;
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 thesis;
end;
theorem
z is Real implies z*<k>=[*0,0,0,Rea z*]
proof
assume
A1: z is Real;
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 thesis;
end;
theorem
z - 0q = z
proof
consider x,y,w,v be Real such that
A1: z = [*x,y,w,v*] by QUATERNI:7;
0q = [*In(0,REAL),In(0,REAL)*] 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 thesis by A1;
end;
theorem
z is Real implies z*z1 = z1*z
proof
assume
A1: z is Real; 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 thesis by A2,A3,QUATERNI:93;
end;
theorem
Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = Rea z
proof
set x = Rea z;
assume Im1 z=0 & Im2 z = 0 & Im3 z = 0;
then A1: z=[*x,0,0,0*] by QUATERNI:24;
reconsider xx=x, zz=0 as Element of REAL by XREAL_0:def 1;
[*x,0,0,0*]=[*xx,zz*] by QUATERNI:91;
hence thesis by A1,ARYTM_0:def 5;
end;
theorem Th11:
|.z.| ^2 = (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2
proof
(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 thesis;
end;
theorem
|.z.| ^2 = |.z*z*'.|
proof
|.z*z.| = |.z*z*'.| & |.z.| ^2 =
(Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z) ^2 by Th11,QUATERNI:89;
hence thesis by QUATERNI:88;
end;
theorem
|.z.| ^2 = Rea (z * z*')
proof
Rea(z*z*') = (Rea z)^2+(Im1 z)^2+(Im2 z)^2+(Im3 z)^2 by QUATERNI:60;
hence thesis by Th11;
end;
theorem
2 * Rea z = Rea (z+ z*')
proof
z = [*Rea z, Im1 z, Im2 z, Im3 z*] & z*' = [*Rea z, -Im1 z, -Im2 z, -Im3
z*] by QUATERNI:24,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 thesis by QUATERNI:23;
end;
theorem
z is Real implies (z * z1)*' = z*' * z1*'
proof
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;
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*', z2 = z1*';
A12: z3 * z2 =
(Rea z3 * Rea z2 - Im1 z3 * Im1 z2 - Im2 z3 * Im2 z2 - Im3 z3 * Im3 z2) +
(Rea z3 * Im1 z2 + Im1 z3 * Rea z2 + Im2 z3 * Im3 z2 - Im3 z3 * Im2 z2)*<i> +
(Rea z3 * Im2 z2 + Im2 z3 * Rea z2 + Im3 z3 * Im1 z2 - Im1 z3 * Im3 z2)*<j> +
(Rea z3 * Im3 z2 + Im3 z3 * Rea z2 + Im1 z3 * Im2 z2 - Im2 z3 * Im1 z2)*<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 thesis by A5,A6,A1,A2,A8,A7,A12,QUATERNI:44;
end;
theorem
(z1*z2)*' = z2*' * z1*'
proof
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*', z4 = z1*';
A9: z3 * z4 =
(Rea z3 * Rea z4 - Im1 z3 * Im1 z4 - Im2 z3 * Im2 z4 - Im3 z3 * Im3 z4) +
(Rea z3 * Im1 z4 + Im1 z3 * Rea z4 + Im2 z3 * Im3 z4 - Im3 z3 * Im2 z4)*<i> +
(Rea z3 * Im2 z4 + Im2 z3 * Rea z4 + Im3 z3 * Im1 z4 - Im1 z3 * Im3 z4)*<j> +
(Rea z3 * Im3 z4 + Im3 z3 * Rea z4 + Im1 z3 * Im2 z4 - Im2 z3 * Im1 z4)*<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 thesis by A1,A2,A6,A5,A9;
end;
theorem Th17:
|.z1*z2.|^2 = |.z1.| ^2 * |.z2.| ^2
proof
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 thesis by A1,A2,Th11;
end;
theorem
<i>*z1-z1*<i> = [*0,0,-2*Im3 z1,2*Im2 z1*]
proof
set z = <i>; set s = z*z1-z1*z;
A1: Rea (z1 * z) =
Rea z1 * Rea z - Im1 z1 * Im1 z - Im2 z1 * Im2 z - Im3 z1 * Im3 z &
Im1 (z1 * z) =
Rea z1 * Im1 z + Im1 z1 * Rea z + Im2 z1 * Im3 z - Im3 z1 * Im2 z &
Im2 (z1 * z) =
Rea z1 * Im2 z + Im2 z1 * Rea z + Im3 z1 * Im1 z - Im1 z1 * Im3 z &
Im3 (z1 * z) =
Rea z1 * Im3 z + Im3 z1 * Rea z + Im1 z1 * Im2 z - Im2 z1 * Im1 z
by QUATERNI:97;
A2: Im2 (z * z1) =
Rea z * Im2 z1 + Im2 z * Rea z1 + Im3 z * Im1 z1 - Im1 z * Im3 z1 &
Im3 (z * z1) =
Rea z * Im3 z1 + Im3 z * Rea z1 + Im1 z * Im2 z1 - Im2 z * Im1 z1
by QUATERNI:97;
Rea (z*z1)= -Im1 z1 & Im1 (z*z1) = Rea z1 by A1,QUATERNI:30,97; then
A3: Rea s = -Im1 z1 - -Im1 z1 & Im1 s = Rea z1 - Rea z1 by A1,QUATERNI:30,42;
Im2 s = -Im3 z1 - Im3 z1 &
Im3 s = Im2 z1 -- Im2 z1 by A2,A1,QUATERNI:30,42;
hence thesis by A3,QUATERNI:24;
end;
theorem
<i>*z1+z1*<i> = [*-2*Im1 z1,2*Rea z1,0,0*]
proof
set z = <i>;
A1: 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
.= [*-Im1 z1,Rea z1,-Im3 z1,Im2 z1*] by QUATERN2:1,QUATERNI:30;then
A2: Im2 (z*z1)= -Im3 z1 & Im3 (z*z1) =Im2 z1 by QUATERNI:23;
A3: 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
.= [*- Im1 z1,Rea z1,Im3 z1,- Im2 z1*] by QUATERN2:1,QUATERNI:30; then
A4: Rea (z1*z)= -Im1 z1 & Im1 (z1*z)=Rea z1 by QUATERNI:23;
A5: Im2 (z1*z)= Im3 z1 & Im3 (z1*z) =-Im2 z1 by A3,QUATERNI:23;
Rea (z*z1)= -Im1 z1 & Im1 (z*z1)=Rea z1 by A1,QUATERNI:23;
then z*z1+z1*z = (-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 thesis by QUATERN2:1;
end;
theorem
<j>*z1-z1*<j> = [*0,2*Im3 z1,0,-2*Im1 z1*]
proof
set z = <j>;
A1: 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
.= [*-Im2 z1,Im3 z1,Rea z1,-Im1 z1*] by QUATERN2:1,QUATERNI:31;
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
.= [*-Im2 z1,- Im3 z1,Rea z1,Im1 z1*] by QUATERN2:1,QUATERNI:31; then
z*z1-z1*z = [*-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 thesis;
end;
theorem
<j>*z1+z1*<j> = [*-2*Im2 z1,0,2*Rea z1,0*]
proof
set z = <j>;
A1: 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
.= [*-Im2 z1,Im3 z1,Rea z1,-Im1 z1*] by QUATERN2:1,QUATERNI:31; then
A2: Im2(z*z1)=Rea z1 & Im3(z*z1) =-Im1 z1 by QUATERNI:23;
A3: 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
.= [*-Im2 z1,- Im3 z1,Rea z1,Im1 z1*] by QUATERN2:1,QUATERNI:31; then
A4: Rea(z1*z)= -Im2 z1 & Im1 (z1*z)=-Im3 z1 by QUATERNI:23;
A5: Im2(z1*z)=Rea z1 & Im3(z1*z) =Im1 z1 by A3,QUATERNI:23;
Rea(z*z1)= -Im2 z1 & Im1 (z*z1)=Im3 z1 by A1,QUATERNI:23; then
z1*z+z*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 thesis by QUATERN2:1;
end;
theorem
<k>*z1-z1*<k> = [*0,-2*Im2 z1,2*Im1 z1,0*]
proof
set z = <k>;
A1: 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
.= [*-Im3 z1,-Im2 z1,Im1 z1,Rea z1 *] by QUATERN2:1,QUATERNI:31;
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
.= [*-Im3 z1,Im2 z1,-Im1 z1,Rea z1*] by QUATERN2:1,QUATERNI:31; then
z*z1-z1*z = [*-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 thesis;
end;
theorem
<k>*z1+z1*<k> = [*-2*Im3 z1,0,0,2*Rea z1*]
proof
set z = <k>;
A1: 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
.= [*-Im3 z1,-Im2 z1,Im1 z1,Rea z1 *] by QUATERN2:1,QUATERNI:31; then
A2: Im2(z*z1)=Im1 z1 & Im3(z*z1) =Rea z1 by QUATERNI:23;
A3: 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
.= [*-Im3 z1,Im2 z1,-Im1 z1,Rea z1*] by QUATERN2:1,QUATERNI:31; then
A4: Rea(z1*z)= -Im3 z1 & Im1 (z1*z)=Im2 z1 by QUATERNI:23;
A5: Im2(z1*z)=-Im1 z1 & Im3(z1*z) = Rea z1 by A3,QUATERNI:23;
Rea(z*z1)= -Im3 z1 & Im1 (z*z1)=-Im2 z1 by A1,QUATERNI:23; then
z1*z+z*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 thesis by QUATERN2:1;
end;
theorem Th24:
Rea (1/(|.z.| ^2) * z*') = 1/(|.z.| ^2)*Rea z
proof
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 thesis by QUATERNI:23;
end;
theorem Th25:
Im1 (1/(|.z.| ^2) * z*') = -1/(|.z.| ^2)*Im1 z
proof
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 thesis by QUATERNI:23;
end;
theorem Th26:
Im2 (1/(|.z.| ^2) * z*') = -1/(|.z.|^2)*Im2 z
proof
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 thesis by QUATERNI:23;
end;
theorem Th27:
Im3 (1/(|.z.| ^2) * z*') = -1/(|.z.|^2)*Im3 z
proof
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 thesis by QUATERNI:23;
end;
theorem
(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
set zz = |.z.| ^2;
(1/zz * z*')=[*Rea ((1/zz * z*')),Im1 ((1/zz * z*')),Im2 ((1/zz * z*')),
Im3 ((1/zz * z*'))*] by QUATERNI:24; then
(1/zz * z*')=[*1/zz*Rea z, Im1 ((1/zz * z*')),Im2 ((1/zz * z*')),Im3 ((1
/zz * z*'))*] by Th24; then
(1/zz * z*')=[*1/zz*Rea z, -1/zz*Im1 z, Im2 ((1/zz * z*')),Im3 ((1/zz *
z*'))*] by Th25; then
(1/zz * z*')=[*1/zz*Rea z, -1/zz*Im1 z, -1/zz*Im2 z, Im3 ((1/zz * z*'))
*] by Th26;
hence thesis by Th27;
end;
theorem
z * (1/(|.z.| ^2) * z*') = [* (|.z.| ^2)/(|.z.| ^2),0,0,0*]
proof
set zz = |.z.| ^2;
set z3 = 1/zz * z*';
z*(1/zz * z*')=
(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)*<i> +
(Rea z * Im2 z3 + Im2 z * Rea z3 + Im3 z * Im1 z3 - Im1 z * Im3 z3)*<j> +
(Rea z * Im3 z3 + Im3 z * Rea z3 + Im1 z * Im2 z3 - Im2 z * Im1 z3)*<k>
by QUATERNI:93
.= [*(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 QUATERN2:1
.=[*(Rea z * (1/zz*Rea z) - 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 Th24
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - 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 Th25
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - 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 Th26
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (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 Th27
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z)+ Im1 z * Rea (1/zz * z*') +
Im2 z * Im3 (1/zz * z*') - Im3 z * Im2 (1/zz * z*')), (Rea z * Im2 (1/zz * z*')
+ Im2 z * Rea (1/zz * z*') + Im3 z * Im1 (1/zz * z*') - Im1 z * Im3 (1/zz * z*'
)), (Rea z * Im3 (1/zz * z*') + Im3 z * Rea (1/zz * z*') + Im1 z * Im2 (1/zz *
z*') - Im2 z * Im1 (1/zz * z*'))*] by Th25
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z)+ Im1 z * (1/zz*Rea z) + Im2
z * Im3 (1/zz * z*') - Im3 z * Im2 (1/zz * z*')), (Rea z * Im2 (1/zz * z*') +
Im2 z * Rea (1/zz * z*') + Im3 z * Im1 (1/zz * z*') - Im1 z * Im3 (1/zz * z*'))
, (Rea z * Im3 (1/zz * z*') + Im3 z * Rea (1/zz * z*') + Im1 z * Im2 (1/zz * z
*') - Im2 z * Im1 (1/zz * z*'))*] by Th24
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z)+ Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - 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 Th27
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z)+ Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (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 Th26
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z)+ Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + 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 Th26
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z)+ Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * Im1 (z3) - Im1 z * Im3 (z3)), (Rea z * Im3 (z3) + Im3 z *
Rea (z3) + Im1 z * Im2 (z3) - Im2 z * Im1 (1/zz * z*'))*] by Th24
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z) + Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * (-1/zz*Im1 z) - Im1 z * Im3 (z3)), (Rea z * Im3 (z3) + Im3
z * Rea (z3) + Im1 z * Im2 (z3) - Im2 z * Im1 (z3))*] by Th25
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z) + Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * (-1/zz*Im1 z) - Im1 z * (-1/zz*Im3 z)), (Rea z * Im3 (1/zz
* z*') + Im3 z * Rea (z3) + Im1 z * Im2 (z3) - Im2 z * Im1 (z3))*] by Th27
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z) + Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * (-1/zz*Im1 z) - Im1 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*
Im3 z) + Im3 z * Rea (1/zz * z*') + Im1 z * Im2 (1/zz * z*') - Im2 z * Im1 (1/
zz * z*'))*] by Th27
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z) + Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * (-1/zz*Im1 z) - Im1 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*
Im3 z) + Im3 z * (1/zz*Rea z) + Im1 z * Im2 (1/zz * z*') - Im2 z * Im1 (1/zz *
z*'))*] by Th24
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z) + Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * (-1/zz*Im1 z) - Im1 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*
Im3 z) + Im3 z * (1/zz*Rea z) + Im1 z * (-1/zz*Im2 z) - Im2 z * Im1 (1/zz * z*'
))*] by Th26
.=[*(Rea z * (1/zz*Rea z) - Im1 z * (-1/zz*Im1 z) - Im2 z * (-1/zz*Im2 z
) - Im3 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*Im1 z) + Im1 z * (1/zz*Rea z) + Im2
z * (-1/zz*Im3 z) - Im3 z * (-1/zz*Im2 z)), (Rea z * (-1/zz*Im2 z) + Im2 z * (1
/zz*Rea z) + Im3 z * (-1/zz*Im1 z) - Im1 z * (-1/zz*Im3 z)), (Rea z * (-1/zz*
Im3 z) + Im3 z * (1/zz*Rea z) + Im1 z * (-1/zz*Im2 z) - Im2 z * (-1/zz*Im1 z))
*] by Th25
.=[*((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2)/zz, 0,0,0*]
.=[*zz/zz, 0,0,0*] by Th11;
hence thesis;
end;
theorem
|.z1*z2*z3.| ^2 = |.z1.| ^2 * |.z2.| ^2 * |.z3.| ^2
proof
|.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 thesis;
end;
theorem
Rea(z1*z2*z3) = Rea (z3*z1*z2)
proof
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 thesis;
end;
theorem Th32:
|.z*z.| = |.z*'* z*'.|
proof
|.z*'* z*'.|=|.z*'.|*|.z*'.| by QUATERNI:87
.=|.z.|*|.z*'.| by QUATERNI:73
.=|.z.|*|.z.| by QUATERNI:73;
hence thesis by QUATERNI:87;
end;
theorem
|.z*'* z*'.| = |.z.| ^2
proof
|.z*'* z*'.| = |.z*z.| by Th32;
hence thesis by QUATERNI:87;
end;
theorem
|.z1*z2*z3.| = |.z1.|*|.z2.|*|.z3.|
proof
|.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 thesis;
end;
theorem
|.z1+z2+z3.| <= |.z1.| + |.z2.|+|.z3.|
proof
|.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 thesis;
end;
theorem
|.z1+z2-z3.| <= |.z1.| + |.z2.| + |.z3.|
proof
|.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 thesis;
end;
theorem
|.z1-z2-z3.| <= |.z1.| + |.z2.| + |.z3.|
proof
|.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 thesis;
end;
theorem
|.z1.| - |.z2.| <= (|.z1 + z2.|+|.z1-z2.|)/2
proof
|.z1.| - |.z2.| <= |.z1 + z2.| & |.z1.| - |.z2.| <= |.z1 - z2.| by
QUATERNI:81,82; then
(|.z1.| - |.z2.|) +(|.z1.| - |.z2.|) <= |.z1 + z2.| + |.z1 - z2.| by
XREAL_1:7;
then 2*(|.z1.| - |.z2.|) <=|.z1 + z2.| + |.z1 - z2.|;
hence thesis by XREAL_1:77;
end;
theorem
|.z1.| - |.z2.| <= (|.z1 + z2.|+|.z2-z1.|)/2
proof
|.z1.| - |.z2.| <= |.z1 + z2.| & |.z1.| - |.z2.| <= |.z1 - z2.| by
QUATERNI:81,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 thesis by XREAL_1:77;
end;
theorem
|.|.z1.| - |.z2.|.| <= |.z2 - z1.|
proof
|.|.z1.| - |.z2.|.| <= |.z1 - z2.| by QUATERNI:86;
hence thesis by QUATERNI:83;
end;
theorem
|.|.z1.| - |.z2.|.| <= |.z1.| + |.z2.|
proof
|.|.z1.| - |.z2.|.| <= |.z1 - z2.| & |.z1 - z2.| <= |.z1.| + |.z2.| by
QUATERNI:80,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 thesis;
end;
theorem
|.z1.| - |.z2.| <= |.z1 - z.| + |.z - z2.|
proof
|.z1.| - |.z2.| <= |.z1 - z2.| & |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
by QUATERNI:82,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 thesis;
end;
theorem
|.z1.|-|.z2.|<>0 implies |.z1.|^2+|.z2.|^2 -2*|.z1.|*|.z2.| >0
proof
assume |.z1.|-|.z2.|<>0;
then (|.z1.|-|.z2.|)^2 >0 by SQUARE_1:12;
hence thesis;
end;
theorem
|.z1.| + |.z2.| >= (|.z1 + z2.|+|.z2 - z1.|)/2
proof
|.z1 + z2.| <= |.z1.| + |.z2.| & |.z1 - z2.| <= |.z1.| + |.z2.| by QUATERNI:79
,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 thesis by XREAL_1:79;
end;
theorem
|.z1.| + |.z2.| >= (|.z1 + z2.|+|.z1 - z2.|)/2
proof
|.z1 + z2.| <= |.z1.| + |.z2.| & |.z1 - z2.| <= |.z1.| + |.z2.| by
QUATERNI:79,80;
then |.z1 + z2.|+|.z1 - z2.| <= |.z1.| + |.z2.|+(|.z1.| + |.z2.|) by
XREAL_1:7;
then |.z1 + z2.|+|.z1 - z2.| <= 2*(|.z1.| + |.z2.|);
hence thesis by XREAL_1:79;
end;
theorem
(z1*z2)" = z2" * z1"
proof
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;
z3" = Rea z3 / (|.z3.|^2) - Im1 z3 / (|.z3.|^2)*<i> - Im2 z3 / (|.z3.|^2)
*<j> - (Im3 z3) / (|.z3.|^2)*<k> by QUATERN2:28
.= Rea z3 / (|.z1.|*|.z2.|)^2 - Im1 (z3) / |.z3.|^2*<i> - Im2 (z3) /|.z3
.|^2*<j> - (Im3 (z3)) / |.z3.|^2*<k> by QUATERNI:87
.= Rea (z3) / (|.z1.|*|.z2.|)^2 -Im1 (z3) / (|.z1.|*|.z2.|)^2*<i> - Im2
(z3) /|.z3.|^2*<j> - (Im3 (z3)) / |.z3.|^2*<k> by QUATERNI:87
.= Rea (z3) / (|.z1.|*|.z2.|)^2 -Im1 (z3) / (|.z1.|*|.z2.|)^2*<i> - Im2
(z3) /(|.z1.|*|.z2.|)^2*<j> - (Im3 (z3)) / |.z3.|^2*<k> by QUATERNI:87
.= Rea (z3) / (|.z1.|*|.z2.|)^2 -Im1 (z3) / (|.z1.|*|.z2.|)^2*<i> - Im2
(z3) /(|.z1.|*|.z2.|)^2*<j> - (Im3 (z3)) /(|.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 thesis by A4;
end;
theorem
(z*')" = (z")*'
proof
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 thesis by A1,A2,A7,A6,A4,A3,A5,QUATERNI:25;
end;
theorem
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;
then 1q"=[*1,0,0,0*] by A3,A2,A1,QUATERNI:24;
hence thesis by QUATERNI:24,29;
end;
theorem
|.z1.|=|.z2.| & |.z1.| <>0 & z1"=z2" implies z1=z2
proof
assume that
A1: |.z1.|=|.z2.| and
A2: |.z1.| <>0 and
A3: 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 thesis by A7,A6,A5,QUATERNI:25;
end;
theorem
(z1-z2)*(z3+z4)=z1*z3-z2*z3+z1*z4-z2*z4
proof
(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 thesis;
end;
theorem
(z1+z2)*(z3+z4)=z1*z3+z2*z3+z1*z4+z2*z4
proof
(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 thesis;
end;
theorem Th52:
-(z1+z2)=-z1-z2
proof
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 thesis by A1;
end;
theorem Th53:
-(z1-z2)=-z1+z2
proof
-(z1-z2)=(-1q)*(z1-z2) by QUATERN2:19
.=(-1q)*z1-(-1q)*z2 by QUATERN2:24
.=(-1q)*z1-(-z2) by QUATERN2:19;
hence thesis by QUATERN2:19;
end;
theorem Th54:
z-(z1+z2)=z-z1-z2
proof
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 thesis by A1,QUATERN2:2;
end;
theorem Th55:
z-(z1-z2)=z-z1+z2
proof
-(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 thesis by QUATERN2:19;
end;
theorem
(z1+z2)*(z3-z4)=z1*z3+z2*z3-z1*z4-z2*z4
proof
(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 thesis;
end;
theorem Th57:
(z1-z2)*(z3-z4)=z1*z3-z2*z3-z1*z4+z2*z4
proof
(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 thesis;
end;
theorem
-(z1+z2+z3)=-z1-z2-z3
proof
-(z1+z2+z3)=-(z1+(z2+z3)) by QUATERN2:2
.=-z1-(z2+z3) by Th52
.=-z1-z2-z3 by Th54;
hence thesis;
end;
theorem
-(z1-z2-z3)=-z1+z2+z3
proof
-(z1-z2-z3)=-(z1-z2)+z3 by Th53
.=-z1+z2+z3 by Th53;
hence thesis;
end;
theorem
-(z1-z2+z3)=-z1+z2-z3
proof
-(z1-z2+z3)=-(z1-z2)-z3 by Th52
.=-z1+z2-z3 by Th53;
hence thesis;
end;
theorem
-(z1+z2-z3)=-z1-z2+z3
proof
-(z1+z2-z3)=-(z1+z2)+z3 by Th53
.=-z1-z2+z3 by Th52;
hence thesis;
end;
theorem
z1+z=z2+z implies z1=z2
proof
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;
hence thesis by A1,A2,A4,A3,QUATERNI:25;
end;
theorem
z1-z=z2-z implies z1=z2
proof
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;
hence thesis by A1,A2,A4,A3,QUATERNI:25;
end;
theorem
(z1+z2-z3)*z4=z1*z4+z2*z4-z3*z4
proof
(z1+z2-z3)*z4=(z1+z2)*z4-z3*z4 by QUATERN2:23
.=z1*z4+z2*z4-z3*z4 by QUATERN2:18;
hence thesis;
end;
theorem
(z1-z2+z3)*z4=z1*z4-z2*z4+z3*z4
proof
(z1-z2+z3)*z4=(z1-z2)*z4+z3*z4 by QUATERN2:18
.=z1*z4-z2*z4+z3*z4 by QUATERN2:23;
hence thesis;
end;
theorem
(z1-z2-z3)*z4=z1*z4-z2*z4-z3*z4
proof
(z1-z2-z3)*z4=(z1-z2)*z4-z3*z4 by QUATERN2:23
.=z1*z4-z2*z4-z3*z4 by QUATERN2:23;
hence thesis;
end;
theorem
(z1+z2+z3)*z4=z1*z4+z2*z4+z3*z4
proof
(z1+z2+z3)*z4=(z1+z2)*z4+z3*z4 by QUATERN2:18
.=z1*z4+z2*z4+z3*z4 by QUATERN2:18;
hence thesis;
end;
theorem
(z1-z2)*z3=(z2-z1)*(-z3)
proof
(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 thesis by QUATERN2:23;
end;
theorem
z3*(z1-z2)=(-z3)*(z2-z1)
proof
(-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 thesis by QUATERN2:24;
end;
theorem Th70:
z1-z2-z3+z4 = z4-z3-z2+z1
proof
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 thesis by A1,A2,A7,A6,A4,A3,A5,QUATERNI:25;
end;
theorem
(z1-z2)*(z3-z4)=(z2-z1)*(z4-z3)
proof
(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 thesis by Th57;
end;
theorem
z-z1-z2=z-z2-z1
proof
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 thesis by A1,A2,A7,A6,A4,A3,A5,QUATERNI:25;
end;
theorem
z"=[*Rea z/|.z.|^2,-Im1 z/|.z.|^2, -Im2 z/|.z.|^2,-Im3 z/|.z.|^2*]
proof
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 thesis;
end;
theorem
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
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 thesis;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
Lm2: <i> = [*In(0,REAL),jj*] by ARYTM_0:def 5;
theorem
<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;
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,jj,0,0*] by QUATERN2:4
.=-<i> by Lm2,QUATERNI:def 6;
hence thesis;
end;
theorem
<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;
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,-jj,-0*] by A3,A2,A1,QUATERNI:24
.=-<j> by QUATERN2:4;
hence thesis;
end;
theorem
<k>"=-<k>
proof
A1: Im3 <k>"= - (Im3 <k>) / (|.<k>.|^2) by QUATERN2:29
.= -1 by QUATERNI:31;
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,-jj*] by A3,A2,A1,QUATERNI:24
.=-<k> by QUATERN2:4;
hence thesis;
end;
definition
let z be Quaternion;
func z^2 -> Number equals
z * z;
correctness;
end;
registration
let z be Quaternion;
cluster z^2 -> quaternion;
coherence;
end;
definition
let z be Element of QUATERNION;
redefine func z^2 -> Element of QUATERNION; :: redefines ^2 (QUATERN3, definition)
correctness;
end;
theorem Th78:
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
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 thesis;
end;
theorem
0q^2 = 0
proof
A1: 0q=[*In(0,REAL),In(0,REAL)*] 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
.=[*In(0,REAL),In(0,REAL)*] by A2,A3,QUATERNI:91
.=0 by ARYTM_0:def 5;
hence thesis;
end;
theorem
1q^2 = 1
proof
A1: 1q =[*jj,In(0,REAL)*] by ARYTM_0:def 5
.=[*jj,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
.=[*jj,In(0,REAL)*] by A2,A3,QUATERNI:91
.=1 by ARYTM_0:def 5;
hence thesis;
end;
theorem Th81:
z^2 = (-z)^2
proof
(-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 thesis by Th78;
end;
definition
let z be Quaternion;
func z^3 -> Number equals
z*z*z;
coherence;
end;
registration
let z be Quaternion;
cluster z^3 -> quaternion;
coherence;
end;
definition
let z be Element of QUATERNION;
redefine func z^3 -> Element of QUATERNION; :: redefines ^3 (QUATERN3, definition)
correctness;
end;
theorem
0q^3 = 0
proof
A1: 0q=[*In(0,REAL),In(0,REAL)*] 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
.=[*In(0,REAL),In(0,REAL)*] by A2,A3,QUATERNI:91
.=0 by ARYTM_0:def 5;
hence thesis;
end;
theorem
1q^3=1
proof
A1: 1q =[*jj,In(0,REAL)*] by ARYTM_0:def 5
.=[*jj,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
.=[*jj,In(0,REAL)*] by A2,A3,QUATERNI:91
.=1 by ARYTM_0:def 5;
hence thesis;
end;
theorem
<i>^3=-<i>
proof
<i> = [*0,jj,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*jj *] by QUATERNI:def 10
.=-[*0,jj,0,0*] by QUATERN2:4;
hence thesis by Lm2,QUATERNI:def 6;
end;
theorem
<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,jj,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,jj,0*] by QUATERN2:4;
hence thesis;
end;
theorem
<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,jj*] 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,jj*] by QUATERN2:4;
hence thesis;
end;
theorem
(-1q)^2=1
proof
1q =[*jj,In(0,REAL)*] by ARYTM_0:def 5
.=[*jj,0,0,0*] by QUATERNI:91;
then A1: -1q=[*-jj,-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
.=[*jj,In(0,REAL)*] by A2,A3,QUATERNI:91
.=1 by ARYTM_0:def 5;
hence thesis;
end;
theorem
(-1q)^3=-1
proof
A1: 1q =[*jj,In(0,REAL)*] by ARYTM_0:def 5
.=[*1,0,0,0*] by QUATERNI:91; then
A2: -1q=[*-jj,-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
.=[*jj,In(0,REAL)*] by A3,A4,QUATERNI:91
.=1 by ARYTM_0:def 5;
then (-1q)^3=-1q by QUATERN2:15
.=[*-jj,-0,-0,-0*] by A1,QUATERN2:4
.=[*-jj,-In(0,REAL)*] by QUATERNI:91
.=-1 by ARYTM_0:def 5;
hence thesis;
end;
theorem
z^3=-(-z)^3
proof
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 thesis;
end;