:: 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

theorem Th1: :: QUATERN3:1

for z1, z2 being Quaternion holds Rea (z1 * z2) = Rea (z2 * z1)

proof end;

Lm1: for z being Quaternion st z is Real holds
( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )

proof end;

theorem :: QUATERN3:2

for z3, z being Quaternion 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 z3, z being Quaternion st z is Real holds
z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]

proof end;

theorem :: QUATERN3:4

for z3, z being Quaternion 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 st z is Real holds
z * <i> = [*0,(Rea z),0,0*]

proof end;

theorem :: QUATERN3:6

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

proof end;

theorem :: QUATERN3:7

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

proof end;

theorem :: QUATERN3:8

for z being Quaternion holds z - 0q = z

proof end;

theorem :: QUATERN3:9

for z1, z being Quaternion st z is Real holds
z * z1 = z1 * z

proof end;

theorem :: QUATERN3:10

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

proof end;

theorem Th11: :: QUATERN3:11

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

proof end;

theorem :: QUATERN3:12

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

proof end;

theorem :: QUATERN3:13

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

proof end;

theorem :: QUATERN3:14

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

proof end;

theorem :: QUATERN3:15

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

proof end;

theorem :: QUATERN3:16

for z1, z2 being Quaternion holds (z1 * z2) *' = (z2 *') * (z1 *')

proof end;

theorem Th17: :: QUATERN3:17

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

proof end;

theorem :: QUATERN3:18

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

proof end;

theorem :: QUATERN3:19

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

proof end;

theorem :: QUATERN3:20

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

proof end;

theorem :: QUATERN3:21

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

proof end;

theorem :: QUATERN3:22

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

proof end;

theorem :: QUATERN3:23

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

proof end;

theorem Th24: :: QUATERN3:24

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

proof end;

theorem Th25: :: QUATERN3:25

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

proof end;

theorem Th26: :: QUATERN3:26

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

proof end;

theorem Th27: :: QUATERN3:27

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

proof end;

theorem :: QUATERN3:28

for z being Quaternion 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 holds z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*]

proof end;

theorem :: QUATERN3:30

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

proof end;

theorem :: QUATERN3:31

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

proof end;

theorem Th32: :: QUATERN3:32

for z being Quaternion holds |.(z * z).| = |.((z *') * (z *')).|

proof end;

theorem :: QUATERN3:33

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

proof end;

theorem :: QUATERN3:34

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

proof end;

theorem :: QUATERN3:35

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

proof end;

theorem :: QUATERN3:36

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

proof end;

theorem :: QUATERN3:37

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

proof end;

theorem :: QUATERN3:38

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

proof end;

theorem :: QUATERN3:39

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

proof end;

theorem :: QUATERN3:40

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

proof end;

theorem :: QUATERN3:41

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

proof end;

theorem :: QUATERN3:42

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

proof end;

theorem :: QUATERN3:43

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

proof end;

theorem :: QUATERN3:44

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

proof end;

theorem :: QUATERN3:45

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

proof end;

theorem :: QUATERN3:46

for z1, z2 being Quaternion holds (z1 * z2) " = (z2 ") * (z1 ")

proof end;

theorem :: QUATERN3:47

for z being Quaternion holds (z *') " = (z ") *'

proof end;

theorem :: QUATERN3:48

1q " = 1q

proof end;

theorem :: QUATERN3:49

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

proof end;

theorem :: QUATERN3:50

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

proof end;

theorem :: QUATERN3:51

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

proof end;

theorem Th52: :: QUATERN3:52

for z1, z2 being Quaternion holds - (z1 + z2) = (- z1) - z2

proof end;

theorem Th53: :: QUATERN3:53

for z1, z2 being Quaternion holds - (z1 - z2) = (- z1) + z2

proof end;

theorem Th54: :: QUATERN3:54

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

proof end;

theorem Th55: :: QUATERN3:55

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

proof end;

theorem :: QUATERN3:56

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

proof end;

theorem Th57: :: QUATERN3:57

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

proof end;

theorem :: QUATERN3:58

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

proof end;

theorem :: QUATERN3:59

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

proof end;

theorem :: QUATERN3:60

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

proof end;

theorem :: QUATERN3:61

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

proof end;

theorem :: QUATERN3:62

for z1, z2, z being Quaternion st z1 + z = z2 + z holds
z1 = z2

proof end;

theorem :: QUATERN3:63

for z1, z2, z being Quaternion st z1 - z = z2 - z holds
z1 = z2

proof end;

theorem :: QUATERN3:64

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

proof end;

theorem :: QUATERN3:65

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

proof end;

theorem :: QUATERN3:66

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

proof end;

theorem :: QUATERN3:67

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

proof end;

theorem :: QUATERN3:68

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

proof end;

theorem :: QUATERN3:69

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

proof end;

theorem Th70: :: QUATERN3:70

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

proof end;

theorem :: QUATERN3:71

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

proof end;

theorem :: QUATERN3:72

for z1, z2, z being Quaternion holds (z - z1) - z2 = (z - z2) - z1

proof end;

theorem :: QUATERN3:73

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

proof end;

theorem :: QUATERN3:74

for z1, z2 being Quaternion 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;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

Lm2: <i> = [*(In (0,REAL)),jj*]
by ARYTM_0:def 5;

theorem :: QUATERN3:75

<i> " = - <i>

proof end;

theorem :: QUATERN3:76

<j> " = - <j>

proof end;

theorem :: QUATERN3:77

<k> " = - <k>

proof end;

definition

let z be Quaternion;

func z ^2 -> Number equals :: QUATERN3:def 1
z * z;

correctness
coherence
z * z is Number ;
;

end;

:: deftheorem defines ^2 QUATERN3:def 1 :
for z being Quaternion holds z ^2 = z * z;

registration

let z be Quaternion;

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 Th78: :: QUATERN3:78

for z being Quaternion 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:79

0q ^2 = 0

proof end;

theorem :: QUATERN3:80

1q ^2 = 1

proof end;

theorem Th81: :: QUATERN3:81

for z being Quaternion holds z ^2 = (- z) ^2

proof end;

definition

let z be Quaternion;

func z ^3 -> Number equals :: QUATERN3:def 2
(z * z) * z;

coherence
(z * z) * z is Number ;

end;

:: deftheorem defines ^3 QUATERN3:def 2 :
for z being Quaternion holds z ^3 = (z * z) * z;

registration

let z be Quaternion;

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:82

0q ^3 = 0

proof end;

theorem :: QUATERN3:83

1q ^3 = 1

proof end;

theorem :: QUATERN3:84

<i> ^3 = - <i>

proof end;

theorem :: QUATERN3:85

<j> ^3 = - <j>

proof end;

theorem :: QUATERN3:86

<k> ^3 = - <k>

proof end;

theorem :: QUATERN3:87

(- 1q) ^2 = 1

proof end;

theorem :: QUATERN3:88

(- 1q) ^3 = - 1

proof end;

theorem :: QUATERN3:89

for z being Quaternion holds z ^3 = - ((- z) ^3)

proof end;