:: Some Operations on Quaternion Numbers
::  by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2021 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;


begin

reserve z1,z2,z3,z4,z for Quaternion;

theorem :: QUATERN3:1
  Rea (z1*z2) = Rea (z2*z1);

theorem :: QUATERN3:2
  z is Real implies z+z3 = Rea z + Rea z3+Im1 z3 *<i>+Im2 z3 *<j>+Im3 z3 *<k>;

theorem :: QUATERN3:3
  z is Real implies z-z3 = [* Rea z -Rea z3,-Im1 z3,-Im2 z3,-Im3 z3*];

theorem :: QUATERN3:4
  z is Real implies z*z3 = [* Rea z*Rea z3,Rea z*Im1 z3,Rea z*Im2 z3,Rea
  z*Im3 z3*];

theorem :: QUATERN3:5
  z is Real implies z*<i>=[*0,Rea z,0,0*];

theorem :: QUATERN3:6
  z is Real implies z*<j>=[*0,0,Rea z,0*];

theorem :: QUATERN3:7
  z is Real implies z*<k>=[*0,0,0,Rea z*];

theorem :: QUATERN3:8
  z - 0q = z;

theorem :: QUATERN3:9
  z is Real implies z*z1 = z1*z;

theorem :: QUATERN3:10
  Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = Rea z;

