:: Some Operations on Quaternion Numbers
:: by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang
::
:: 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 *')) = (1 / ()) * (Rea z)
proof end;

theorem Th25: :: QUATERN3:25
for z being Quaternion holds Im1 ((1 / ()) * (z *')) = - ((1 / ()) * (Im1 z))
proof end;

theorem Th26: :: QUATERN3:26
for z being Quaternion holds Im2 ((1 / ()) * (z *')) = - ((1 / ()) * (Im2 z))
proof end;

theorem Th27: :: QUATERN3:27
for z being Quaternion holds Im3 ((1 / ()) * (z *')) = - ((1 / ()) * (Im3 z))
proof end;

theorem :: QUATERN3:28
for z being Quaternion holds (1 / ()) * (z *') = [*((1 / ()) * (Rea z)),(- ((1 / ()) * (Im1 z))),(- ((1 / ()) * (Im2 z))),(- ((1 / ()) * (Im3 z)))*]
proof end;

theorem :: QUATERN3:29
for z being Quaternion holds z * ((1 / ()) * (z *')) = [*(() / ()),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
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) / ()),(- ((Im1 z) / ())),(- ((Im2 z) / ())),(- ((Im3 z) / ()))*]
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
proof end;

theorem :: QUATERN3:76
proof end;

theorem :: QUATERN3:77
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;
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
proof end;

theorem :: QUATERN3:80
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;
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
proof end;

theorem :: QUATERN3:83
proof end;

theorem :: QUATERN3:84
proof end;

theorem :: QUATERN3:85
proof end;

theorem :: QUATERN3:86
proof end;

theorem :: QUATERN3:87
() ^2 = 1
proof end;

theorem :: QUATERN3:88
() ^3 = - 1
proof end;

theorem :: QUATERN3:89
for z being Quaternion holds z ^3 = - ((- z) ^3)
proof end;