:: Some Operations on Quaternion Numbers
:: by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang
::
:: Received October 14, 2008
:: Copyright (c) 2008 Association of Mizar Users

begin

Lm1: for x, y, z being quaternion number st z = x * y holds
( Rea z = ((((Rea x) * (Rea y)) - ((Im1 x) * (Im1 y))) - ((Im2 x) * (Im2 y))) - ((Im3 x) * (Im3 y)) & Im1 z = ((((Rea x) * (Im1 y)) + ((Im1 x) * (Rea y))) + ((Im2 x) * (Im3 y))) - ((Im3 x) * (Im2 y)) & Im2 z = ((((Rea x) * (Im2 y)) + ((Im2 x) * (Rea y))) + ((Im3 x) * (Im1 y))) - ((Im1 x) * (Im3 y)) & Im3 z = ((((Rea x) * (Im3 y)) + ((Im3 x) * (Rea y))) + ((Im1 x) * (Im2 y))) - ((Im2 x) * (Im1 y)) )

proof end;

theorem Th1: :: QUATERN3:1

for z1, z2 being quaternion number holds Rea (z1 * z2) = Rea (z2 * z1)

proof end;

Lm2: for z being quaternion number st z is Real holds
( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )

proof end;

theorem :: QUATERN3:2

for z, z3 being quaternion number st z is Real holds
z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i> )) + ((Im2 z3) * <j> )) + ((Im3 z3) * <k> )

proof end;

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))*]

proof end;

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))*]

proof end;

theorem :: QUATERN3:5

for z being quaternion number st z is Real holds
z * <i> = [*0 ,(Rea z),0 ,0 *]

proof end;

theorem :: QUATERN3:6

for z being quaternion number st z is Real holds
z * <j> = [*0 ,0 ,(Rea z),0 *]

proof end;

theorem :: QUATERN3:7

for z being quaternion number st z is Real holds
z * <k> = [*0 ,0 ,0 ,(Rea z)*]

proof end;

theorem :: QUATERN3:8

for z being quaternion number holds z - 0q = z

proof end;

theorem :: QUATERN3:9

for z, z1 being quaternion number st z is Real holds
z * z1 = z1 * z

proof end;

theorem :: QUATERN3:10

for z being quaternion number st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds
z = Rea z

proof end;

theorem Th11: :: QUATERN3:11

for z being quaternion number holds |.z.| ^2 = ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )

proof end;

theorem :: QUATERN3:12

