:: 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
)
proof
end;
Lm1
:
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
,
z3
being
quaternion
number
holds
|.
(
(
z1
*
z2
)
*
z3
)
.|
^2
=
(
(
|.
z1
.|
^2
)
*
(
|.
z2
.|
^2
)
)
*
(
|.
z3
.|
^2
)
proof
end;
theorem
:: QUATERN3:31
for
z1
,
z2
,
z3
being
quaternion
number
holds
Rea
(
(
z1
*
z2
)
*
z3
)
=
Rea
(
(
z3
*
z1
)
*
z2
)
proof
end;
theorem
Th32
:
:: QUATERN3:32
for
z
being
quaternion
number
holds
|.
(
z
*
z
)
.|
=
|.
(
(
z
*'
)
*
(
z
*'
)
)
.|
proof
end;
theorem
:: QUATERN3:33
for
z
being
quaternion
number
holds
|.
(
(
z
*'
)
*
(
z
*'
)
)
.|
=
|.
z
.|
^2
proof
end;
theorem
:: QUATERN3:34
for
z1
,
z2
,
z3
being
quaternion
number
holds
|.
(
(
z1
*
z2
)
*
z3
)
.|
=
(
|.
z1
.|
*
|.
z2
.|
)
*
|.
z3
.|
proof
end;
theorem
:: QUATERN3:35
for
z1
,
z2
,
z3
being
quaternion
number
holds
|.
(
(
z1
+
z2
)
+
z3
)
.|
<=
(
|.
z1
.|
+
|.
z2
.|
)
+
|.
z3
.|
proof
end;
theorem
:: QUATERN3:36
for
z1
,
z2
,
z3
being
quaternion
number
holds
|.
(
(
z1
+
z2
)
-
z3
)
.|
<=
(
|.
z1
.|
+
|.
z2
.|
)
+
|.
z3
.|
proof
end;
theorem
:: QUATERN3:37
for
z1
,
z2
,
z3
being
quaternion
number
holds
|.
(
(
z1
-
z2
)
-
z3
)
.|
<=
(
|.
z1
.|
+
|.
z2
.|
)
+
|.
z3
.|
proof
end;
theorem
:: QUATERN3:38
for
z1
,
z2
being
quaternion
number
holds
|.
z1
.|
-
|.
z2
.|
<=
(
|.
(
z1
+
z2
)
.|
+
|.
(
z1
-
z2
)
.|
)
/
2
proof
end;
theorem
:: QUATERN3:39
for
z1
,
z2
being
quaternion
number
holds
|.
z1
.|
-
|.
z2
.|
<=
(
|.
(
z1
+
z2
)
.|
+
|.
(
z2
-
z1
)
.|
)
/
2
proof
end;
theorem
:: QUATERN3:40
for
z1
,
z2
being
quaternion
number
holds
|.
(
|.
z1
.|
-
|.
z2
.|
)
.|
<=
|.
(
z2
-
z1
)
.|
proof
end;
theorem
:: QUATERN3:41
for
z1
,
z2
being
quaternion
number
holds
|.
(
|.
z1
.|
-
|.
z2
.|
)
.|
<=
|.
z1
.|
+
|.
z2
.|
proof
end;
theorem
:: QUATERN3:42
for
z1
,
z2
,
z
being
quaternion
number
holds
|.
z1
.|
-
|.
z2
.|
<=
|.
(
z1
-
z
)
.|
+
|.
(
z
-
z2
)
.|
proof
end;
theorem
:: QUATERN3:43
for
z1
,
z2
being
quaternion
number
st
|.
z1
.|
-
|.
z2
.|
<>
0
holds
(
(
|.
z1
.|
^2
)
+
(
|.
z2
.|
^2
)
)
-
(
(
2
*
|.
z1
.|
)
*
|.
z2
.|
)
>
0
proof
end;
theorem
:: QUATERN3:44
for
z1
,
z2
being
quaternion
number
holds
|.
z1
.|
+
|.
z2
.|
>=
(
|.
(
z1
+
z2
)
.|
+
|.
(
z2
-
z1
)
.|
)
/
2
proof
end;
theorem
:: QUATERN3:45
for
z1
,
z2
being
quaternion
number
holds
|.
z1
.|
+
|.
z2
.|
>=
(
|.
(
z1
+
z2
)
.|
+
|.
(
z1
-
z2
)
.|
)
/
2
proof
end;
theorem
:: QUATERN3:46
for
z1
,
z2
being
quaternion
number
holds
(
z1
*
z2
)
"
=
(
z2
"
)
*
(
z1
"
)
proof
end;
theorem
:: QUATERN3:47
for
z
being
quaternion
number
holds
(
z
*'
)
"
=
(
z
"
)
*'
proof
end;
theorem
:: QUATERN3:48
1q
"
=
1q
proof
end;
theorem
:: QUATERN3:49
for
z1
,
z2
being
quaternion
number
st
|.
z1
.|
=
|.
z2
.|
&
|.
z1
.|
<>
0
&
z1
"
=
z2
"
holds
z1
=
z2
proof
end;
theorem
:: QUATERN3:50
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:51
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
z1
+
z2
)
*
(
z3
+
z4
)
=
(
(
(
z1
*
z3
)
+
(
z2
*
z3
)
)
+
(
z1
*
z4
)
)
+
(
z2
*
z4
)
proof
end;
theorem
Th52
:
:: QUATERN3:52
for
z1
,
z2
being
quaternion
number
holds
-
(
z1
+
z2
)
=
(
-
z1
)
-
z2
proof
end;
theorem
Th53
:
:: QUATERN3:53
for
z1
,
z2
being
quaternion
number
holds
-
(
z1
-
z2
)
=
(
-
z1
)
+
z2
proof
end;
theorem
Th54
:
:: QUATERN3:54
for
z
,
z1
,
z2
being
quaternion
number
holds
z
-
(
z1
+
z2
)
=
(
z
-
z1
)
-
z2
proof
end;
theorem
Th55
:
:: QUATERN3:55
for
z
,
z1
,
z2
being
quaternion
number
holds
z
-
(
z1
-
z2
)
=
(
z
-
z1
)
+
z2
proof
end;
theorem
:: QUATERN3:56
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
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
number
holds
(
z1
-
z2
)
*
(
z3
-
z4
)
=
(
(
(
z1
*
z3
)
-
(
z2
*
z3
)
)
-
(
z1
*
z4
)
)
+
(
z2
*
z4
)
proof
end;
theorem
:: QUATERN3:58
for
z1
,
z2
,
z3
being
quaternion
number
holds
-
(
(
z1
+
z2
)
+
z3
)
=
(
(
-
z1
)
-
z2
)
-
z3
proof
end;
theorem
:: QUATERN3:59
for
z1
,
z2
,
z3
being
quaternion
number
holds
-
(
(
z1
-
z2
)
-
z3
)
=
(
(
-
z1
)
+
z2
)
+
z3
proof
end;
theorem
:: QUATERN3:60
for
z1
,
z2
,
z3
being
quaternion
number
holds
-
(
(
z1
-
z2
)
+
z3
)
=
(
(
-
z1
)
+
z2
)
-
z3
proof
end;
theorem
:: QUATERN3:61
for
z1
,
z2
,
z3
being
quaternion
number
holds
-
(
(
z1
+
z2
)
-
z3
)
=
(
(
-
z1
)
-
z2
)
+
z3
proof
end;
theorem
:: QUATERN3:62
for
z1
,
z
,
z2
being
quaternion
number
st
z1
+
z
=
z2
+
z
holds
z1
=
z2
proof
end;
theorem
:: QUATERN3:63
for
z1
,
z
,
z2
being
quaternion
number
st
z1
-
z
=
z2
-
z
holds
z1
=
z2
proof
end;
theorem
:: QUATERN3:64
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
(
z1
+
z2
)
-
z3
)
*
z4
=
(
(
z1
*
z4
)
+
(
z2
*
z4
)
)
-
(
z3
*
z4
)
proof
end;
theorem
:: QUATERN3:65
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
(
z1
-
z2
)
+
z3
)
*
z4
=
(
(
z1
*
z4
)
-
(
z2
*
z4
)
)
+
(
z3
*
z4
)
proof
end;
theorem
:: QUATERN3:66
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
(
z1
-
z2
)
-
z3
)
*
z4
=
(
(
z1
*
z4
)
-
(
z2
*
z4
)
)
-
(
z3
*
z4
)
proof
end;
theorem
:: QUATERN3:67
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
(
z1
+
z2
)
+
z3
)
*
z4
=
(
(
z1
*
z4
)
+
(
z2
*
z4
)
)
+
(
z3
*
z4
)
proof
end;
theorem
:: QUATERN3:68
for
z1
,
z2
,
z3
being
quaternion
number
holds
(
z1
-
z2
)
*
z3
=
(
z2
-
z1
)
*
(
-
z3
)
proof
end;
theorem
:: QUATERN3:69
for
z3
,
z1
,
z2
being
quaternion
number
holds
z3
*
(
z1
-
z2
)
=
(
-
z3
)
*
(
z2
-
z1
)
proof
end;
theorem
Th70
:
:: QUATERN3:70
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
(
z1
-
z2
)
-
z3
)
+
z4
=
(
(
z4
-
z3
)
-
z2
)
+
z1
proof
end;
theorem
:: QUATERN3:71
for
z1
,
z2
,
z3
,
z4
being
quaternion
number
holds
(
z1
-
z2
)
*
(
z3
-
z4
)
=
(
z2
-
z1
)
*
(
z4
-
z3
)
proof
end;
theorem
:: QUATERN3:72
for
z
,
z1
,
z2
being
quaternion
number
holds
(
z
-
z1
)
-
z2
=
(
z
-
z2
)
-
z1
proof
end;
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
)
)
)
*]
proof
end;
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
)
)
*]
proof
end;
Lm2
:
<i>
=
[*
0
,1
*]
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
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
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
)
)
)
*]
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
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: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
number
holds
z
^3
=
-
(
(
-
z
)
^3
)
proof
end;