theorem :: QUATERN3:11
  |.z.| ^2 = (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2;

theorem :: QUATERN3:12
  |.z.| ^2 = |.z*z*'.|;

theorem :: QUATERN3:13
  |.z.| ^2 = Rea (z * z*');

theorem :: QUATERN3:14
  2 * Rea z = Rea (z+ z*');

theorem :: QUATERN3:15
  z is Real implies (z * z1)*' = z*' * z1*';

theorem :: QUATERN3:16
  (z1*z2)*' = z2*' * z1*';

theorem :: QUATERN3:17
  |.z1*z2.|^2 = |.z1.| ^2 * |.z2.| ^2;

theorem :: QUATERN3:18
  <i>*z1-z1*<i> = [*0,0,-2*Im3 z1,2*Im2 z1*];

theorem :: QUATERN3:19
  <i>*z1+z1*<i> = [*-2*Im1 z1,2*Rea z1,0,0*];

theorem :: QUATERN3:20
  <j>*z1-z1*<j> = [*0,2*Im3 z1,0,-2*Im1 z1*];

theorem :: QUATERN3:21
  <j>*z1+z1*<j> = [*-2*Im2 z1,0,2*Rea z1,0*];

theorem :: QUATERN3:22
  <k>*z1-z1*<k> = [*0,-2*Im2 z1,2*Im1 z1,0*];

theorem :: QUATERN3:23
  <k>*z1+z1*<k> = [*-2*Im3 z1,0,0,2*Rea z1*];

theorem :: QUATERN3:24
  Rea (1/(|.z.| ^2) * z*') = 1/(|.z.| ^2)*Rea z;

theorem :: QUATERN3:25
  Im1 (1/(|.z.| ^2) * z*') = -1/(|.z.| ^2)*Im1 z;

theorem :: QUATERN3:26
  Im2 (1/(|.z.| ^2) * z*') = -1/(|.z.|^2)*Im2 z;

theorem :: QUATERN3:27
  Im3 (1/(|.z.| ^2) * z*') = -1/(|.z.|^2)*Im3 z;

theorem :: QUATERN3:28
  (1/(|.z.| ^2) * z*')=[*1/(|.z.|^2)*Rea z, -1/(|.z.|^2)*Im1 z, -1/(|.z
  .|^2)*Im2 z, -1/(|.z.|^2)*Im3 z*];

theorem :: QUATERN3:29
  z * (1/(|.z.| ^2) * z*') = [* (|.z.| ^2)/(|.z.| ^2),0,0,0*];

theorem :: QUATERN3:30
  |.z1*z2*z3.| ^2 = |.z1.| ^2 * |.z2.| ^2 * |.z3.| ^2;

theorem :: QUATERN3:31
  Rea(z1*z2*z3) = Rea (z3*z1*z2);

theorem :: QUATERN3:32
  |.z*z.| = |.z*'* z*'.|;

theorem :: QUATERN3:33
  |.z*'* z*'.| = |.z.| ^2;

theorem :: QUATERN3:34
  |.z1*z2*z3.| = |.z1.|*|.z2.|*|.z3.|;

theorem :: QUATERN3:35
  |.z1+z2+z3.| <= |.z1.| + |.z2.|+|.z3.|;

theorem :: QUATERN3:36
  |.z1+z2-z3.| <= |.z1.| + |.z2.| + |.z3.|;

theorem :: QUATERN3:37
  |.z1-z2-z3.| <= |.z1.| + |.z2.| + |.z3.|;

theorem :: QUATERN3:38
  |.z1.| - |.z2.| <= (|.z1 + z2.|+|.z1-z2.|)/2;

theorem :: QUATERN3:39
  |.z1.| - |.z2.| <= (|.z1 + z2.|+|.z2-z1.|)/2;

theorem :: QUATERN3:40
  |.|.z1.| - |.z2.|.| <= |.z2 - z1.|;

theorem :: QUATERN3:41
  |.|.z1.| - |.z2.|.| <= |.z1.| + |.z2.|;

theorem :: QUATERN3:42
  |.z1.| - |.z2.| <= |.z1 - z.| + |.z - z2.|;

theorem :: QUATERN3:43
  |.z1.|-|.z2.|<>0 implies |.z1.|^2+|.z2.|^2 -2*|.z1.|*|.z2.| >0;

theorem :: QUATERN3:44
  |.z1.| + |.z2.| >= (|.z1 + z2.|+|.z2 - z1.|)/2;

theorem :: QUATERN3:45
  |.z1.| + |.z2.| >= (|.z1 + z2.|+|.z1 - z2.|)/2;

theorem :: QUATERN3:46
  (z1*z2)" = z2" * z1";

theorem :: QUATERN3:47
  (z*')" = (z")*';

theorem :: QUATERN3:48
  1q" = 1q;

theorem :: QUATERN3:49
  |.z1.|=|.z2.| & |.z1.| <>0 & z1"=z2" implies z1=z2;

theorem :: QUATERN3:50
  (z1-z2)*(z3+z4)=z1*z3-z2*z3+z1*z4-z2*z4;

theorem :: QUATERN3:51
  (z1+z2)*(z3+z4)=z1*z3+z2*z3+z1*z4+z2*z4;

theorem :: QUATERN3:52
  -(z1+z2)=-z1-z2;

theorem :: QUATERN3:53
  -(z1-z2)=-z1+z2;

theorem :: QUATERN3:54
  z-(z1+z2)=z-z1-z2;

theorem :: QUATERN3:55
  z-(z1-z2)=z-z1+z2;

theorem :: QUATERN3:56
  (z1+z2)*(z3-z4)=z1*z3+z2*z3-z1*z4-z2*z4;

theorem :: QUATERN3:57
  (z1-z2)*(z3-z4)=z1*z3-z2*z3-z1*z4+z2*z4;

theorem :: QUATERN3:58
  -(z1+z2+z3)=-z1-z2-z3;

theorem :: QUATERN3:59
  -(z1-z2-z3)=-z1+z2+z3;

theorem :: QUATERN3:60
  -(z1-z2+z3)=-z1+z2-z3;

theorem :: QUATERN3:61
  -(z1+z2-z3)=-z1-z2+z3;

theorem :: QUATERN3:62
  z1+z=z2+z implies z1=z2;

theorem :: QUATERN3:63
  z1-z=z2-z implies z1=z2;

theorem :: QUATERN3:64
  (z1+z2-z3)*z4=z1*z4+z2*z4-z3*z4;

theorem :: QUATERN3:65
  (z1-z2+z3)*z4=z1*z4-z2*z4+z3*z4;

theorem :: QUATERN3:66
  (z1-z2-z3)*z4=z1*z4-z2*z4-z3*z4;

theorem :: QUATERN3:67
  (z1+z2+z3)*z4=z1*z4+z2*z4+z3*z4;

theorem :: QUATERN3:68
  (z1-z2)*z3=(z2-z1)*(-z3);

theorem :: QUATERN3:69
  z3*(z1-z2)=(-z3)*(z2-z1);

theorem :: QUATERN3:70
  z1-z2-z3+z4 = z4-z3-z2+z1;

theorem :: QUATERN3:71
  (z1-z2)*(z3-z4)=(z2-z1)*(z4-z3);

theorem :: QUATERN3:72
  z-z1-z2=z-z2-z1;

theorem :: QUATERN3:73
  z"=[*Rea z/|.z.|^2,-Im1 z/|.z.|^2, -Im2 z/|.z.|^2,-Im3 z/|.z.|^2*];

theorem :: QUATERN3:74
  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)*];

theorem :: QUATERN3:75
  <i>"=-<i>;

theorem :: QUATERN3:76
  <j>"=-<j>;

theorem :: QUATERN3:77
  <k>"=-<k>;

definition
  let z be Quaternion;
  func z^2 -> Number equals
:: QUATERN3:def 1
  z * z;
end;

registration
  let z be Quaternion;
  cluster z^2 -> quaternion;
end;

definition
  let z be Element of QUATERNION;
  redefine func z^2 -> Element of QUATERNION;
end;

theorem :: QUATERN3:78
  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)*];

theorem :: QUATERN3:79
  0q^2 = 0;

theorem :: QUATERN3:80
  1q^2 = 1;

theorem :: QUATERN3:81
  z^2 = (-z)^2;

definition
  let z be Quaternion;
  func z^3 -> Number equals
:: QUATERN3:def 2
  z*z*z;
end;

registration
  let z be Quaternion;
  cluster z^3 -> quaternion;
end;

definition
  let z be Element of QUATERNION;
  redefine func z^3 -> Element of QUATERNION;
end;

theorem :: QUATERN3:82
  0q^3 = 0;

theorem :: QUATERN3:83
  1q^3=1;

theorem :: QUATERN3:84
  <i>^3=-<i>;

theorem :: QUATERN3:85
  <j>^3=-<j>;

theorem :: QUATERN3:86
  <k>^3=-<k>;

theorem :: QUATERN3:87
  (-1q)^2=1;

theorem :: QUATERN3:88
  (-1q)^3=-1;

theorem :: QUATERN3:89
  z^3=-(-z)^3;