for z being quaternion number holds |.z.| ^2 = |.(z * (z *' )).|

proof end;

theorem :: QUATERN3:13

for z being quaternion number holds |.z.| ^2 = Rea (z * (z *' ))

proof end;

theorem :: QUATERN3:14

for z being quaternion number holds 2 * (Rea z) = Rea (z + (z *' ))

proof end;

theorem :: QUATERN3:15

for z, z1 being quaternion number st z is Real holds
(z * z1) *' = (z *' ) * (z1 *' )

proof end;

theorem :: QUATERN3:16

for z1, z2 being quaternion number holds (z1 * z2) *' = (z2 *' ) * (z1 *' )

proof end;

theorem Th17: :: QUATERN3:17

for z1, z2 being quaternion number holds |.(z1 * z2).| ^2 = (|.z1.| ^2 ) * (|.z2.| ^2 )

proof end;

theorem :: QUATERN3:18

for z1 being quaternion number holds (<i> * z1) - (z1 * <i> ) = [*0 ,0 ,(- (2 * (Im3 z1))),(2 * (Im2 z1))*]

proof end;

theorem :: QUATERN3:19

for z1 being quaternion number holds (<i> * z1) + (z1 * <i> ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0 ,0 *]

proof end;

theorem :: QUATERN3:20

for z1 being quaternion number holds (<j> * z1) - (z1 * <j> ) = [*0 ,(2 * (Im3 z1)),0 ,(- (2 * (Im1 z1)))*]

proof end;

theorem :: QUATERN3:21

for z1 being quaternion number holds (<j> * z1) + (z1 * <j> ) = [*(- (2 * (Im2 z1))),0 ,(2 * (Rea z1)),0 *]

proof end;

theorem :: QUATERN3:22

for z1 being quaternion number holds (<k> * z1) - (z1 * <k> ) = [*0 ,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0 *]

proof end;

theorem :: QUATERN3:23

for z1 being quaternion number holds (<k> * z1) + (z1 * <k> ) = [*(- (2 * (Im3 z1))),0 ,0 ,(2 * (Rea z1))*]

proof end;

theorem Th24: :: QUATERN3:24

for z being quaternion number holds Rea ((1 / (|.z.| ^2 )) * (z *' )) = (1 / (|.z.| ^2 )) * (Rea z)

proof end;

theorem Th25: :: QUATERN3:25

for z being quaternion number holds Im1 ((1 / (|.z.| ^2 )) * (z *' )) = - ((1 / (|.z.| ^2 )) * (Im1 z))

proof end;

theorem Th26: :: QUATERN3:26

for z being quaternion number holds Im2 ((1 / (|.z.| ^2 )) * (z *' )) = - ((1 / (|.z.| ^2 )) * (Im2 z))

proof end;

theorem Th27: :: QUATERN3:27

for z being quaternion number holds Im3 ((1 / (|.z.| ^2 )) * (z *' )) = - ((1 / (|.z.| ^2 )) * (Im3 z))

proof end;

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)))*]

proof end;

theorem :: QUATERN3:29

for z being quaternion number holds z * ((1 / (|.z.| ^2 )) * (z *' )) = [*((|.z.| ^2 ) / (|.z.| ^2 )),0 ,0 ,0 *]

proof end;

theorem :: QUATERN3:30

for z1, z2 being quaternion number holds Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) by Lm1;

theorem :: QUATERN3:31

for z1, z2 being quaternion number holds Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by Lm1;

theorem :: QUATERN3:32

for z1, z2 being quaternion number holds Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) by Lm1;

theorem :: QUATERN3:33

for z1, z2 being quaternion number holds Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) by Lm1;

theorem :: QUATERN3:34

for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2 ) * (|.z2.| ^2 )) * (|.z3.| ^2 )

proof end;

theorem :: QUATERN3:35

for z1, z2, z3 being quaternion number holds Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2)

proof end;

theorem Th36: :: QUATERN3:36

for z being quaternion number holds |.(z * z).| = |.((z *' ) * (z *' )).|

proof end;

theorem :: QUATERN3:37

for z being quaternion number holds |.((z *' ) * (z *' )).| = |.z.| ^2

proof end;

theorem :: QUATERN3:38

for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.|

proof end;

theorem :: QUATERN3:39

for z1, z2, z3 being quaternion number holds |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.|

proof end;

theorem :: QUATERN3:40

for z1, z2, z3 being quaternion number holds |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|

proof end;

theorem :: QUATERN3:41

for z1, z2, z3 being quaternion number holds |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|

proof end;

theorem :: QUATERN3:42

for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2

proof end;

theorem :: QUATERN3:43

for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2

proof end;

theorem :: QUATERN3:44

for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).|

proof end;

theorem :: QUATERN3:45

for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.|

proof end;

theorem :: QUATERN3:46

for z1, z2, z being quaternion number holds |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).|

proof end;

theorem :: QUATERN3:47

for z1, z2 being quaternion number st |.z1.| - |.z2.| <> 0 holds
((|.z1.| ^2 ) + (|.z2.| ^2 )) - ((2 * |.z1.|) * |.z2.|) > 0

proof end;

theorem :: QUATERN3:48

for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2

proof end;

theorem :: QUATERN3:49

for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2

proof end;

theorem :: QUATERN3:50

for z1, z2 being quaternion number holds (z1 * z2) " = (z2 " ) * (z1 " )

proof end;

theorem :: QUATERN3:51

for z being quaternion number holds (z *' ) " = (z " ) *'

proof end;

theorem :: QUATERN3:52

1q " = 1q

proof end;

theorem :: QUATERN3:53

for z1, z2 being quaternion number st |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " holds
z1 = z2

proof end;

theorem :: QUATERN3:54

for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4)

proof end;

theorem :: QUATERN3:55

for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4)

proof end;

theorem Th56: :: QUATERN3:56

for z1, z2 being quaternion number holds - (z1 + z2) = (- z1) - z2

proof end;

theorem Th57: :: QUATERN3:57

for z1, z2 being quaternion number holds - (z1 - z2) = (- z1) + z2

proof end;

theorem Th58: :: QUATERN3:58

for z, z1, z2 being quaternion number holds z - (z1 + z2) = (z - z1) - z2

proof end;

theorem Th59: :: QUATERN3:59

for z, z1, z2 being quaternion number holds z - (z1 - z2) = (z - z1) + z2

proof end;

theorem :: QUATERN3:60

for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4)

proof end;

theorem Th61: :: QUATERN3:61

for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4)

proof end;

theorem :: QUATERN3:62

for z1, z2, z3 being quaternion number holds - ((z1 + z2) + z3) = ((- z1) - z2) - z3

proof end;

theorem :: QUATERN3:63

for z1, z2, z3 being quaternion number holds - ((z1 - z2) - z3) = ((- z1) + z2) + z3

proof end;

theorem :: QUATERN3:64

for z1, z2, z3 being quaternion number holds - ((z1 - z2) + z3) = ((- z1) + z2) - z3

proof end;

theorem :: QUATERN3:65

for z1, z2, z3 being quaternion number holds - ((z1 + z2) - z3) = ((- z1) - z2) + z3

proof end;

theorem :: QUATERN3:66

for z1, z, z2 being quaternion number st z1 + z = z2 + z holds
z1 = z2

proof end;

theorem :: QUATERN3:67

for z1, z, z2 being quaternion number st z1 - z = z2 - z holds
z1 = z2

proof end;

theorem :: QUATERN3:68

for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4)

