:: QUATERN3 semantic presentation
begin
theorem
:: QUATERN3:1
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
Rea
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
Rea
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:2
for
z
,
z3
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
+
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
Rea
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im1
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
)
)
: ( ( ) (
quaternion
)
set
)
+
(
(
Im2
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
(
Im3
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:3
for
z
,
z3
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
-
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
Rea
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
Im1
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
Im2
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
Im3
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:4
for
z
,
z3
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:5
for
z
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
*
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:6
for
z
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
*
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:7
for
z
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
*
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:8
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
-
0q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
z
: ( (
quaternion
) (
quaternion
)
number
) ;
theorem
:: QUATERN3:9
for
z
,
z1
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
*
z1
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:10
for
z
being ( (
quaternion
) (
quaternion
)
number
) st
Im1
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) &
Im2
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) &
Im3
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
=
Rea
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:11
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
(
(
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im1
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im2
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im3
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:12
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
|.
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:13
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
Rea
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:14
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds 2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
Rea
(
z
: ( (
quaternion
) (
quaternion
)
number
)
+
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:15
for
z
,
z1
being ( (
quaternion
) (
quaternion
)
number
) st
z
: ( (
quaternion
) (
quaternion
)
number
) is ( ( ) (
V28
()
V29
()
ext-real
)
Real
) holds
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*'
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:16
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*'
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:17
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:18
for
z1
being ( (
quaternion
) (
quaternion
)
number
) holds
(
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
-
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:19
for
z1
being ( (
quaternion
) (
quaternion
)
number
) holds
(
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
-
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:20
for
z1
being ( (
quaternion
) (
quaternion
)
number
) holds
(
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
-
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:21
for
z1
being ( (
quaternion
) (
quaternion
)
number
) holds
(
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
-
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:22
for
z1
being ( (
quaternion
) (
quaternion
)
number
) holds
(
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
-
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:23
for
z1
being ( (
quaternion
) (
quaternion
)
number
) holds
(
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
-
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:24
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
Rea
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:25
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
Im1
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
-
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:26
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
Im2
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
-
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:27
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
Im3
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
-
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:28
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
set
)
=
[*
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:29
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
*
(
(
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
set
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:30
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
(
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
|.
z3
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:31
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
Rea
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
Rea
(
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
*
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:32
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
|.
(
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:33
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:34
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
|.
z3
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:35
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z3
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:36
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z3
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:37
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z3
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:38
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
(
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:39
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
(
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:40
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
|.
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:41
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:42
for
z1
,
z2
,
z
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<=
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
(
z
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:43
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) st
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<>
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
>
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: QUATERN3:44
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
>=
(
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:45
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
>=
(
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
|.
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:46
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
"
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
"
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:47
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z
: ( (
quaternion
) (
quaternion
)
number
)
*'
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z
: ( (
quaternion
) (
quaternion
)
number
)
"
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*'
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:48
1q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
1q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:49
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) st
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
=
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) &
|.
z1
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
<>
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) &
z1
: ( (
quaternion
) (
quaternion
)
number
)
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
z2
: ( (
quaternion
) (
quaternion
)
number
)
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) holds
z1
: ( (
quaternion
) (
quaternion
)
number
)
=
z2
: ( (
quaternion
) (
quaternion
)
number
) ;
theorem
:: QUATERN3:50
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
+
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:51
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
+
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:52
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z2
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:53
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z2
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:54
for
z
,
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z2
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:55
for
z
,
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z2
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:56
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
-
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:57
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
-
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:58
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
-
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:59
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
-
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:60
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
-
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:61
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
-
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:62
for
z1
,
z
,
z2
being ( (
quaternion
) (
quaternion
)
number
) st
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
z2
: ( (
quaternion
) (
quaternion
)
number
)
+
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) holds
z1
: ( (
quaternion
) (
quaternion
)
number
)
=
z2
: ( (
quaternion
) (
quaternion
)
number
) ;
theorem
:: QUATERN3:63
for
z1
,
z
,
z2
being ( (
quaternion
) (
quaternion
)
number
) st
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) holds
z1
: ( (
quaternion
) (
quaternion
)
number
)
=
z2
: ( (
quaternion
) (
quaternion
)
number
) ;
theorem
:: QUATERN3:64
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z4
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:65
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z4
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:66
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z4
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:67
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
+
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z4
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
*
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:68
for
z1
,
z2
,
z3
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z3
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:69
for
z3
,
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
z3
: ( (
quaternion
) (
quaternion
)
number
)
*
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:70
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z4
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
(
z4
: ( (
quaternion
) (
quaternion
)
number
)
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
+
z1
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:71
for
z1
,
z2
,
z3
,
z4
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z1
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z3
: ( (
quaternion
) (
quaternion
)
number
)
-
z4
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z2
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
(
z4
: ( (
quaternion
) (
quaternion
)
number
)
-
z3
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:72
for
z
,
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
(
z
: ( (
quaternion
) (
quaternion
)
number
)
-
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z2
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
(
z
: ( (
quaternion
) (
quaternion
)
number
)
-
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
-
z1
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:73
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
(
Im1
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
(
Im2
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
-
(
(
Im3
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:74
for
z1
,
z2
being ( (
quaternion
) (
quaternion
)
number
) holds
z1
: ( (
quaternion
) (
quaternion
)
number
)
/
z2
: ( (
quaternion
) (
quaternion
)
number
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
[*
(
(
(
(
(
(
Rea
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im2
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im3
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
(
(
(
(
(
Rea
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im1
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im2
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im3
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
(
(
(
(
(
Rea
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im1
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im2
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im3
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
(
(
(
(
(
Rea
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im1
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
+
(
(
Im2
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im3
z2
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Rea
z1
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
/
(
|.
z2
: ( (
quaternion
) (
quaternion
)
number
)
.|
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:75
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:76
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:77
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
"
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
definition
let
z
be ( (
quaternion
) (
quaternion
)
number
) ;
func
z
^2
->
( ( ) ( )
set
)
equals
:: QUATERN3:def 1
z
: ( ( ) ( )
Element
of the
U1
of
K272
() : ( (
V109
() ) (
V109
() )
L11
()) : ( ( ) ( )
set
) )
*
z
: ( ( ) ( )
Element
of the
U1
of
K272
() : ( (
V109
() ) (
V109
() )
L11
()) : ( ( ) ( )
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
end;
registration
let
z
be ( (
quaternion
) (
quaternion
)
number
) ;
cluster
z
: ( (
quaternion
) (
quaternion
)
set
)
^2
: ( ( ) ( )
set
)
->
quaternion
;
end;
definition
let
z
be ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
:: original:
^2
redefine
func
z
^2
->
( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
end;
theorem
:: QUATERN3:78
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
^2
: ( ( ) (
quaternion
)
set
)
=
[*
(
(
(
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im1
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im2
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
-
(
(
Im3
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
^2
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im1
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im2
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ,
(
2 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
Rea
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*
(
Im3
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
)
: ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) )
*]
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:79
0q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^2
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: QUATERN3:80
1q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^2
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: QUATERN3:81
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
^2
: ( ( ) (
quaternion
)
set
)
=
(
-
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^2
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
definition
let
z
be ( (
quaternion
) (
quaternion
)
number
) ;
func
z
^3
->
( ( ) ( )
set
)
equals
:: QUATERN3:def 2
(
z
: ( (
quaternion
) (
quaternion
)
set
)
*
z
: ( (
quaternion
) (
quaternion
)
set
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
*
z
: ( (
quaternion
) (
quaternion
)
set
) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
end;
registration
let
z
be ( (
quaternion
) (
quaternion
)
number
) ;
cluster
z
: ( (
quaternion
) (
quaternion
)
set
)
^3
: ( ( ) ( )
set
)
->
quaternion
;
end;
definition
let
z
be ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
:: original:
^3
redefine
func
z
^3
->
( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
end;
theorem
:: QUATERN3:82
0q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
0
: ( ( ) (
natural
V28
()
V29
()
ext-real
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: QUATERN3:83
1q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: QUATERN3:84
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
<i>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:85
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
<j>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:86
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
<k>
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;
theorem
:: QUATERN3:87
(
-
1q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^2
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: QUATERN3:88
(
-
1q
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
=
-
1 : ( ( ) ( non
zero
natural
V28
()
V29
()
ext-real
positive
V43
()
V44
()
V45
()
V46
()
V47
()
V48
() )
Element
of
NAT
: ( ( ) (
V43
()
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K19
(
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V28
()
V29
()
ext-real
)
Element
of
REAL
: ( ( ) (
V43
()
V44
()
V45
()
V49
() )
set
) ) ;
theorem
:: QUATERN3:89
for
z
being ( (
quaternion
) (
quaternion
)
number
) holds
z
: ( (
quaternion
) (
quaternion
)
number
)
^3
: ( ( ) (
quaternion
)
set
)
=
-
(
(
-
z
: ( (
quaternion
) (
quaternion
)
number
)
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) )
^3
)
: ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) : ( ( ) (
quaternion
)
Element
of
QUATERNION
: ( ( ) ( non
zero
)
set
) ) ;