:: Some Operations on Quaternion Numbers :: by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang :: :: Received October 14, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin theorem Th1: :: QUATERN3:1 for z1, z2 being quaternion number holds Rea (z1 * z2) = Rea (z2 * z1) proofend; Lm1: for z being quaternion number st z is Real holds ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) proofend; theorem :: QUATERN3:2 for z, z3 being quaternion number st z is Real holds z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * )) + ((Im2 z3) * )) + ((Im3 z3) * ) proofend; 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))*] proofend; 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))*] proofend; theorem :: QUATERN3:5 for z being quaternion number st z is Real holds z * = [*0,(Rea z),0,0*] proofend; theorem :: QUATERN3:6 for z being quaternion number st z is Real holds z * = [*0,0,(Rea z),0*] proofend; theorem :: QUATERN3:7 for z being quaternion number st z is Real holds z * = [*0,0,0,(Rea z)*] proofend; theorem :: QUATERN3:8 for z being quaternion number holds z - 0q = z proofend; theorem :: QUATERN3:9 for z, z1 being quaternion number st z is Real holds z * z1 = z1 * z proofend; theorem :: QUATERN3:10 for z being quaternion number st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds z = Rea z proofend; theorem Th11: :: QUATERN3:11 for z being quaternion number holds |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) proofend; theorem :: QUATERN3:12 for z being quaternion number holds |.z.| ^2 = |.(z * (z *')).| proofend; theorem :: QUATERN3:13 for z being quaternion number holds |.z.| ^2 = Rea (z * (z *')) proofend; theorem :: QUATERN3:14 for z being quaternion number holds 2 * (Rea z) = Rea (z + (z *')) proofend; theorem :: QUATERN3:15 for z, z1 being quaternion number st z is Real holds (z * z1) *' = (z *') * (z1 *') proofend; theorem :: QUATERN3:16 for z1, z2 being quaternion number holds (z1 * z2) *' = (z2 *') * (z1 *') proofend; theorem Th17: :: QUATERN3:17 for z1, z2 being quaternion number holds |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2) proofend; theorem :: QUATERN3:18 for z1 being quaternion number holds ( * z1) - (z1 * ) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*] proofend; theorem :: QUATERN3:19 for z1 being quaternion number holds ( * z1) + (z1 * ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*] proofend; theorem :: QUATERN3:20 for z1 being quaternion number holds ( * z1) - (z1 * ) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] proofend; theorem :: QUATERN3:21 for z1 being quaternion number holds ( * z1) + (z1 * ) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*] proofend; theorem :: QUATERN3:22 for z1 being quaternion number holds ( * z1) - (z1 * ) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] proofend; theorem :: QUATERN3:23 for z1 being quaternion number holds ( * z1) + (z1 * ) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*] proofend; theorem Th24: :: QUATERN3:24 for z being quaternion number holds Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z) proofend; theorem Th25: :: QUATERN3:25 for z being quaternion number holds Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z)) proofend; theorem Th26: :: QUATERN3:26 for z being quaternion number holds Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z)) proofend; theorem Th27: :: QUATERN3:27 for z being quaternion number holds Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z)) proofend; 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)))*] proofend; theorem :: QUATERN3:29 for z being quaternion number holds z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] proofend; theorem :: QUATERN3:30 for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) proofend; theorem :: QUATERN3:31 for z1, z2, z3 being quaternion number holds Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2) proofend; theorem Th32: :: QUATERN3:32 for z being quaternion number holds |.(z * z).| = |.((z *') * (z *')).| proofend; theorem :: QUATERN3:33 for z being quaternion number holds |.((z *') * (z *')).| = |.z.| ^2 proofend; theorem :: QUATERN3:34 for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.| proofend; theorem :: QUATERN3:35 for z1, z2, z3 being quaternion number holds |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.| proofend; theorem :: QUATERN3:36 for z1, z2, z3 being quaternion number holds |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| proofend; theorem :: QUATERN3:37 for z1, z2, z3 being quaternion number holds |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| proofend; theorem :: QUATERN3:38 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 proofend; theorem :: QUATERN3:39 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 proofend; theorem :: QUATERN3:40 for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| proofend; theorem :: QUATERN3:41 for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.| proofend; theorem :: QUATERN3:42 for z1, z2, z being quaternion number holds |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| proofend; theorem :: QUATERN3:43 for z1, z2 being quaternion number st |.z1.| - |.z2.| <> 0 holds ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 proofend; theorem :: QUATERN3:44 for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 proofend; theorem :: QUATERN3:45 for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 proofend; theorem :: QUATERN3:46 for z1, z2 being quaternion number holds (z1 * z2) " = (z2 ") * (z1 ") proofend; theorem :: QUATERN3:47 for z being quaternion number holds (z *') " = (z ") *' proofend; theorem :: QUATERN3:48 1q " = 1q proofend; theorem :: QUATERN3:49 for z1, z2 being quaternion number st |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " holds z1 = z2 proofend; theorem :: QUATERN3:50 for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) proofend; theorem :: QUATERN3:51 for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) proofend; theorem Th52: :: QUATERN3:52 for z1, z2 being quaternion number holds - (z1 + z2) = (- z1) - z2 proofend; theorem Th53: :: QUATERN3:53 for z1, z2 being quaternion number holds - (z1 - z2) = (- z1) + z2 proofend; theorem Th54: :: QUATERN3:54 for z, z1, z2 being quaternion number holds z - (z1 + z2) = (z - z1) - z2 proofend; theorem Th55: :: QUATERN3:55 for z, z1, z2 being quaternion number holds z - (z1 - z2) = (z - z1) + z2 proofend; theorem :: QUATERN3:56 for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) proofend; 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) proofend; theorem :: QUATERN3:58 for z1, z2, z3 being quaternion number holds - ((z1 + z2) + z3) = ((- z1) - z2) - z3 proofend; theorem :: QUATERN3:59 for z1, z2, z3 being quaternion number holds - ((z1 - z2) - z3) = ((- z1) + z2) + z3 proofend; theorem :: QUATERN3:60 for z1, z2, z3 being quaternion number holds - ((z1 - z2) + z3) = ((- z1) + z2) - z3 proofend; theorem :: QUATERN3:61 for z1, z2, z3 being quaternion number holds - ((z1 + z2) - z3) = ((- z1) - z2) + z3 proofend; theorem :: QUATERN3:62 for z1, z, z2 being quaternion number st z1 + z = z2 + z holds z1 = z2 proofend; theorem :: QUATERN3:63 for z1, z, z2 being quaternion number st z1 - z = z2 - z holds z1 = z2 proofend; theorem :: QUATERN3:64 for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4) proofend; theorem :: QUATERN3:65 for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4) proofend; theorem :: QUATERN3:66 for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4) proofend; theorem :: QUATERN3:67 for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4) proofend; theorem :: QUATERN3:68 for z1, z2, z3 being quaternion number holds (z1 - z2) * z3 = (z2 - z1) * (- z3) proofend; theorem :: QUATERN3:69 for z3, z1, z2 being quaternion number holds z3 * (z1 - z2) = (- z3) * (z2 - z1) proofend; theorem Th70: :: QUATERN3:70 for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1 proofend; theorem :: QUATERN3:71 for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3) proofend; theorem :: QUATERN3:72 for z, z1, z2 being quaternion number holds (z - z1) - z2 = (z - z2) - z1 proofend; 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)))*] proofend; 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))*] proofend; Lm2: = [*0,1*] by ARYTM_0:def_5; theorem :: QUATERN3:75 " = - proofend; theorem :: QUATERN3:76 " = - proofend; theorem :: QUATERN3:77 " = - proofend; 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)))*] proofend; theorem :: QUATERN3:79 0q ^2 = 0 proofend; theorem :: QUATERN3:80 1q ^2 = 1 proofend; theorem Th81: :: QUATERN3:81 for z being quaternion number holds z ^2 = (- z) ^2 proofend; 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 proofend; theorem :: QUATERN3:83 1q ^3 = 1 proofend; theorem :: QUATERN3:84 ^3 = - proofend; theorem :: QUATERN3:85 ^3 = - proofend; theorem :: QUATERN3:86 ^3 = - proofend; theorem :: QUATERN3:87 (- 1q) ^2 = 1 proofend; theorem :: QUATERN3:88 (- 1q) ^3 = - 1 proofend; theorem :: QUATERN3:89 for z being quaternion number holds z ^3 = - ((- z) ^3) proofend;