:: Some Operations on Quaternion Numbers :: by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang :: :: Received October 14, 2008 :: Copyright (c) 2008-2018 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, BOOLE, 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 *+Im2 z3 *+Im3 z3 *; 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*=[*0,Rea z,0,0*]; theorem :: QUATERN3:6 z is Real implies z*=[*0,0,Rea z,0*]; theorem :: QUATERN3:7 z is Real implies z*=[*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 *z1-z1* = [*0,0,-2*Im3 z1,2*Im2 z1*]; theorem :: QUATERN3:19 *z1+z1* = [*-2*Im1 z1,2*Rea z1,0,0*]; theorem :: QUATERN3:20 *z1-z1* = [*0,2*Im3 z1,0,-2*Im1 z1*]; theorem :: QUATERN3:21 *z1+z1* = [*-2*Im2 z1,0,2*Rea z1,0*]; theorem :: QUATERN3:22 *z1-z1* = [*0,-2*Im2 z1,2*Im1 z1,0*]; theorem :: QUATERN3:23 *z1+z1* = [*-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 "=-; theorem :: QUATERN3:76 "=-; theorem :: QUATERN3:77 "=-; 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 ^3=-; theorem :: QUATERN3:85 ^3=-; theorem :: QUATERN3:86 ^3=-; theorem :: QUATERN3:87 (-1q)^2=1; theorem :: QUATERN3:88 (-1q)^3=-1; theorem :: QUATERN3:89 z^3=-(-z)^3;