Beginning of Section SurOctonions
Definition. We define
HSNo_pair to be
pair_tag {4} of type
set → set → set.
Axiom. (
HSNo_pair_0) We take the following as an axiom:
Definition. We define
OSNo to be
CD_carr {4} HSNo of type
set → prop.
Axiom. (
OSNo_I) We take the following as an axiom:
Axiom. (
OSNo_E) We take the following as an axiom:
Axiom. (
HSNo_OSNo) We take the following as an axiom:
Axiom. (
OSNo_0) We take the following as an axiom:
Axiom. (
OSNo_1) We take the following as an axiom:
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {4}
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_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 353 and no associativity corresponding to applying term
div_HSNo.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj_HSNo.
Let i ≝ Complex_i
Let j ≝ Quaternion_j
Let k ≝ Quaternion_k
Definition. We define
OSNo_proj0 to be
CD_proj0 {4} HSNo of type
set → set.
Definition. We define
OSNo_proj1 to be
CD_proj1 {4} HSNo of type
set → set.
Axiom. (
OSNo_proj0_1) We take the following as an axiom:
∀z, OSNo z → HSNo (p0 z) ∧ ∃y, HSNo y ∧ z = pa (p0 z) y
Axiom. (
OSNo_proj0_2) We take the following as an axiom:
∀x y, HSNo x → HSNo y → p0 (pa x y) = x
Axiom. (
OSNo_proj1_1) We take the following as an axiom:
∀z, OSNo z → HSNo (p1 z) ∧ z = pa (p0 z) (p1 z)
Axiom. (
OSNo_proj1_2) We take the following as an axiom:
∀x y, HSNo x → HSNo y → p1 (pa x y) = y
Axiom. (
OSNo_proj0R) We take the following as an axiom:
Axiom. (
OSNo_proj1R) We take the following as an axiom:
Axiom. (
OSNo_proj0p1) We take the following as an axiom:
∀z, OSNo z → z = pa (p0 z) (p1 z)
Definition. We define
OSNoLev to be
λz ⇒ HSNoLev (p0 z) ∪ HSNoLev (p1 z) of type
set → set.
Definition. We define
minus_OSNo to be
CD_minus {4} HSNo minus_HSNo of type
set → set.
Definition. We define
conj_OSNo to be
CD_conj {4} HSNo minus_HSNo conj_HSNo of type
set → set.
Definition. We define
add_OSNo to be
CD_add {4} HSNo add_HSNo of type
set → set → set.
Definition. We define
mul_OSNo to be
CD_mul {4} HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo of type
set → set → set.
Definition. We define
exp_OSNo_nat to be
CD_exp_nat {4} HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo of type
set → set → set.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_OSNo.
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
conj_OSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_OSNo.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_OSNo.
Notation. We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_OSNo_nat.
Axiom. (
HSNo_OSNo_proj0) We take the following as an axiom:
∀x, HSNo x → p0 x = x
Axiom. (
HSNo_OSNo_proj1) We take the following as an axiom:
∀x, HSNo x → p1 x = 0
Axiom. (
OSNo_p0_0) We take the following as an axiom:
p0 0 = 0
Axiom. (
OSNo_p1_0) We take the following as an axiom:
p1 0 = 0
Axiom. (
OSNo_p0_1) We take the following as an axiom:
p0 1 = 1
Axiom. (
OSNo_p1_1) We take the following as an axiom:
p1 1 = 0
Axiom. (
OSNo_p0_i) We take the following as an axiom:
p0 i = i
Axiom. (
OSNo_p1_i) We take the following as an axiom:
p1 i = 0
Axiom. (
OSNo_p0_j) We take the following as an axiom:
p0 j = j
Axiom. (
OSNo_p1_j) We take the following as an axiom:
p1 j = 0
Axiom. (
OSNo_p0_k) We take the following as an axiom:
p0 k = k
Axiom. (
OSNo_p1_k) We take the following as an axiom:
p1 k = 0
Axiom. (
conj_OSNo_0) We take the following as an axiom:
Axiom. (
conj_OSNo_1) We take the following as an axiom:
Axiom. (
add_OSNo_add_HSNo) We take the following as an axiom:
∀x y, HSNo x → HSNo y → x + y = x + y
Axiom. (
mul_OSNo_mul_HSNo) We take the following as an axiom:
∀x y, HSNo x → HSNo y → x ⨯ y = x * y
Axiom. (
add_OSNo_0L) We take the following as an axiom:
Axiom. (
add_OSNo_0R) We take the following as an axiom:
Axiom. (
mul_OSNo_0R) We take the following as an axiom:
Axiom. (
mul_OSNo_0L) We take the following as an axiom:
Axiom. (
mul_OSNo_1R) We take the following as an axiom:
Axiom. (
mul_OSNo_1L) We take the following as an axiom:
Axiom. (
exp_OSNo_nat_S) We take the following as an axiom:
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
Axiom. (
add_HSNo_com_3b_1_2) We take the following as an axiom:
∀x y z, HSNo x → HSNo y → HSNo z → (x + y) + z = (x + z) + y
Axiom. (
add_HSNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, HSNo x → HSNo y → HSNo z → HSNo w → (x + y) + (z + w) = (x + z) + (y + w)
Axiom. (
add_HSNo_rotate_4_0312) We take the following as an axiom:
∀x y z w, HSNo x → HSNo y → HSNo z → HSNo w → (x + y) + (z + w) = (x + w) + (y + z)
Definition. We define
Octonion_i0 to be
pa 0 1 of type
set.
Definition. We define
Octonion_i3 to be
pa 0 (- Complex_i) of type
set.
Definition. We define
Octonion_i5 to be
pa 0 (- Quaternion_k) of type
set.
Definition. We define
Octonion_i6 to be
pa 0 (- Quaternion_j) of type
set.
Let i1 ≝ Complex_i
Let i2 ≝ Quaternion_j
Let i4 ≝ Quaternion_k
Axiom. (
OSNo_p0_i0) We take the following as an axiom:
p0 i0 = 0
Axiom. (
OSNo_p1_i0) We take the following as an axiom:
p1 i0 = 1
Axiom. (
OSNo_p0_i3) We take the following as an axiom:
p0 i3 = 0
Axiom. (
OSNo_p1_i3) We take the following as an axiom:
Axiom. (
OSNo_p0_i5) We take the following as an axiom:
p0 i5 = 0
Axiom. (
OSNo_p1_i5) We take the following as an axiom:
Axiom. (
OSNo_p0_i6) We take the following as an axiom:
p0 i6 = 0
Axiom. (
OSNo_p1_i6) We take the following as an axiom:
End of Section SurOctonions