proof end;

theorem :: QUATERN3:69

for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4)

proof end;

theorem :: QUATERN3:70

for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4)

proof end;

theorem :: QUATERN3:71

for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4)

proof end;

theorem :: QUATERN3:72

for z1, z2, z3 being quaternion number holds (z1 - z2) * z3 = (z2 - z1) * (- z3)

proof end;

theorem :: QUATERN3:73

for z3, z1, z2 being quaternion number holds z3 * (z1 - z2) = (- z3) * (z2 - z1)

proof end;

theorem Th74: :: QUATERN3:74

for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1

proof end;

theorem :: QUATERN3:75

for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3)

proof end;

theorem :: QUATERN3:76

for z, z1, z2 being quaternion number holds (z - z1) - z2 = (z - z2) - z1

proof end;

theorem :: QUATERN3:77

for z being quaternion number holds z " = [*((Rea z) / (|.z.| ^2 )),(- ((Im1 z) / (|.z.| ^2 ))),(- ((Im2 z) / (|.z.| ^2 ))),(- ((Im3 z) / (|.z.| ^2 )))*]

proof end;

theorem :: QUATERN3:78

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 ))*]

proof end;

Lm3: <i> = [*0 ,1*]
by ARYTM_0:def 7;

theorem :: QUATERN3:79

<i> " = - <i>

proof end;

theorem :: QUATERN3:80

<j> " = - <j>

proof end;

theorem :: QUATERN3:81

<k> " = - <k>

proof end;

definition

let z be quaternion number ;
func z ^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 ;
cluster z ^2 -> quaternion ;
coherence
z ^2 is quaternion ;

end;

definition

let z be Element of QUATERNION ;
:: original: ^2
redefine func z ^2 -> Element of QUATERNION ;
correctness
coherence
z ^2 is Element of QUATERNION ;
;

end;

theorem Th82: :: QUATERN3:82

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)))*]

proof end;

theorem :: QUATERN3:83

0q ^2 = 0

proof end;

theorem :: QUATERN3:84

1q ^2 = 1

proof end;

theorem Th85: :: QUATERN3:85

for z being quaternion number holds z ^2 = (- z) ^2

proof end;

definition

let z be quaternion number ;
func z ^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 ;
cluster z ^3 -> quaternion ;
coherence
z ^3 is quaternion ;

end;

definition

let z be Element of QUATERNION ;
:: original: ^3
redefine func z ^3 -> Element of QUATERNION ;
correctness
coherence
z ^3 is Element of QUATERNION ;
;

end;

theorem :: QUATERN3:86

0q ^3 = 0

proof end;

theorem :: QUATERN3:87

1q ^3 = 1

proof end;

theorem :: QUATERN3:88

<i> ^3 = - <i>

proof end;

theorem :: QUATERN3:89

<j> ^3 = - <j>

proof end;

theorem :: QUATERN3:90

<k> ^3 = - <k>

proof end;

theorem :: QUATERN3:91

(- 1q ) ^2 = 1

proof end;

theorem :: QUATERN3:92

(- 1q ) ^3 = - 1

proof end;

theorem :: QUATERN3:93

for z being quaternion number holds z ^3 = - ((- z) ^3 )

proof end;