:: QUATERN3 semantic presentation

REAL is V43() V44() V45() V49() set
NAT is V43() V44() V45() V46() V47() V48() V49() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V43() V49() set
0 is set
1 is non zero natural V28() V29() ext-real positive V43() V44() V45() V46() V47() V48() Element of NAT
K81(0,1) is set
QUATERNION is non zero set
omega is V43() V44() V45() V46() V47() V48() V49() set
K19(omega) is set
K20(QUATERNION,QUATERNION) is set
K19(K20(QUATERNION,QUATERNION)) is set
K20(K20(QUATERNION,QUATERNION),QUATERNION) is set
K19(K20(K20(QUATERNION,QUATERNION),QUATERNION)) is set
K272() is V109() L11()
the U1 of K272() is set
0 is natural V28() V29() ext-real V43() V44() V45() V46() V47() V48() Element of NAT
2 is non zero natural V28() V29() ext-real positive V43() V44() V45() V46() V47() V48() Element of NAT
3 is non zero natural V28() V29() ext-real positive V43() V44() V45() V46() V47() V48() Element of NAT
1q is quaternion set
Rea 1q is V28() V29() ext-real Element of REAL
Im1 1q is V28() V29() ext-real Element of REAL
Im2 1q is V28() V29() ext-real Element of REAL
Im3 1q is V28() V29() ext-real Element of REAL
K107() is quaternion set
K88(REAL,0,1,0,1) is V6() V18(K81(0,1), REAL ) Element of K19(K20(K81(0,1),REAL))
K81(0,1) is V43() V44() V45() V46() V47() V48() set
K20(K81(0,1),REAL) is set
K19(K20(K81(0,1),REAL)) is set
Rea K107() is V28() V29() ext-real Element of REAL
Im1 K107() is V28() V29() ext-real Element of REAL
Im2 K107() is V28() V29() ext-real Element of REAL
Im3 K107() is V28() V29() ext-real Element of REAL
<j> is quaternion Element of QUATERNION
K200(NAT,0,1,2,3,0,0,1,0) is V1() V6() V18(K191(0,1,2,3), NAT ) Element of K19(K20(K191(0,1,2,3),NAT))
K191(0,1,2,3) is set
K20(K191(0,1,2,3),NAT) is set
K19(K20(K191(0,1,2,3),NAT)) is set
K87(0,1,0,0) is set
K87(2,3,1,0) is set
K84(K87(0,1,0,0),K87(2,3,1,0)) is V1() V6() set
[*0,0,1,0*] is quaternion Element of QUATERNION
Rea <j> is V28() V29() ext-real Element of REAL
Im1 <j> is V28() V29() ext-real Element of REAL
Im2 <j> is V28() V29() ext-real Element of REAL
Im3 <j> is V28() V29() ext-real Element of REAL
<k> is quaternion Element of QUATERNION
K200(NAT,0,1,2,3,0,0,0,1) is V1() V6() V18(K191(0,1,2,3), NAT ) Element of K19(K20(K191(0,1,2,3),NAT))
K87(2,3,0,1) is set
K84(K87(0,1,0,0),K87(2,3,0,1)) is V1() V6() set
[*0,0,0,1*] is quaternion Element of QUATERNION
Rea <k> is V28() V29() ext-real Element of REAL
Im1 <k> is V28() V29() ext-real Element of REAL
Im2 <k> is V28() V29() ext-real Element of REAL
Im3 <k> is V28() V29() ext-real Element of REAL
|.1q.| is V29() set
(Rea 1q) ^2 is V28() V29() ext-real Element of REAL
K109((Rea 1q),(Rea 1q)) is set
(Im1 1q) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 1q),(Im1 1q)) is set
((Rea 1q) ^2) + ((Im1 1q) ^2) is V28() V29() ext-real Element of REAL
(Im2 1q) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 1q),(Im2 1q)) is set
(((Rea 1q) ^2) + ((Im1 1q) ^2)) + ((Im2 1q) ^2) is V28() V29() ext-real Element of REAL
(Im3 1q) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 1q),(Im3 1q)) is set
((((Rea 1q) ^2) + ((Im1 1q) ^2)) + ((Im2 1q) ^2)) + ((Im3 1q) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea 1q) ^2) + ((Im1 1q) ^2)) + ((Im2 1q) ^2)) + ((Im3 1q) ^2)) is V28() V29() ext-real Element of REAL
|.K107().| is V29() set
(Rea K107()) ^2 is V28() V29() ext-real Element of REAL
K109((Rea K107()),(Rea K107())) is set
(Im1 K107()) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 K107()),(Im1 K107())) is set
((Rea K107()) ^2) + ((Im1 K107()) ^2) is V28() V29() ext-real Element of REAL
(Im2 K107()) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 K107()),(Im2 K107())) is set
(((Rea K107()) ^2) + ((Im1 K107()) ^2)) + ((Im2 K107()) ^2) is V28() V29() ext-real Element of REAL
(Im3 K107()) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 K107()),(Im3 K107())) is set
((((Rea K107()) ^2) + ((Im1 K107()) ^2)) + ((Im2 K107()) ^2)) + ((Im3 K107()) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea K107()) ^2) + ((Im1 K107()) ^2)) + ((Im2 K107()) ^2)) + ((Im3 K107()) ^2)) is V28() V29() ext-real Element of REAL
|.<j>.| is V29() set
(Rea <j>) ^2 is V28() V29() ext-real Element of REAL
K109((Rea <j>),(Rea <j>)) is set
(Im1 <j>) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 <j>),(Im1 <j>)) is set
((Rea <j>) ^2) + ((Im1 <j>) ^2) is V28() V29() ext-real Element of REAL
(Im2 <j>) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 <j>),(Im2 <j>)) is set
(((Rea <j>) ^2) + ((Im1 <j>) ^2)) + ((Im2 <j>) ^2) is V28() V29() ext-real Element of REAL
(Im3 <j>) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 <j>),(Im3 <j>)) is set
((((Rea <j>) ^2) + ((Im1 <j>) ^2)) + ((Im2 <j>) ^2)) + ((Im3 <j>) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea <j>) ^2) + ((Im1 <j>) ^2)) + ((Im2 <j>) ^2)) + ((Im3 <j>) ^2)) is V28() V29() ext-real Element of REAL
|.<k>.| is V29() set
(Rea <k>) ^2 is V28() V29() ext-real Element of REAL
K109((Rea <k>),(Rea <k>)) is set
(Im1 <k>) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 <k>),(Im1 <k>)) is set
((Rea <k>) ^2) + ((Im1 <k>) ^2) is V28() V29() ext-real Element of REAL
(Im2 <k>) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 <k>),(Im2 <k>)) is set
(((Rea <k>) ^2) + ((Im1 <k>) ^2)) + ((Im2 <k>) ^2) is V28() V29() ext-real Element of REAL
(Im3 <k>) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 <k>),(Im3 <k>)) is set
((((Rea <k>) ^2) + ((Im1 <k>) ^2)) + ((Im2 <k>) ^2)) + ((Im3 <k>) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea <k>) ^2) + ((Im1 <k>) ^2)) + ((Im2 <k>) ^2)) + ((Im3 <k>) ^2)) is V28() V29() ext-real Element of REAL
1q is quaternion Element of QUATERNION
- 1q is quaternion Element of QUATERNION
<i> is quaternion Element of QUATERNION
z is quaternion set
z2 is quaternion set
z * z2 is quaternion Element of QUATERNION
Rea (z * z2) is V28() V29() ext-real Element of REAL
z2 * z is quaternion Element of QUATERNION
Rea (z2 * z) is V28() V29() ext-real Element of REAL
Rea z2 is V28() V29() ext-real Element of REAL
Rea z is V28() V29() ext-real Element of REAL
(Rea z2) * (Rea z) is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z2) * (Im1 z) is V28() V29() ext-real Element of REAL
((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z)) is V28() V29() ext-real Element of REAL
K110(((Im1 z2) * (Im1 z))) is V28() set
K108(((Rea z2) * (Rea z)),K110(((Im1 z2) * (Im1 z)))) is set
Im2 z2 is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z2) * (Im2 z) is V28() V29() ext-real Element of REAL
(((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z)) is V28() V29() ext-real Element of REAL
K110(((Im2 z2) * (Im2 z))) is V28() set
K108((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))),K110(((Im2 z2) * (Im2 z)))) is set
Im3 z2 is V28() V29() ext-real Element of REAL
Im3 z is V28() V29() ext-real Element of REAL
(Im3 z2) * (Im3 z) is V28() V29() ext-real Element of REAL
((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))) - ((Im3 z2) * (Im3 z)) is V28() V29() ext-real Element of REAL
K110(((Im3 z2) * (Im3 z))) is V28() set
K108(((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))),K110(((Im3 z2) * (Im3 z)))) is set
z is quaternion set
Rea z is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
Im3 z is V28() V29() ext-real Element of REAL
z2 is V28() V29() ext-real Element of REAL
[*z2,0*] is V28() Element of COMPLEX
[*z2,0,0,0*] is quaternion Element of QUATERNION
z is quaternion set
Rea z is V28() V29() ext-real Element of REAL
z2 is quaternion set
z + z2 is quaternion Element of QUATERNION
Rea z2 is V28() V29() ext-real Element of REAL
(Rea z) + (Rea z2) is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
(Im1 z2) * <i> is quaternion set
((Rea z) + (Rea z2)) + ((Im1 z2) * <i>) is quaternion set
Im2 z2 is V28() V29() ext-real Element of REAL
(Im2 z2) * <j> is quaternion set
(((Rea z) + (Rea z2)) + ((Im1 z2) * <i>)) + ((Im2 z2) * <j>) is quaternion Element of QUATERNION
Im3 z2 is V28() V29() ext-real Element of REAL
(Im3 z2) * <k> is quaternion set
((((Rea z) + (Rea z2)) + ((Im1 z2) * <i>)) + ((Im2 z2) * <j>)) + ((Im3 z2) * <k>) is quaternion Element of QUATERNION
Im3 z is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z) + (Im1 z2) is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z) + (Im2 z2) is V28() V29() ext-real Element of REAL
(Im3 z) + (Im3 z2) is V28() V29() ext-real Element of REAL
[*((Rea z) + (Rea z2)),((Im1 z) + (Im1 z2)),((Im2 z) + (Im2 z2)),((Im3 z) + (Im3 z2))*] is quaternion Element of QUATERNION
Rea [*((Rea z) + (Rea z2)),((Im1 z) + (Im1 z2)),((Im2 z) + (Im2 z2)),((Im3 z) + (Im3 z2))*] is V28() V29() ext-real Element of REAL
z2 is quaternion set
Rea z2 is V28() V29() ext-real Element of REAL
Im1 [*((Rea z) + (Rea z2)),((Im1 z) + (Im1 z2)),((Im2 z) + (Im2 z2)),((Im3 z) + (Im3 z2))*] is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
Im3 [*((Rea z) + (Rea z2)),((Im1 z) + (Im1 z2)),((Im2 z) + (Im2 z2)),((Im3 z) + (Im3 z2))*] is V28() V29() ext-real Element of REAL
Im3 z2 is V28() V29() ext-real Element of REAL
Im2 [*((Rea z) + (Rea z2)),((Im1 z) + (Im1 z2)),((Im2 z) + (Im2 z2)),((Im3 z) + (Im3 z2))*] is V28() V29() ext-real Element of REAL
Im2 z2 is V28() V29() ext-real Element of REAL
[*((Rea z) + (Rea z2)),(Im1 z2),(Im2 z2),(Im3 z2)*] is quaternion Element of QUATERNION
z is quaternion set
Rea z is V28() V29() ext-real Element of REAL
z2 is quaternion set
z - z2 is quaternion Element of QUATERNION
- z2 is quaternion set
z + (- z2) is quaternion set
Rea z2 is V28() V29() ext-real Element of REAL
(Rea z) - (Rea z2) is V28() V29() ext-real Element of REAL
K110((Rea z2)) is V28() set
K108((Rea z),K110((Rea z2))) is set
Im1 z2 is V28() V29() ext-real Element of REAL
- (Im1 z2) is V28() V29() ext-real Element of REAL
Im2 z2 is V28() V29() ext-real Element of REAL
- (Im2 z2) is V28() V29() ext-real Element of REAL
Im3 z2 is V28() V29() ext-real Element of REAL
- (Im3 z2) is V28() V29() ext-real Element of REAL
[*((Rea z) - (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] is quaternion Element of QUATERNION
- z2 is quaternion Element of QUATERNION
z + (- z2) is quaternion Element of QUATERNION
Im3 z is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z) - (Im1 z2) is V28() V29() ext-real Element of REAL
K110((Im1 z2)) is V28() set
K108((Im1 z),K110((Im1 z2))) is set
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z) - (Im2 z2) is V28() V29() ext-real Element of REAL
K110((Im2 z2)) is V28() set
K108((Im2 z),K110((Im2 z2))) is set
(Im3 z) - (Im3 z2) is V28() V29() ext-real Element of REAL
K110((Im3 z2)) is V28() set
K108((Im3 z),K110((Im3 z2))) is set
[*((Rea z) - (Rea z2)),((Im1 z) - (Im1 z2)),((Im2 z) - (Im2 z2)),((Im3 z) - (Im3 z2))*] is quaternion Element of QUATERNION
Rea [*((Rea z) - (Rea z2)),((Im1 z) - (Im1 z2)),((Im2 z) - (Im2 z2)),((Im3 z) - (Im3 z2))*] is V28() V29() ext-real Element of REAL
- (Rea z2) is V28() V29() ext-real Element of REAL
(Rea z) + (- (Rea z2)) is V28() V29() ext-real Element of REAL
Rea (- z2) is V28() V29() ext-real Element of REAL
(Rea z) + (Rea (- z2)) is V28() V29() ext-real Element of REAL
z2 is quaternion set
Rea z2 is V28() V29() ext-real Element of REAL
Im1 [*((Rea z) - (Rea z2)),((Im1 z) - (Im1 z2)),((Im2 z) - (Im2 z2)),((Im3 z) - (Im3 z2))*] is V28() V29() ext-real Element of REAL
(Im1 z) + (- (Im1 z2)) is V28() V29() ext-real Element of REAL
Im1 (- z2) is V28() V29() ext-real Element of REAL
(Im1 z) + (Im1 (- z2)) is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
Im3 [*((Rea z) - (Rea z2)),((Im1 z) - (Im1 z2)),((Im2 z) - (Im2 z2)),((Im3 z) - (Im3 z2))*] is V28() V29() ext-real Element of REAL
(Im3 z) + (- (Im3 z2)) is V28() V29() ext-real Element of REAL
Im3 (- z2) is V28() V29() ext-real Element of REAL
(Im3 z) + (Im3 (- z2)) is V28() V29() ext-real Element of REAL
Im3 z2 is V28() V29() ext-real Element of REAL
Im2 [*((Rea z) - (Rea z2)),((Im1 z) - (Im1 z2)),((Im2 z) - (Im2 z2)),((Im3 z) - (Im3 z2))*] is V28() V29() ext-real Element of REAL
(Im2 z) + (- (Im2 z2)) is V28() V29() ext-real Element of REAL
Im2 (- z2) is V28() V29() ext-real Element of REAL
(Im2 z) + (Im2 (- z2)) is V28() V29() ext-real Element of REAL
Im2 z2 is V28() V29() ext-real Element of REAL
z is quaternion set
Rea z is V28() V29() ext-real Element of REAL
z2 is quaternion set
z * z2 is quaternion Element of QUATERNION
Rea z2 is V28() V29() ext-real Element of REAL
(Rea z) * (Rea z2) is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
(Rea z) * (Im1 z2) is V28() V29() ext-real Element of REAL
Im2 z2 is V28() V29() ext-real Element of REAL
(Rea z) * (Im2 z2) is V28() V29() ext-real Element of REAL
Im3 z2 is V28() V29() ext-real Element of REAL
(Rea z) * (Im3 z2) is V28() V29() ext-real Element of REAL
[*((Rea z) * (Rea z2)),((Rea z) * (Im1 z2)),((Rea z) * (Im2 z2)),((Rea z) * (Im3 z2))*] is quaternion Element of QUATERNION
Im3 z is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z) * (Im1 z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2)) is V28() V29() ext-real Element of REAL
K110(((Im1 z) * (Im1 z2))) is V28() set
K108(((Rea z) * (Rea z2)),K110(((Im1 z) * (Im1 z2)))) is set
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z) * (Im2 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2)) is V28() V29() ext-real Element of REAL
K110(((Im2 z) * (Im2 z2))) is V28() set
K108((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))),K110(((Im2 z) * (Im2 z2)))) is set
(Im3 z) * (Im3 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2)) is V28() V29() ext-real Element of REAL
K110(((Im3 z) * (Im3 z2))) is V28() set
K108(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))),K110(((Im3 z) * (Im3 z2)))) is set
(Im1 z) * (Rea z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2)) is V28() V29() ext-real Element of REAL
(Im2 z) * (Im3 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2)) is V28() V29() ext-real Element of REAL
(Im3 z) * (Im2 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2)) is V28() V29() ext-real Element of REAL
K110(((Im3 z) * (Im2 z2))) is V28() set
K108(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))),K110(((Im3 z) * (Im2 z2)))) is set
(Im2 z) * (Rea z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2)) is V28() V29() ext-real Element of REAL
(Im3 z) * (Im1 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2)) is V28() V29() ext-real Element of REAL
(Im1 z) * (Im3 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2)) is V28() V29() ext-real Element of REAL
K110(((Im1 z) * (Im3 z2))) is V28() set
K108(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))),K110(((Im1 z) * (Im3 z2)))) is set
(Im3 z) * (Rea z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2)) is V28() V29() ext-real Element of REAL
(Im1 z) * (Im2 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2)) is V28() V29() ext-real Element of REAL
(Im2 z) * (Im1 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)) is V28() V29() ext-real Element of REAL
K110(((Im2 z) * (Im1 z2))) is V28() set
K108(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))),K110(((Im2 z) * (Im1 z2)))) is set
[*(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2))),(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2))),(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2))),(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)))*] is quaternion Element of QUATERNION
Im1 [*(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2))),(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2))),(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2))),(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)))*] is V28() V29() ext-real Element of REAL
z2 is quaternion set
Im1 z2 is V28() V29() ext-real Element of REAL
Im2 [*(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2))),(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2))),(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2))),(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)))*] is V28() V29() ext-real Element of REAL
Im2 z2 is V28() V29() ext-real Element of REAL
Im3 [*(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2))),(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2))),(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2))),(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)))*] is V28() V29() ext-real Element of REAL
Im3 z2 is V28() V29() ext-real Element of REAL
Rea [*(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2))),(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2))),(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2))),(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)))*] is V28() V29() ext-real Element of REAL
Rea z2 is V28() V29() ext-real Element of REAL
z is quaternion set
z * <i> is quaternion Element of QUATERNION
Rea z is V28() V29() ext-real Element of REAL
[*0,(Rea z),0,0*] is quaternion Element of QUATERNION
z2 is V28() V29() ext-real Element of REAL
Rea (z * <i>) is V28() V29() ext-real Element of REAL
Im1 (z * <i>) is V28() V29() ext-real Element of REAL
Im2 (z * <i>) is V28() V29() ext-real Element of REAL
Im3 (z * <i>) is V28() V29() ext-real Element of REAL
[*(Rea (z * <i>)),(Im1 (z * <i>)),(Im2 (z * <i>)),(Im3 (z * <i>))*] is quaternion Element of QUATERNION
[*0,(Im1 (z * <i>)),(Im2 (z * <i>)),(Im3 (z * <i>))*] is quaternion Element of QUATERNION
[*0,z2,(Im2 (z * <i>)),(Im3 (z * <i>))*] is quaternion Element of QUATERNION
[*0,z2,0,(Im3 (z * <i>))*] is quaternion Element of QUATERNION
z is quaternion set
z * <j> is quaternion Element of QUATERNION
Rea z is V28() V29() ext-real Element of REAL
[*0,0,(Rea z),0*] is quaternion Element of QUATERNION
z2 is V28() V29() ext-real Element of REAL
Rea (z * <j>) is V28() V29() ext-real Element of REAL
Im1 (z * <j>) is V28() V29() ext-real Element of REAL
Im2 (z * <j>) is V28() V29() ext-real Element of REAL
Im3 (z * <j>) is V28() V29() ext-real Element of REAL
[*(Rea (z * <j>)),(Im1 (z * <j>)),(Im2 (z * <j>)),(Im3 (z * <j>))*] is quaternion Element of QUATERNION
[*0,(Im1 (z * <j>)),(Im2 (z * <j>)),(Im3 (z * <j>))*] is quaternion Element of QUATERNION
[*0,0,(Im2 (z * <j>)),(Im3 (z * <j>))*] is quaternion Element of QUATERNION
[*0,0,z2,(Im3 (z * <j>))*] is quaternion Element of QUATERNION
z is quaternion set
z * <k> is quaternion Element of QUATERNION
Rea z is V28() V29() ext-real Element of REAL
[*0,0,0,(Rea z)*] is quaternion Element of QUATERNION
z2 is V28() V29() ext-real Element of REAL
Rea (z * <k>) is V28() V29() ext-real Element of REAL
Im1 (z * <k>) is V28() V29() ext-real Element of REAL
Im2 (z * <k>) is V28() V29() ext-real Element of REAL
Im3 (z * <k>) is V28() V29() ext-real Element of REAL
[*(Rea (z * <k>)),(Im1 (z * <k>)),(Im2 (z * <k>)),(Im3 (z * <k>))*] is quaternion Element of QUATERNION
[*0,(Im1 (z * <k>)),(Im2 (z * <k>)),(Im3 (z * <k>))*] is quaternion Element of QUATERNION
[*0,0,(Im2 (z * <k>)),(Im3 (z * <k>))*] is quaternion Element of QUATERNION
[*0,0,0,(Im3 (z * <k>))*] is quaternion Element of QUATERNION
0q is quaternion Element of QUATERNION
z is quaternion set
z - 0q is quaternion Element of QUATERNION
- 0q is quaternion set
z + (- 0q) is quaternion set
z2 is V28() V29() ext-real Element of REAL
z2 is V28() V29() ext-real Element of REAL
z4 is V28() V29() ext-real Element of REAL
z2 is V28() V29() ext-real Element of REAL
[*z2,z2,z4,z2*] is quaternion Element of QUATERNION
[*0,0*] is V28() Element of COMPLEX
[*0,0,0,0*] is quaternion Element of QUATERNION
- 0q is quaternion Element of QUATERNION
- 0 is V28() V29() ext-real Element of REAL
[*(- 0),(- 0),(- 0),(- 0)*] is quaternion Element of QUATERNION
z2 + (- 0) is V28() V29() ext-real Element of REAL
z2 + (- 0) is V28() V29() ext-real Element of REAL
z4 + (- 0) is V28() V29() ext-real Element of REAL
z2 + (- 0) is V28() V29() ext-real Element of REAL
[*(z2 + (- 0)),(z2 + (- 0)),(z4 + (- 0)),(z2 + (- 0))*] is quaternion Element of QUATERNION
z is quaternion set
z2 is quaternion set
z * z2 is quaternion Element of QUATERNION
z2 * z is quaternion Element of QUATERNION
Im3 z is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
Rea z2 is V28() V29() ext-real Element of REAL
Rea z is V28() V29() ext-real Element of REAL
(Rea z2) * (Rea z) is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
(Im1 z2) * (Im1 z) is V28() V29() ext-real Element of REAL
((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z)) is V28() V29() ext-real Element of REAL
K110(((Im1 z2) * (Im1 z))) is V28() set
K108(((Rea z2) * (Rea z)),K110(((Im1 z2) * (Im1 z)))) is set
Im2 z2 is V28() V29() ext-real Element of REAL
(Im2 z2) * (Im2 z) is V28() V29() ext-real Element of REAL
(((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z)) is V28() V29() ext-real Element of REAL
K110(((Im2 z2) * (Im2 z))) is V28() set
K108((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))),K110(((Im2 z2) * (Im2 z)))) is set
Im3 z2 is V28() V29() ext-real Element of REAL
(Im3 z2) * (Im3 z) is V28() V29() ext-real Element of REAL
((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))) - ((Im3 z2) * (Im3 z)) is V28() V29() ext-real Element of REAL
K110(((Im3 z2) * (Im3 z))) is V28() set
K108(((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))),K110(((Im3 z2) * (Im3 z)))) is set
(Rea z2) * (Im1 z) is V28() V29() ext-real Element of REAL
(Im1 z2) * (Rea z) is V28() V29() ext-real Element of REAL
((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z)) is V28() V29() ext-real Element of REAL
(Im2 z2) * (Im3 z) is V28() V29() ext-real Element of REAL
(((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z)) is V28() V29() ext-real Element of REAL
(Im3 z2) * (Im2 z) is V28() V29() ext-real Element of REAL
((((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z))) - ((Im3 z2) * (Im2 z)) is V28() V29() ext-real Element of REAL
K110(((Im3 z2) * (Im2 z))) is V28() set
K108(((((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z))),K110(((Im3 z2) * (Im2 z)))) is set
(((((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z))) - ((Im3 z2) * (Im2 z))) * <i> is quaternion set
(((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))) - ((Im3 z2) * (Im3 z))) + ((((((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z))) - ((Im3 z2) * (Im2 z))) * <i>) is quaternion set
(Rea z2) * (Im2 z) is V28() V29() ext-real Element of REAL
(Im2 z2) * (Rea z) is V28() V29() ext-real Element of REAL
((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z)) is V28() V29() ext-real Element of REAL
(Im3 z2) * (Im1 z) is V28() V29() ext-real Element of REAL
(((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z))) + ((Im3 z2) * (Im1 z)) is V28() V29() ext-real Element of REAL
(Im1 z2) * (Im3 z) is V28() V29() ext-real Element of REAL
((((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z))) + ((Im3 z2) * (Im1 z))) - ((Im1 z2) * (Im3 z)) is V28() V29() ext-real Element of REAL
K110(((Im1 z2) * (Im3 z))) is V28() set
K108(((((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z))) + ((Im3 z2) * (Im1 z))),K110(((Im1 z2) * (Im3 z)))) is set
(((((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z))) + ((Im3 z2) * (Im1 z))) - ((Im1 z2) * (Im3 z))) * <j> is quaternion set
((((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))) - ((Im3 z2) * (Im3 z))) + ((((((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z))) - ((Im3 z2) * (Im2 z))) * <i>)) + ((((((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z))) + ((Im3 z2) * (Im1 z))) - ((Im1 z2) * (Im3 z))) * <j>) is quaternion Element of QUATERNION
(Rea z2) * (Im3 z) is V28() V29() ext-real Element of REAL
(Im3 z2) * (Rea z) is V28() V29() ext-real Element of REAL
((Rea z2) * (Im3 z)) + ((Im3 z2) * (Rea z)) is V28() V29() ext-real Element of REAL
(Im1 z2) * (Im2 z) is V28() V29() ext-real Element of REAL
(((Rea z2) * (Im3 z)) + ((Im3 z2) * (Rea z))) + ((Im1 z2) * (Im2 z)) is V28() V29() ext-real Element of REAL
(Im2 z2) * (Im1 z) is V28() V29() ext-real Element of REAL
((((Rea z2) * (Im3 z)) + ((Im3 z2) * (Rea z))) + ((Im1 z2) * (Im2 z))) - ((Im2 z2) * (Im1 z)) is V28() V29() ext-real Element of REAL
K110(((Im2 z2) * (Im1 z))) is V28() set
K108(((((Rea z2) * (Im3 z)) + ((Im3 z2) * (Rea z))) + ((Im1 z2) * (Im2 z))),K110(((Im2 z2) * (Im1 z)))) is set
(((((Rea z2) * (Im3 z)) + ((Im3 z2) * (Rea z))) + ((Im1 z2) * (Im2 z))) - ((Im2 z2) * (Im1 z))) * <k> is quaternion set
(((((((Rea z2) * (Rea z)) - ((Im1 z2) * (Im1 z))) - ((Im2 z2) * (Im2 z))) - ((Im3 z2) * (Im3 z))) + ((((((Rea z2) * (Im1 z)) + ((Im1 z2) * (Rea z))) + ((Im2 z2) * (Im3 z))) - ((Im3 z2) * (Im2 z))) * <i>)) + ((((((Rea z2) * (Im2 z)) + ((Im2 z2) * (Rea z))) + ((Im3 z2) * (Im1 z))) - ((Im1 z2) * (Im3 z))) * <j>)) + ((((((Rea z2) * (Im3 z)) + ((Im3 z2) * (Rea z))) + ((Im1 z2) * (Im2 z))) - ((Im2 z2) * (Im1 z))) * <k>) is quaternion Element of QUATERNION
z is quaternion set
Im1 z is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
Im3 z is V28() V29() ext-real Element of REAL
Rea z is V28() V29() ext-real Element of REAL
[*(Rea z),0,0,0*] is quaternion Element of QUATERNION
[*(Rea z),0*] is V28() Element of COMPLEX
z is quaternion set
|.z.| is V28() V29() ext-real Element of REAL
Rea z is V28() V29() ext-real Element of REAL
(Rea z) ^2 is V28() V29() ext-real Element of REAL
K109((Rea z),(Rea z)) is set
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 z),(Im1 z)) is set
((Rea z) ^2) + ((Im1 z) ^2) is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 z),(Im2 z)) is set
(((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2) is V28() V29() ext-real Element of REAL
Im3 z is V28() V29() ext-real Element of REAL
(Im3 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 z),(Im3 z)) is set
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) is V28() V29() ext-real Element of REAL
|.z.| ^2 is V28() V29() ext-real Element of REAL
K109(|.z.|,|.z.|) is set
(((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) ^2 is V28() V29() ext-real Element of REAL
K109((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)),(((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2))) is set
sqrt ((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) ^2) is V28() V29() ext-real Element of REAL
z is quaternion set
|.z.| is V28() V29() ext-real Element of REAL
Rea z is V28() V29() ext-real Element of REAL
(Rea z) ^2 is V28() V29() ext-real Element of REAL
K109((Rea z),(Rea z)) is set
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 z),(Im1 z)) is set
((Rea z) ^2) + ((Im1 z) ^2) is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 z),(Im2 z)) is set
(((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2) is V28() V29() ext-real Element of REAL
Im3 z is V28() V29() ext-real Element of REAL
(Im3 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 z),(Im3 z)) is set
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) is V28() V29() ext-real Element of REAL
|.z.| ^2 is V28() V29() ext-real Element of REAL
K109(|.z.|,|.z.|) is set
z *' is quaternion Element of QUATERNION
- (Im1 z) is V28() V29() ext-real Element of REAL
(- (Im1 z)) * K107() is quaternion set
(Rea z) + ((- (Im1 z)) * K107()) is quaternion set
- (Im2 z) is V28() V29() ext-real Element of REAL
(- (Im2 z)) * <j> is quaternion set
((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>) is quaternion Element of QUATERNION
- (Im3 z) is V28() V29() ext-real Element of REAL
(- (Im3 z)) * <k> is quaternion set
(((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) is quaternion Element of QUATERNION
z * (z *') is quaternion Element of QUATERNION
|.(z * (z *')).| is V28() V29() ext-real Element of REAL
Rea (z * (z *')) is V28() V29() ext-real Element of REAL
(Rea (z * (z *'))) ^2 is V28() V29() ext-real Element of REAL
K109((Rea (z * (z *'))),(Rea (z * (z *')))) is set
Im1 (z * (z *')) is V28() V29() ext-real Element of REAL
(Im1 (z * (z *'))) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 (z * (z *'))),(Im1 (z * (z *')))) is set
((Rea (z * (z *'))) ^2) + ((Im1 (z * (z *'))) ^2) is V28() V29() ext-real Element of REAL
Im2 (z * (z *')) is V28() V29() ext-real Element of REAL
(Im2 (z * (z *'))) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 (z * (z *'))),(Im2 (z * (z *')))) is set
(((Rea (z * (z *'))) ^2) + ((Im1 (z * (z *'))) ^2)) + ((Im2 (z * (z *'))) ^2) is V28() V29() ext-real Element of REAL
Im3 (z * (z *')) is V28() V29() ext-real Element of REAL
(Im3 (z * (z *'))) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 (z * (z *'))),(Im3 (z * (z *')))) is set
((((Rea (z * (z *'))) ^2) + ((Im1 (z * (z *'))) ^2)) + ((Im2 (z * (z *'))) ^2)) + ((Im3 (z * (z *'))) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea (z * (z *'))) ^2) + ((Im1 (z * (z *'))) ^2)) + ((Im2 (z * (z *'))) ^2)) + ((Im3 (z * (z *'))) ^2)) is V28() V29() ext-real Element of REAL
z * z is quaternion Element of QUATERNION
|.(z * z).| is V28() V29() ext-real Element of REAL
Rea (z * z) is V28() V29() ext-real Element of REAL
(Rea (z * z)) ^2 is V28() V29() ext-real Element of REAL
K109((Rea (z * z)),(Rea (z * z))) is set
Im1 (z * z) is V28() V29() ext-real Element of REAL
(Im1 (z * z)) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 (z * z)),(Im1 (z * z))) is set
((Rea (z * z)) ^2) + ((Im1 (z * z)) ^2) is V28() V29() ext-real Element of REAL
Im2 (z * z) is V28() V29() ext-real Element of REAL
(Im2 (z * z)) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 (z * z)),(Im2 (z * z))) is set
(((Rea (z * z)) ^2) + ((Im1 (z * z)) ^2)) + ((Im2 (z * z)) ^2) is V28() V29() ext-real Element of REAL
Im3 (z * z) is V28() V29() ext-real Element of REAL
(Im3 (z * z)) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 (z * z)),(Im3 (z * z))) is set
((((Rea (z * z)) ^2) + ((Im1 (z * z)) ^2)) + ((Im2 (z * z)) ^2)) + ((Im3 (z * z)) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea (z * z)) ^2) + ((Im1 (z * z)) ^2)) + ((Im2 (z * z)) ^2)) + ((Im3 (z * z)) ^2)) is V28() V29() ext-real Element of REAL
z is quaternion set
|.z.| is V28() V29() ext-real Element of REAL
Rea z is V28() V29() ext-real Element of REAL
(Rea z) ^2 is V28() V29() ext-real Element of REAL
K109((Rea z),(Rea z)) is set
Im1 z is V28() V29() ext-real Element of REAL
(Im1 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im1 z),(Im1 z)) is set
((Rea z) ^2) + ((Im1 z) ^2) is V28() V29() ext-real Element of REAL
Im2 z is V28() V29() ext-real Element of REAL
(Im2 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im2 z),(Im2 z)) is set
(((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2) is V28() V29() ext-real Element of REAL
Im3 z is V28() V29() ext-real Element of REAL
(Im3 z) ^2 is V28() V29() ext-real Element of REAL
K109((Im3 z),(Im3 z)) is set
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) is V28() V29() ext-real Element of REAL
sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) is V28() V29() ext-real Element of REAL
|.z.| ^2 is V28() V29() ext-real Element of REAL
K109(|.z.|,|.z.|) is set
z *' is quaternion Element of QUATERNION
- (Im1 z) is V28() V29() ext-real Element of REAL
(- (Im1 z)) * K107() is quaternion set
(Rea z) + ((- (Im1 z)) * K107()) is quaternion set
- (Im2 z) is V28() V29() ext-real Element of REAL
(- (Im2 z)) * <j> is quaternion set
((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>) is quaternion Element of QUATERNION
- (Im3 z) is V28() V29() ext-real Element of REAL
(- (Im3 z)) * <k> is quaternion set
(((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) is quaternion Element of QUATERNION
z * (z *') is quaternion Element of QUATERNION
Rea (z * (z *')) is V28() V29() ext-real Element of REAL
z is quaternion set
Rea z is V28() V29() ext-real Element of REAL
2 * (Rea z) is V28() V29() ext-real Element of REAL
z *' is quaternion Element of QUATERNION
Im1 z is V28() V29() ext-real Element of REAL
- (Im1 z) is V28() V29() ext-real Element of REAL
(- (Im1 z)) * K107() is quaternion set
(Rea z) + ((- (Im1 z)) * K107()) is quaternion set
Im2 z is V28() V29() ext-real Element of REAL
- (Im2 z) is V28() V29() ext-real Element of REAL
(- (Im2 z)) * <j> is quaternion set
((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>) is quaternion Element of QUATERNION
Im3 z is V28() V29() ext-real Element of REAL
- (Im3 z) is V28() V29() ext-real Element of REAL
(- (Im3 z)) * <k> is quaternion set
(((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) is quaternion Element of QUATERNION
z + (z *') is quaternion Element of QUATERNION
Rea (z + (z *')) is V28() V29() ext-real Element of REAL
[*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] is quaternion Element of QUATERNION
[*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] is quaternion Element of QUATERNION
(Rea z) + (Rea z) is V28() V29() ext-real Element of REAL
(Im1 z) + (- (Im1 z)) is V28() V29() ext-real Element of REAL
(Im2 z) + (- (Im2 z)) is V28() V29() ext-real Element of REAL
(Im3 z) + (- (Im3 z)) is V28() V29() ext-real Element of REAL
[*((Rea z) + (Rea z)),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] is quaternion Element of QUATERNION
[*(2 * (Rea z)),0,0,0*] is quaternion Element of QUATERNION
z is quaternion set
z *' is quaternion Element of QUATERNION
Rea z is V28() V29() ext-real Element of REAL
Im1 z is V28() V29() ext-real Element of REAL
- (Im1 z) is V28() V29() ext-real Element of REAL
(- (Im1 z)) * K107() is quaternion set
(Rea z) + ((- (Im1 z)) * K107()) is quaternion set
Im2 z is V28() V29() ext-real Element of REAL
- (Im2 z) is V28() V29() ext-real Element of REAL
(- (Im2 z)) * <j> is quaternion set
((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>) is quaternion Element of QUATERNION
Im3 z is V28() V29() ext-real Element of REAL
- (Im3 z) is V28() V29() ext-real Element of REAL
(- (Im3 z)) * <k> is quaternion set
(((Rea z) + ((- (Im1 z)) * K107())) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) is quaternion Element of QUATERNION
z2 is quaternion set
z * z2 is quaternion Element of QUATERNION
(z * z2) *' is quaternion Element of QUATERNION
Rea (z * z2) is V28() V29() ext-real Element of REAL
Im1 (z * z2) is V28() V29() ext-real Element of REAL
- (Im1 (z * z2)) is V28() V29() ext-real Element of REAL
(- (Im1 (z * z2))) * K107() is quaternion set
(Rea (z * z2)) + ((- (Im1 (z * z2))) * K107()) is quaternion set
Im2 (z * z2) is V28() V29() ext-real Element of REAL
- (Im2 (z * z2)) is V28() V29() ext-real Element of REAL
(- (Im2 (z * z2))) * <j> is quaternion set
((Rea (z * z2)) + ((- (Im1 (z * z2))) * K107())) + ((- (Im2 (z * z2))) * <j>) is quaternion Element of QUATERNION
Im3 (z * z2) is V28() V29() ext-real Element of REAL
- (Im3 (z * z2)) is V28() V29() ext-real Element of REAL
(- (Im3 (z * z2))) * <k> is quaternion set
(((Rea (z * z2)) + ((- (Im1 (z * z2))) * K107())) + ((- (Im2 (z * z2))) * <j>)) + ((- (Im3 (z * z2))) * <k>) is quaternion Element of QUATERNION
z2 *' is quaternion Element of QUATERNION
Rea z2 is V28() V29() ext-real Element of REAL
Im1 z2 is V28() V29() ext-real Element of REAL
- (Im1 z2) is V28() V29() ext-real Element of REAL
(- (Im1 z2)) * K107() is quaternion set
(Rea z2) + ((- (Im1 z2)) * K107()) is quaternion set
Im2 z2 is V28() V29() ext-real Element of REAL
- (Im2 z2) is V28() V29() ext-real Element of REAL
(- (Im2 z2)) * <j> is quaternion set
((Rea z2) + ((- (Im1 z2)) * K107())) + ((- (Im2 z2)) * <j>) is quaternion Element of QUATERNION
Im3 z2 is V28() V29() ext-real Element of REAL
- (Im3 z2) is V28() V29() ext-real Element of REAL
(- (Im3 z2)) * <k> is quaternion set
(((Rea z2) + ((- (Im1 z2)) * K107())) + ((- (Im2 z2)) * <j>)) + ((- (Im3 z2)) * <k>) is quaternion Element of QUATERNION
(z *') * (z2 *') is quaternion Element of QUATERNION
Im1 (z2 *') is V28() V29() ext-real Element of REAL
Im2 (z2 *') is V28() V29() ext-real Element of REAL
Im3 (z2 *') is V28() V29() ext-real Element of REAL
Rea (z *') is V28() V29() ext-real Element of REAL
(Rea z) * (Rea z2) is V28() V29() ext-real Element of REAL
(Im1 z) * (Im1 z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2)) is V28() V29() ext-real Element of REAL
K110(((Im1 z) * (Im1 z2))) is V28() set
K108(((Rea z) * (Rea z2)),K110(((Im1 z) * (Im1 z2)))) is set
(Im2 z) * (Im2 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2)) is V28() V29() ext-real Element of REAL
K110(((Im2 z) * (Im2 z2))) is V28() set
K108((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))),K110(((Im2 z) * (Im2 z2)))) is set
(Im3 z) * (Im3 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))) - ((Im3 z) * (Im3 z2)) is V28() V29() ext-real Element of REAL
K110(((Im3 z) * (Im3 z2))) is V28() set
K108(((((Rea z) * (Rea z2)) - ((Im1 z) * (Im1 z2))) - ((Im2 z) * (Im2 z2))),K110(((Im3 z) * (Im3 z2)))) is set
Im3 (z *') is V28() V29() ext-real Element of REAL
Im1 (z *') is V28() V29() ext-real Element of REAL
Im2 (z *') is V28() V29() ext-real Element of REAL
(Rea z) * (Im3 z2) is V28() V29() ext-real Element of REAL
(Im3 z) * (Rea z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2)) is V28() V29() ext-real Element of REAL
(Im1 z) * (Im2 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2)) is V28() V29() ext-real Element of REAL
(Im2 z) * (Im1 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))) - ((Im2 z) * (Im1 z2)) is V28() V29() ext-real Element of REAL
K110(((Im2 z) * (Im1 z2))) is V28() set
K108(((((Rea z) * (Im3 z2)) + ((Im3 z) * (Rea z2))) + ((Im1 z) * (Im2 z2))),K110(((Im2 z) * (Im1 z2)))) is set
(Rea z) * (Im2 z2) is V28() V29() ext-real Element of REAL
(Im2 z) * (Rea z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2)) is V28() V29() ext-real Element of REAL
(Im3 z) * (Im1 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2)) is V28() V29() ext-real Element of REAL
(Im1 z) * (Im3 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))) - ((Im1 z) * (Im3 z2)) is V28() V29() ext-real Element of REAL
K110(((Im1 z) * (Im3 z2))) is V28() set
K108(((((Rea z) * (Im2 z2)) + ((Im2 z) * (Rea z2))) + ((Im3 z) * (Im1 z2))),K110(((Im1 z) * (Im3 z2)))) is set
(Rea z) * (Im1 z2) is V28() V29() ext-real Element of REAL
(Im1 z) * (Rea z2) is V28() V29() ext-real Element of REAL
((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2)) is V28() V29() ext-real Element of REAL
(Im2 z) * (Im3 z2) is V28() V29() ext-real Element of REAL
(((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2)) is V28() V29() ext-real Element of REAL
(Im3 z) * (Im2 z2) is V28() V29() ext-real Element of REAL
((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))) - ((Im3 z) * (Im2 z2)) is V28() V29() ext-real Element of REAL
K110(((Im3 z) * (Im2 z2))) is V28() set
K108(((((Rea z) * (Im1 z2)) + ((Im1 z) * (Rea z2))) + ((Im2 z) * (Im3 z2))),K110(((Im3 z) * (Im2 z2)))) is set
Rea (z2 *') is V28() V29() ext-real Element of REAL
(Rea (z *')) * (Rea (z2 *')) is V28() V29() ext-real Element of REAL
(Im1 (z *')) * (Im1 (z2 *')) is V28() V29() ext-real Element of REAL
((Rea (z *')) * (Rea (z2 *'))) - ((Im1 (z *')) * (Im1 (z2 *'))) is V28() V29() ext-real Element of REAL
K110(((Im1 (z *')) * (Im1 (z2 *')))) is V28() set
K108(((Rea (z *')) * (Rea (z2 *'))),K110(((Im1 (z *')) * (Im1 (z2 *'))))) is set
(Im2 (z *')) * (Im2 (z2 *')) is V28() V29() ext-real Element of REAL
(((Rea (z *')) * (Rea (z2 *'))) - ((Im1 (z *')) * (Im1 (z2 *')))) - ((Im2 (z *')) * (Im2 (z2 *'))) is V28() V29() ext-real Element of REAL
K110(((Im2 (z *')) * (Im2 (z2 *')))) is V28() set
K108((((Rea (z *')) * (Rea (z2 *'))) - ((Im1 (z *')) * (Im1 (z2 *')))),K110(((Im2 (z *')) * (Im2 (z2 *'))))) is set
(Im3 (z *')) * (Im3 (z2 *')) is V28() V29() ext-real Element of REAL
((((Rea (z *')) * (Rea (z2 *'))) - ((Im1 (z *')) * (Im1 (z2 *')))) - ((Im2 (z *')) * (Im2 (z2 *')))) - ((Im3 (z *')) * (Im3 (z2 *'))) is V28() V29() ext-real Element of REAL
K110(((Im3 (z *')) * (Im3 (z2 *')))) is V28() set
K108(((((Rea (z *')) * (Rea (z2 *'))) - ((Im1 (z *')) * (Im1 (z2 *')))) - ((Im2 (z *')) * (Im2 (z2 *')))),K110(((Im3 (z *')) * (Im3 (z2 *'))))) is set
(Rea (z *')) * (Im1 (z2 *')) is V28() V29() ext-real Element of REAL
(Im1 (z *')) * (Rea (z2 *')) is V28() V29() ext-real Element of REAL
((Rea (z *')) * (Im1 (z2 *'))) + ((Im1 (z *')) * (Rea (z2 *'))) is V28() V29() ext-real Element of REAL
(Im2 (z *')) * (Im3 (z2 *')) is V28() V29() ext-real Element of REAL
(((Rea (z *')) * (Im1 (z2 *'))) + ((Im1 (z *')) * (Rea (z2 *')))) + ((Im2 (z *')) * (Im3 (z2 *'))) is V28() V29() ext-real Element of REAL
(Im3 (z *')) * (Im2 (z2 *')) is V28() V29() ext-real Element of REAL
((((Rea (z *')) * (Im1 (z2 *'))) + ((Im1 (z *')) * (Rea (z2 *')))) + ((Im2 (z *')) * (Im3 (z2 *')))) - ((Im3 (z *')) * (Im2 (z2 *'))) is V28() V29() ext-real Element of REAL
K110(((Im3 (z *')) * (Im2 (z2 *')))) is V28() set
K108(((((Rea (z *')) * (Im1 (z2 *'))) + ((Im1 (z *')) * (Rea (z2 *')))) + ((Im2 (z *')) * (Im3 (z2 *')))),K110(((Im3 (z *')) * (Im2 (z2 *'))))) is set
(((((Rea (z *')) * (Im1 (z2 *'))) + ((Im1 (z *')) * (Rea (z2 *')))) + ((Im2 (z *')) * (Im3 (z2 *')))) - ((Im3 (z *')) * (Im2 (z2 *')))) * <i> is quaternion set
(((((Rea (z *')) * (Rea (z2 *'))) - ((Im1 (z *')) * (Im1 (z2 *')))) - ((Im2 (z *')) * (Im2 (z2 *')))) - ((Im3 (z *')) * (Im3 (z2 *')))) + ((((((Rea (z *')) * (Im1 (z2 *'))) + ((Im1 (z *')) * (Rea (z2 *')))) + ((Im2 (z *')) * (Im3 (z2 *')))) - ((Im3 (z *')) * (Im2 (z2 *')))) * <i>) is quaternion set
(Rea (z *')) * (Im2 (z2 *')) is V28() V29() ext-real Element of REAL
(Im2 (z *')) * (Rea (z2 *')) is V28() V29() ext-real Element of REAL
((Rea (z *')) * (Im2 (z2 *'))) + ((Im2 (z *')) * (Rea (z2 *'))) is V28() V29() ext-real Element of REAL
(Im3 (z *')) * (Im1 (z2 *')) is V28() V29() ext-real Element of REAL
(((Rea (z *')) * (Im2 (z2 *'))) + ((Im2 (z *')) * (Rea (z2 *')))) + ((Im3 (z *')) * (Im1 (z2 *'))) is V28() V29() ext-real Element of REAL
(Im1 (z *')) * (Im3 (z2 *')) is V28() V29() ext-real Element of REAL<