Beginning of Section SurQuaternions
Definition. We define
CSNo_pair to be
pair_tag {3} of type
set → set → set.
Axiom. (
CSNo_pair_0) We take the following as an axiom:
Definition. We define
HSNo to be
CD_carr {3} CSNo of type
set → prop.
Axiom. (
HSNo_I) We take the following as an axiom:
Axiom. (
HSNo_E) We take the following as an axiom:
Axiom. (
CSNo_HSNo) We take the following as an axiom:
Axiom. (
HSNo_0) We take the following as an axiom:
Axiom. (
HSNo_1) We take the following as an axiom:
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {3}
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_CSNo.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj_CSNo.
Let i ≝ Complex_i
Definition. We define
HSNo_proj0 to be
CD_proj0 {3} CSNo of type
set → set.
Definition. We define
HSNo_proj1 to be
CD_proj1 {3} CSNo of type
set → set.
Axiom. (
HSNo_proj0_1) We take the following as an axiom:
∀z, HSNo z → CSNo (p0 z) ∧ ∃y, CSNo y ∧ z = pa (p0 z) y
Axiom. (
HSNo_proj0_2) We take the following as an axiom:
∀x y, CSNo x → CSNo y → p0 (pa x y) = x
Axiom. (
HSNo_proj1_1) We take the following as an axiom:
∀z, HSNo z → CSNo (p1 z) ∧ z = pa (p0 z) (p1 z)
Axiom. (
HSNo_proj1_2) We take the following as an axiom:
∀x y, CSNo x → CSNo y → p1 (pa x y) = y
Axiom. (
HSNo_proj0R) We take the following as an axiom:
Axiom. (
HSNo_proj1R) We take the following as an axiom:
Axiom. (
HSNo_proj0p1) We take the following as an axiom:
∀z, HSNo z → z = pa (p0 z) (p1 z)
Definition. We define
HSNoLev to be
λz ⇒ CSNoLev (p0 z) ∪ CSNoLev (p1 z) of type
set → set.
Definition. We define
minus_HSNo to be
CD_minus {3} CSNo minus_CSNo of type
set → set.
Definition. We define
conj_HSNo to be
CD_conj {3} CSNo minus_CSNo conj_CSNo of type
set → set.
Definition. We define
add_HSNo to be
CD_add {3} CSNo add_CSNo of type
set → set → set.
Definition. We define
mul_HSNo to be
CD_mul {3} CSNo minus_CSNo conj_CSNo add_CSNo mul_CSNo of type
set → set → set.
Definition. We define
exp_HSNo_nat to be
CD_exp_nat {3} CSNo minus_CSNo conj_CSNo add_CSNo mul_CSNo of type
set → set → set.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_HSNo.
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
conj_HSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_HSNo.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_HSNo.
Notation. We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_HSNo_nat.
Axiom. (
CSNo_HSNo_proj0) We take the following as an axiom:
∀x, CSNo x → p0 x = x
Axiom. (
CSNo_HSNo_proj1) We take the following as an axiom:
∀x, CSNo x → p1 x = 0
Axiom. (
HSNo_p0_0) We take the following as an axiom:
p0 0 = 0
Axiom. (
HSNo_p1_0) We take the following as an axiom:
p1 0 = 0
Axiom. (
HSNo_p0_1) We take the following as an axiom:
p0 1 = 1
Axiom. (
HSNo_p1_1) We take the following as an axiom:
p1 1 = 0
Axiom. (
HSNo_p0_i) We take the following as an axiom:
p0 i = i
Axiom. (
HSNo_p1_i) We take the following as an axiom:
p1 i = 0
Axiom. (
HSNo_p0_j) We take the following as an axiom:
p0 j = 0
Axiom. (
HSNo_p1_j) We take the following as an axiom:
p1 j = 1
Axiom. (
HSNo_p0_k) We take the following as an axiom:
p0 k = 0
Axiom. (
HSNo_p1_k) We take the following as an axiom:
p1 k = i
Axiom. (
conj_HSNo_0) We take the following as an axiom:
Axiom. (
conj_HSNo_1) We take the following as an axiom:
Axiom. (
add_HSNo_add_CSNo) We take the following as an axiom:
∀x y, CSNo x → CSNo y → x + y = x + y
Axiom. (
mul_HSNo_mul_CSNo) We take the following as an axiom:
∀x y, CSNo x → CSNo y → x ⨯ y = x * y
Axiom. (
add_HSNo_0L) We take the following as an axiom:
Axiom. (
add_HSNo_0R) We take the following as an axiom:
Axiom. (
mul_HSNo_0R) We take the following as an axiom:
Axiom. (
mul_HSNo_0L) We take the following as an axiom:
Axiom. (
mul_HSNo_1R) We take the following as an axiom:
Axiom. (
mul_HSNo_1L) We take the following as an axiom:
Axiom. (
exp_HSNo_nat_S) We take the following as an axiom:
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
Axiom. (
add_CSNo_com_3b_1_2) We take the following as an axiom:
∀x y z, CSNo x → CSNo y → CSNo z → (x + y) + z = (x + z) + y
Axiom. (
add_CSNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, CSNo x → CSNo y → CSNo z → CSNo w → (x + y) + (z + w) = (x + z) + (y + w)
Axiom. (
add_CSNo_rotate_4_0312) We take the following as an axiom:
∀x y z w, CSNo x → CSNo y → CSNo z → CSNo w → (x + y) + (z + w) = (x + w) + (y + z)
Axiom. (
add_CSNo_rotate_3_1) We take the following as an axiom:
∀x y z, CSNo x → CSNo y → CSNo z → x + y + z = z + x + y
Axiom. (
mul_CSNo_rotate_3_1) We take the following as an axiom:
∀x y z, CSNo x → CSNo y → CSNo z → x * y * z = z * x * y
Axiom. (
conj_HSNo_i) We take the following as an axiom:
Axiom. (
conj_HSNo_j) We take the following as an axiom:
Axiom. (
conj_HSNo_k) We take the following as an axiom:
End of Section SurQuaternions
Beginning of Section Quaternions
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_HSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_HSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_HSNo.
Let i ≝ Complex_i
Definition. We define
quaternion to be
{pa (u 0) (u 1)|u ∈ complex ⨯ complex} of type
set.
Axiom. (
quaternion_E) We take the following as an axiom:
∀z ∈ quaternion, ∀p : prop, (∀x y ∈ complex, z = pa x y → p) → p
Axiom. (
quaternion_p0_eq) We take the following as an axiom:
∀x y ∈ complex, p0 (pa x y) = x
Axiom. (
quaternion_p1_eq) We take the following as an axiom:
∀x y ∈ complex, p1 (pa x y) = y
End of Section Quaternions