:: The Quaternion Numbers :: by Xiquan Liang and Fuguo Ge :: :: Received November 14, 2006 :: Copyright (c) 2006-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, XBOOLE_0, FUNCT_2, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1, FUNCOP_1, RELAT_1, TARSKI, ZFMISC_1, XCMPLX_0, ARYTM_0, XREAL_0, ARYTM_3, ARYTM_2, ARYTM_1, COMPLEX1, REAL_1, SQUARE_1, XXREAL_0, QUATERNI, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ARYTM_3, NUMBERS, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, COMPLEX1, ARYTM_0, ZFMISC_1, ARYTM_2, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, XXREAL_0, RELSET_1; constructors ENUMSET1, FUNCT_4, ARYTM_1, ARYTM_0, REAL_1, SQUARE_1, COMPLEX1, VALUED_1, RELSET_1; registrations XBOOLE_0, ORDINAL1, FUNCT_4, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, VALUED_0, RELSET_1, FUNCT_7; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin reserve a,b,c,d,x,y,w,z,x1,x2,x3,x4 , X for set; reserve A for non empty set; definition func QUATERNION -> set equals :: QUATERNI:def 1 Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL): x.2 = 0 & x.3 = 0} \/ COMPLEX; end; definition let x be Number; attr x is quaternion means :: QUATERNI:def 2 x in QUATERNION; end; registration cluster QUATERNION -> non empty; end; registration cluster quaternion for Number; end; definition mode Quaternion is quaternion Number; end; ::$CD ::$CT 4 theorem :: QUATERNI:5 {x1,x2,x3,x4} c= X iff x1 in X & x2 in X & x3 in X & x4 in X; definition let A,x,y,w,z; let a,b,c,d be Element of A; redefine func (x,y,w,z) --> (a,b,c,d) -> Function of {x,y,w,z},A; end; definition func -> Number equals :: QUATERNI:def 4 (0,1,2,3) --> (0,0,1,0); func -> Number equals :: QUATERNI:def 5 (0,1,2,3) --> (0,0,0,1); end; registration cluster -> quaternion; cluster -> quaternion; cluster -> quaternion; end; registration cluster -> quaternion for Element of QUATERNION; end; definition let x,y,w,z be Real; func [*x,y,w,z*] -> Element of QUATERNION means :: QUATERNI:def 6 ex x9, y9 being Element of REAL st x9 = x & y9 = y & it = [*x9,y9*] if w=0 & z=0 otherwise it = (0,1,2,3) --> (x,y,w,z); end; ::$CT theorem :: QUATERNI:7 for g being Quaternion ex r,s,t,u being Real st g = [*r,s,t,u*]; reserve i,j,k for Element of NAT; reserve a,b,c,d for Real; reserve y,r,s,x,t,w for Element of RAT+; ::$CT theorem :: QUATERNI:9 for A being Subset of RAT+ st (ex t st t in A & t <> {}) & for r,s st r in A & s <=' r holds s in A ex r1,r2,r3,r4,r5 being Element of RAT+ st r1 in A & r2 in A & r3 in A & r4 in A & r5 in A & r1 <> r2 & r1 <> r3 & r1<>r4 & r1 <> r5 & r2<> r3 & r2<> r4 & r2<> r5& r3 <> r4 & r3 <> r5 & r4 <> r5; theorem :: QUATERNI:10 not (0,1,2,3) --> (a,b,c,d) in COMPLEX; ::$CT theorem :: QUATERNI:12 for x1,x2,x3,x4,y1,y2,y3,y4 being Real st [*x1,x2,x3,x4*] = [*y1,y2,y3,y4*] holds x1 = y1 & x2 = y2 & x3=y3 & x4=y4; definition let x,y be Quaternion; func x + y -> Number means :: QUATERNI:def 7 ex x1,x2,x3,x4,y1,y2,y3,y4 being Real st x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [*x1+y1,x2+y2,x3+y3,x4+y4*]; commutativity; end; definition let z be Quaternion; func - z -> Quaternion means :: QUATERNI:def 8 z + it = 0; involutiveness; end; definition let x,y be Quaternion; func x-y -> Number equals :: QUATERNI:def 9 x + - y; end; definition let x,y be Quaternion; func x*y -> Number means :: QUATERNI:def 10 ex x1,x2,x3,x4,y1,y2,y3,y4 being Real st x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3, x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *]; end; registration let z,z9 be Quaternion; cluster z + z9 -> quaternion; cluster z*z9 -> quaternion; end; definition redefine func -> Element of QUATERNION equals :: QUATERNI:def 11 [*0,0,1,0*]; redefine func -> Element of QUATERNION equals :: QUATERNI:def 12 [*0,0,0,1*]; end; theorem :: QUATERNI:13 * = -1; theorem :: QUATERNI:14 * = -1; theorem :: QUATERNI:15 * = -1; theorem :: QUATERNI:16 * = ; theorem :: QUATERNI:17 * = ; theorem :: QUATERNI:18 * = ; theorem :: QUATERNI:19 * = - * ; theorem :: QUATERNI:20 * = - * ; theorem :: QUATERNI:21 * = - * ; definition let z be Quaternion; func Rea z -> Number means :: QUATERNI:def 13 ex z9 being Complex st z=z9 & it = Re z9 if z in COMPLEX otherwise ex f being Function of 4,REAL st z = f & it = f.0; func Im1 z -> Number means :: QUATERNI:def 14 ex z9 being Complex st z=z9 & it = Im z9 if z in COMPLEX otherwise ex f being Function of 4,REAL st z = f & it = f.1; func Im2 z -> Number means :: QUATERNI:def 15 it = 0 if z in COMPLEX otherwise ex f being Function of 4,REAL st z = f & it = f.2; func Im3 z -> Number means :: QUATERNI:def 16 it = 0 if z in COMPLEX otherwise ex f being Function of 4,REAL st z = f & it = f.3; end; registration let z be Quaternion; cluster Rea z -> real; cluster Im1 z -> real; cluster Im2 z -> real; cluster Im3 z -> real; end; theorem :: QUATERNI:22 for f being Function of 4,REAL ex a,b,c,d st f = (0,1,2,3)-->(a,b,c,d); theorem :: QUATERNI:23 Rea [*a,b,c,d*] = a & Im1 [*a,b,c,d*] = b & Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d; reserve z,z1,z2,z3,z4 for Quaternion; theorem :: QUATERNI:24 z = [*Rea z, Im1 z, Im2 z, Im3 z*]; theorem :: QUATERNI:25 Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 & Im3 z1 = Im3 z2 implies z1 = z2; definition func 0q -> Quaternion equals :: QUATERNI:def 17 0; func 1q -> Quaternion equals :: QUATERNI:def 18 1; end; theorem :: QUATERNI:26 Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q; theorem :: QUATERNI:27 z = 0 implies (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0; theorem :: QUATERNI:28 (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0 implies z = 0q; theorem :: QUATERNI:29 Rea (1q) = 1 & Im1(1q) = 0 & Im2 (1q) = 0 & Im3 (1q) = 0; theorem :: QUATERNI:30 Rea = 0 & Im1 = 1 & Im2 = 0 & Im3 = 0; theorem :: QUATERNI:31 Rea = 0 & Im1 = 0 & Im2 = 1 & Im3 = 0 & Rea = 0 & Im1 = 0 & Im2 = 0 & Im3 = 1; theorem :: QUATERNI:32 Rea (z1 + z2 + z3 + z4) = Rea z1 + Rea z2 + Rea z3 + Rea z4 & Im1 (z1 + z2 + z3 + z4) = Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4 & Im2 (z1 + z2 + z3 + z4) = Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4 & Im3 (z1 + z2 + z3 + z4) = Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4; reserve x for Real; theorem :: QUATERNI:33 z1 = x implies Rea (z1*) = 0 & Im1 (z1*) = x & Im2 (z1*) = 0 & Im3 (z1*) = 0; theorem :: QUATERNI:34 z1 = x implies Rea (z1*) = 0 & Im1 (z1*) = 0 & Im2 (z1*) = x & Im3 (z1*) = 0; theorem :: QUATERNI:35 z1 = x implies Rea (z1*) = 0 & Im1 (z1*) = 0 & Im2 (z1*) = 0 & Im3 (z1*) = x; definition let x be Real, y be Quaternion; func x + y -> Number means :: QUATERNI:def 19 ex y1,y2,y3,y4 being Real st y = [*y1,y2,y3,y4*] & it = [*x+y1,y2,y3,y4*]; end; definition let x be Real, y be Quaternion; func x - y -> Number equals :: QUATERNI:def 20 x + -y; end; definition let x be Real, y be Quaternion; func x * y -> Number means :: QUATERNI:def 21 ex y1,y2,y3,y4 being Real st y = [*y1,y2,y3,y4*] & it = [*x*y1,x*y2,x*y3,x*y4*]; end; registration let x be Real,z9 be Quaternion; cluster x+z9 -> quaternion; cluster x*z9 -> quaternion; cluster x-z9 -> quaternion; end; definition let z1,z2 be Quaternion; redefine func z1 + z2 -> Element of QUATERNION; end; theorem :: QUATERNI:36 Rea (z1 + z2) = Rea z1 + Rea z2 & Im1(z1 + z2) = Im1 z1 + Im1 z2 & Im2 (z1 + z2) = Im2 z1 + Im2 z2 & Im3(z1 + z2) = Im3 z1 + Im3 z2; definition let z1,z2 be Quaternion; redefine func z1 * z2 -> Element of QUATERNION; end; theorem :: QUATERNI:37 z = Rea z+(Im1 z)* + (Im2 z)* + (Im3 z)*; theorem :: QUATERNI:38 Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 implies Rea(z1*z2) = Rea z1 * Rea z2 & Im1(z1*z2) = Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 & Im2(z1*z2) = Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 & Im3(z1*z2) = Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2; theorem :: QUATERNI:39 Rea z1 = 0 & Rea z2 = 0 implies Rea(z1*z2) = - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 & Im1(z1*z2) = Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 & Im2(z1*z2) = Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 & Im3(z1*z2) = Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2; theorem :: QUATERNI:40 Rea(z*z) = (Rea z)^2 - (Im1 z)^2 - (Im2 z)^2 - (Im3 z)^2 & Im1(z*z) = 2*(Rea z * Im1 z) & Im2(z*z) = 2*( Rea z * Im2 z) & Im3(z*z) = 2*(Rea z * Im3 z); definition let z be Quaternion; redefine func -z -> Element of QUATERNION; end; theorem :: QUATERNI:41 Rea(-z) = -(Rea z) & Im1(-z) = -(Im1 z) & Im2(-z) = -(Im2 z) & Im3(-z) = -(Im3 z); definition let z1,z2 be Quaternion; redefine func z1 - z2 -> Element of QUATERNION; end; theorem :: QUATERNI:42 Rea(z1 - z2) = Rea z1 - Rea z2 & Im1(z1 - z2) = Im1 z1 - Im1 z2 & Im2(z1 - z2) = Im2 z1 - Im2 z2 & Im3(z1 - z2) = Im3 z1 - Im3 z2; definition let z be Quaternion; func z*' -> Quaternion equals :: QUATERNI:def 22 Rea z + (-Im1 z)* + (-Im2 z)* + (-Im3 z)*; end; definition let z be Quaternion; redefine func z*' -> Element of QUATERNION; end; theorem :: QUATERNI:43 z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*]; theorem :: QUATERNI:44 Rea (z*') = Rea z & Im1 (z*') = -Im1 z & Im2 (z*') = -Im2 z & Im3 (z*') = -Im3 z; theorem :: QUATERNI:45 z = 0 implies z*' = 0; theorem :: QUATERNI:46 z*' = 0 implies z = 0; theorem :: QUATERNI:47 1q*' = 1q; theorem :: QUATERNI:48 Rea (*') = 0 & Im1 (*') = -1 & Im2 (*') = 0 & Im3 (*') = 0; theorem :: QUATERNI:49 Rea (*') = 0 & Im1 (*') = 0 & Im2 (*') = -1 & Im3 (*') = 0; theorem :: QUATERNI:50 Rea (*') = 0 & Im1 (*') = 0 & Im2 (*') = 0 & Im3 (*') = -1; theorem :: QUATERNI:51 *' = -; theorem :: QUATERNI:52 *' = -; theorem :: QUATERNI:53 *' = -; theorem :: QUATERNI:54 (z1 + z2)*' = z1*' + z2*'; theorem :: QUATERNI:55 (-z)*' = -(z*'); theorem :: QUATERNI:56 (z1 - z2)*' = z1*' - z2*'; theorem :: QUATERNI:57 (z1*z2)*' = z1*' * z2*' implies (Im2 z1 * Im3 z2) = (Im3 z1)*(Im2 z2); theorem :: QUATERNI:58 Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z*' = z; theorem :: QUATERNI:59 Rea z = 0 implies z*' = -z; theorem :: QUATERNI:60 Rea(z*z*') = (Rea z)^2+(Im1 z)^2+(Im2 z)^2+(Im3 z)^2 & Im1(z*z*') = 0 & Im2(z*z*') = 0 & Im3(z*z*') = 0; theorem :: QUATERNI:61 Rea(z + z*') = 2*Rea z & Im1(z + z*') = 0 & Im2(z + z*') = 0 & Im3(z + z*') = 0; theorem :: QUATERNI:62 -z = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*]; theorem :: QUATERNI:63 z1 - z2 = [*Rea z1 - Rea z2, Im1 z1 - Im1 z2, Im2 z1 - Im2 z2, Im3 z1 - Im3 z2*]; theorem :: QUATERNI:64 Rea(z - z*') = 0 & Im1(z - z*') = 2*Im1 z & Im2(z - z*') = 2*Im2 z & Im3(z - z*') = 2*Im3 z; definition let z; func |.z.| -> Real equals :: QUATERNI:def 23 sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2); end; theorem :: QUATERNI:65 |.0q.| = 0; theorem :: QUATERNI:66 |.z.| = 0 implies z = 0; theorem :: QUATERNI:67 0 <= |.z.|; theorem :: QUATERNI:68 |.1q.| = 1; theorem :: QUATERNI:69 |..| = 1; theorem :: QUATERNI:70 |..| = 1; theorem :: QUATERNI:71 |..| = 1; theorem :: QUATERNI:72 |.-z.| = |.z.|; theorem :: QUATERNI:73 |.z*'.| = |.z.|; theorem :: QUATERNI:74 for a,b,c,d being Real holds a^2 + b^2 + c^2 + d^2 >= 0; theorem :: QUATERNI:75 Rea z <= |.z.|; theorem :: QUATERNI:76 Im1 z <= |.z.|; theorem :: QUATERNI:77 Im2 z <= |.z.|; theorem :: QUATERNI:78 Im3 z <= |.z.|; theorem :: QUATERNI:79 |.z1 + z2.| <= |.z1.| + |.z2.|; theorem :: QUATERNI:80 |.z1 - z2.| <= |.z1.| + |.z2.|; theorem :: QUATERNI:81 |.z1.| - |.z2.| <= |.z1 + z2.|; theorem :: QUATERNI:82 |.z1.| - |.z2.| <= |.z1 - z2.|; theorem :: QUATERNI:83 |.z1 - z2.| = |.z2 - z1.|; theorem :: QUATERNI:84 |.z1 - z2.| = 0 iff z1 = z2; theorem :: QUATERNI:85 |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|; theorem :: QUATERNI:86 |.|.z1.| - |.z2.|.| <= |.z1 - z2.|; theorem :: QUATERNI:87 |.z1*z2.| = |.z1.|*|.z2.|; theorem :: QUATERNI:88 |.z*z.| = (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2; theorem :: QUATERNI:89 |.z*z.| = |.z*z*'.|; theorem :: QUATERNI:90 z is real implies Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0; theorem :: QUATERNI:91 for x,y being Element of REAL holds [*x,y,0,0*] = [*x,y*]; theorem :: QUATERNI:92 z1+z2 = Rea z1 + Rea z2 + (Im1 z1 + Im1 z2)* + (Im2 z1 + Im2 z2)* + (Im3 z1 + Im3 z2)*; theorem :: QUATERNI:93 z1*z2 = (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)* + (Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2)* + (Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*; theorem :: QUATERNI:94 -z = -Rea z + (-Im1 z)* + (-Im2 z)* + (-Im3 z)*; theorem :: QUATERNI:95 z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)* + (Im2 z1 - Im2 z2)* + (Im3 z1 - Im3 z2)*; theorem :: QUATERNI:96 for a, b, c, d being Real st a^2 + b^2 + c^2 + d^2 = 0 holds a = 0 & b = 0 & c = 0 & d = 0; theorem :: QUATERNI:97 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 & 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;