Beginning of Section SurOctonions
L15
Axiom. (octonion_tag_fresh) We take the following as an axiom:
∀x, HSNo x → ∀u ∈ x, {4} ∉ u
In Proofgold the corresponding term root is b25e72... and proposition id is 9cf79c...
L16
Definition. We define HSNo_pair to be pair_tag {4} of type set → set → set.
In Proofgold the corresponding term root is 62b543... and object id is 60b502...
L17
Axiom. (HSNo_pair_0) We take the following as an axiom:
∀x, HSNo_pair x 0 = x
In Proofgold the corresponding term root is 121f87... and proposition id is 367405...
L18
Axiom. (HSNo_pair_prop_1) We take the following as an axiom:
∀x1 y1 x2 y2, HSNo x1 → HSNo x2 → HSNo_pair x1 y1 = HSNo_pair x2 y2 → x1 = x2
In Proofgold the corresponding term root is 99dd5b... and proposition id is 30edd7...
L19
Axiom. (HSNo_pair_prop_2) We take the following as an axiom:
∀x1 y1 x2 y2, HSNo x1 → HSNo y1 → HSNo x2 → HSNo y2 → HSNo_pair x1 y1 = HSNo_pair x2 y2 → y1 = y2
In Proofgold the corresponding term root is 9a74c6... and proposition id is 9508dd...
L20
Definition. We define OSNo to be CD_carr {4} HSNo of type set → prop.
In Proofgold the corresponding term root is fbe446... and object id is e6b55c...
L21
Axiom. (OSNo_I) We take the following as an axiom:
∀x y, HSNo x → HSNo y → OSNo (HSNo_pair x y)
In Proofgold the corresponding term root is afb109... and proposition id is 1fdc97...
L22
Axiom. (OSNo_E) We take the following as an axiom:
∀z, OSNo z → ∀p : set → prop, (∀x y, HSNo x → HSNo y → z = HSNo_pair x y → p (HSNo_pair x y)) → p z
In Proofgold the corresponding term root is c2c632... and proposition id is 2673ee...
L23
Axiom. (HSNo_OSNo) We take the following as an axiom:
∀x, HSNo x → OSNo x
In Proofgold the corresponding term root is 4fae92... and proposition id is 097009...
L24
Axiom. (OSNo_0) We take the following as an axiom:
OSNo 0
In Proofgold the corresponding term root is 6ebd11... and proposition id is 819fb5...
L25
Axiom. (OSNo_1) We take the following as an axiom:
OSNo 1
In Proofgold the corresponding term root is 76552d... and proposition id is a6d6f8...
L26
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {4}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
L28
Axiom. (OSNo_ExtendedSNoElt_5) We take the following as an axiom:
∀z, OSNo z → ExtendedSNoElt_ 5 z
In Proofgold the corresponding term root is 5f1c66... and proposition id is 8a0ec8...
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.
L34
Let i ≝ Complex_i
L35
Let j ≝ Quaternion_j
L36
Let k ≝ Quaternion_k
L37
Definition. We define OSNo_proj0 to be CD_proj0 {4} HSNo of type set → set.
In Proofgold the corresponding term root is 13b462... and object id is a29720...
L38
Definition. We define OSNo_proj1 to be CD_proj1 {4} HSNo of type set → set.
In Proofgold the corresponding term root is c77647... and object id is 6492a3...
L39
Let p0 : set → set ≝ OSNo_proj0
L40
Let p1 : set → set ≝ OSNo_proj1
L41
Let pa : set → set → set ≝ HSNo_pair
L42
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
In Proofgold the corresponding term root is d56b4b... and proposition id is b5e6a4...
L43
Axiom. (OSNo_proj0_2) We take the following as an axiom:
∀x y, HSNo x → HSNo y → p0 (pa x y) = x
In Proofgold the corresponding term root is b97eaa... and proposition id is 37276d...
L44
Axiom. (OSNo_proj1_1) We take the following as an axiom:
∀z, OSNo z → HSNo (p1 z) ∧ z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is 8334fc... and proposition id is d28a24...
L45
Axiom. (OSNo_proj1_2) We take the following as an axiom:
∀x y, HSNo x → HSNo y → p1 (pa x y) = y
In Proofgold the corresponding term root is 00b55f... and proposition id is ad4890...
L46
Axiom. (OSNo_proj0R) We take the following as an axiom:
∀z, OSNo z → HSNo (p0 z)
In Proofgold the corresponding term root is d79361... and proposition id is bb9e47...
L47
Axiom. (OSNo_proj1R) We take the following as an axiom:
∀z, OSNo z → HSNo (p1 z)
In Proofgold the corresponding term root is 010b9d... and proposition id is 7e4dac...
L48
Axiom. (OSNo_proj0p1) We take the following as an axiom:
∀z, OSNo z → z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is 5c4035... and proposition id is d5f2d3...
L49
Axiom. (OSNo_proj0proj1_split) We take the following as an axiom:
∀z w, OSNo z → OSNo w → p0 z = p0 w → p1 z = p1 w → z = w
In Proofgold the corresponding term root is 9e9a0b... and proposition id is 2764ac...
L50
Definition. We define OSNoLev to be λz ⇒ HSNoLev (p0 z) ∪ HSNoLev (p1 z) of type set → set.
In Proofgold the corresponding term root is 26d397... and object id is 5ccbab...
L51
Axiom. (OSNoLev_ordinal) We take the following as an axiom:
∀z, OSNo z → ordinal (OSNoLev z)
In Proofgold the corresponding term root is 49d6e6... and proposition id is 9886f3...
L52
Definition. We define minus_OSNo to be CD_minus {4} HSNo minus_HSNo of type set → set.
In Proofgold the corresponding term root is ad664e... and object id is 656a9e...
L53
Definition. We define conj_OSNo to be CD_conj {4} HSNo minus_HSNo conj_HSNo of type set → set.
In Proofgold the corresponding term root is 6daad6... and object id is 78d882...
L54
Definition. We define add_OSNo to be CD_add {4} HSNo add_HSNo of type set → set → set.
In Proofgold the corresponding term root is fe136b... and object id is 298874...
L55
Definition. We define mul_OSNo to be CD_mul {4} HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo of type set → set → set.
In Proofgold the corresponding term root is a82d6b... and object id is cf582d...
L56
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.
In Proofgold the corresponding term root is 80e8fd... and object id is d6861c...
L57
Let plus' ≝ add_OSNo
L58
Let mult' ≝ mul_OSNo
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.
L64
Axiom. (OSNo_minus_OSNo) We take the following as an axiom:
∀z, OSNo z → OSNo (minus_OSNo z)
In Proofgold the corresponding term root is 5239a5... and proposition id is 33ab42...
L65
Axiom. (minus_OSNo_proj0) We take the following as an axiom:
∀z, OSNo z → p0 (:-: z) = - p0 z
In Proofgold the corresponding term root is 537bbd... and proposition id is bf0daa...
L66
Axiom. (minus_OSNo_proj1) We take the following as an axiom:
∀z, OSNo z → p1 (:-: z) = - p1 z
In Proofgold the corresponding term root is 34ff58... and proposition id is 0637f8...
L67
Axiom. (OSNo_conj_OSNo) We take the following as an axiom:
∀z, OSNo z → OSNo (conj_OSNo z)
In Proofgold the corresponding term root is 0bd248... and proposition id is 4a891d...
L68
Axiom. (conj_OSNo_proj0) We take the following as an axiom:
∀z, OSNo z → p0 (z '') = (p0 z) '
In Proofgold the corresponding term root is 9f0c90... and proposition id is 9f6dc7...
L69
Axiom. (conj_OSNo_proj1) We take the following as an axiom:
∀z, OSNo z → p1 (z '') = - p1 z
In Proofgold the corresponding term root is 0b0356... and proposition id is 88571e...
L70
Axiom. (OSNo_add_OSNo) We take the following as an axiom:
∀z w, OSNo z → OSNo w → OSNo (add_OSNo z w)
In Proofgold the corresponding term root is d59847... and proposition id is 96e815...
L71
Axiom. (add_OSNo_proj0) We take the following as an axiom:
∀z w, OSNo z → OSNo w → p0 (plus' z w) = p0 z + p0 w
In Proofgold the corresponding term root is 2a7265... and proposition id is acc7f5...
L72
Axiom. (add_OSNo_proj1) We take the following as an axiom:
∀z w, OSNo z → OSNo w → p1 (plus' z w) = p1 z + p1 w
In Proofgold the corresponding term root is 1f76aa... and proposition id is dbcaac...
L73
Axiom. (OSNo_mul_OSNo) We take the following as an axiom:
∀z w, OSNo z → OSNo w → OSNo (z ⨯ w)
In Proofgold the corresponding term root is 121ca3... and proposition id is 965453...
L74
Axiom. (mul_OSNo_proj0) We take the following as an axiom:
∀z w, OSNo z → OSNo w → p0 (mult' z w) = p0 z * p0 w + - (p1 w ' * p1 z)
In Proofgold the corresponding term root is 34f083... and proposition id is 45d781...
L75
Axiom. (mul_OSNo_proj1) We take the following as an axiom:
∀z w, OSNo z → OSNo w → p1 (mult' z w) = p1 w * p0 z + p1 z * p0 w '
In Proofgold the corresponding term root is 587f08... and proposition id is 251060...
L76
Axiom. (HSNo_OSNo_proj0) We take the following as an axiom:
∀x, HSNo x → p0 x = x
In Proofgold the corresponding term root is 3841a4... and proposition id is 5dc42a...
L77
Axiom. (HSNo_OSNo_proj1) We take the following as an axiom:
∀x, HSNo x → p1 x = 0
In Proofgold the corresponding term root is c0d013... and proposition id is 1ce9ac...
L78
Axiom. (OSNo_p0_0) We take the following as an axiom:
p0 0 = 0
In Proofgold the corresponding term root is 6e03c2... and proposition id is 50bfb2...
L79
Axiom. (OSNo_p1_0) We take the following as an axiom:
p1 0 = 0
In Proofgold the corresponding term root is 6a2ee2... and proposition id is 5b3474...
L80
Axiom. (OSNo_p0_1) We take the following as an axiom:
p0 1 = 1
In Proofgold the corresponding term root is 6166b0... and proposition id is e0ed62...
L81
Axiom. (OSNo_p1_1) We take the following as an axiom:
p1 1 = 0
In Proofgold the corresponding term root is decdcd... and proposition id is 52bcba...
L82
Axiom. (OSNo_p0_i) We take the following as an axiom:
p0 i = i
In Proofgold the corresponding term root is d61cfb... and proposition id is 092df0...
L83
Axiom. (OSNo_p1_i) We take the following as an axiom:
p1 i = 0
In Proofgold the corresponding term root is 041303... and proposition id is 0ea4e3...
L84
Axiom. (OSNo_p0_j) We take the following as an axiom:
p0 j = j
In Proofgold the corresponding term root is abf3bd... and proposition id is a67029...
L85
Axiom. (OSNo_p1_j) We take the following as an axiom:
p1 j = 0
In Proofgold the corresponding term root is d50e95... and proposition id is 2eedc2...
L86
Axiom. (OSNo_p0_k) We take the following as an axiom:
p0 k = k
In Proofgold the corresponding term root is 7d823a... and proposition id is 669c9a...
L87
Axiom. (OSNo_p1_k) We take the following as an axiom:
p1 k = 0
In Proofgold the corresponding term root is 3ff0b5... and proposition id is 1b52cc...
L88
Axiom. (minus_OSNo_minus_HSNo) We take the following as an axiom:
∀x, HSNo x → :-: x = - x
In Proofgold the corresponding term root is ad664f... and proposition id is aba4f2...
L89
Axiom. (minus_OSNo_0) We take the following as an axiom:
:-: 0 = 0
In Proofgold the corresponding term root is 82bb0f... and proposition id is 86b97f...
L90
Axiom. (conj_OSNo_conj_HSNo) We take the following as an axiom:
∀x, HSNo x → x '' = x '
In Proofgold the corresponding term root is 8cc42b... and proposition id is 071fef...
L91
Axiom. (conj_OSNo_0) We take the following as an axiom:
0 '' = 0
In Proofgold the corresponding term root is 898c21... and proposition id is 41501c...
L92
Axiom. (conj_OSNo_1) We take the following as an axiom:
1 '' = 1
In Proofgold the corresponding term root is eb7536... and proposition id is 657772...
L93
Axiom. (add_OSNo_add_HSNo) We take the following as an axiom:
∀x y, HSNo x → HSNo y → x + y = x + y
In Proofgold the corresponding term root is c83899... and proposition id is b499cd...
L94
Axiom. (mul_OSNo_mul_HSNo) We take the following as an axiom:
∀x y, HSNo x → HSNo y → x ⨯ y = x * y
In Proofgold the corresponding term root is 7fa435... and proposition id is 1eaaef...
L95
Axiom. (minus_OSNo_invol) We take the following as an axiom:
∀z, OSNo z → :-: :-: z = z
In Proofgold the corresponding term root is 0a5f21... and proposition id is 101363...
L96
Axiom. (conj_OSNo_invol) We take the following as an axiom:
∀z, OSNo z → z '' '' = z
In Proofgold the corresponding term root is 93265e... and proposition id is 468f13...
L97
Axiom. (conj_minus_OSNo) We take the following as an axiom:
∀z, OSNo z → (:-: z) '' = :-: (z '')
In Proofgold the corresponding term root is 7ff953... and proposition id is 66cbb8...
L98
Axiom. (minus_add_OSNo) We take the following as an axiom:
∀z w, OSNo z → OSNo w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is 77b3e0... and proposition id is d27c28...
L99
Axiom. (conj_add_OSNo) We take the following as an axiom:
∀z w, OSNo z → OSNo w → (z + w) '' = z '' + w ''
In Proofgold the corresponding term root is 35c199... and proposition id is 02f2b8...
L100
Axiom. (add_OSNo_com) We take the following as an axiom:
∀z w, OSNo z → OSNo w → z + w = w + z
In Proofgold the corresponding term root is a80b65... and proposition id is 2dee60...
L101
Axiom. (add_OSNo_assoc) We take the following as an axiom:
∀z w v, OSNo z → OSNo w → OSNo v → (z + w) + v = z + (w + v)
In Proofgold the corresponding term root is 88229f... and proposition id is 1279b1...
L102
Axiom. (add_OSNo_0L) We take the following as an axiom:
∀z, OSNo z → add_OSNo 0 z = z
In Proofgold the corresponding term root is 7b12c3... and proposition id is cb288a...
L103
Axiom. (add_OSNo_0R) We take the following as an axiom:
∀z, OSNo z → add_OSNo z 0 = z
In Proofgold the corresponding term root is 206e65... and proposition id is 11264f...
L104
Axiom. (add_OSNo_minus_OSNo_linv) We take the following as an axiom:
∀z, OSNo z → add_OSNo (minus_OSNo z) z = 0
In Proofgold the corresponding term root is d558dc... and proposition id is 8767d9...
L105
Axiom. (add_OSNo_minus_OSNo_rinv) We take the following as an axiom:
∀z, OSNo z → add_OSNo z (minus_OSNo z) = 0
In Proofgold the corresponding term root is 67ef27... and proposition id is 1f6cac...
L106
Axiom. (mul_OSNo_0R) We take the following as an axiom:
∀z, OSNo z → z ⨯ 0 = 0
In Proofgold the corresponding term root is 4efeb2... and proposition id is ee156e...
L107
Axiom. (mul_OSNo_0L) We take the following as an axiom:
∀z, OSNo z → 0 ⨯ z = 0
In Proofgold the corresponding term root is 9ff46d... and proposition id is ea206a...
L108
Axiom. (mul_OSNo_1R) We take the following as an axiom:
∀z, OSNo z → z ⨯ 1 = z
In Proofgold the corresponding term root is 0cf2d9... and proposition id is 71047e...
L109
Axiom. (mul_OSNo_1L) We take the following as an axiom:
∀z, OSNo z → 1 ⨯ z = z
In Proofgold the corresponding term root is d299c9... and proposition id is 0048db...
L110
Axiom. (conj_mul_OSNo) We take the following as an axiom:
∀z w, OSNo z → OSNo w → (z ⨯ w) '' = w '' ⨯ z ''
In Proofgold the corresponding term root is 05d740... and proposition id is b7721c...
L111
Axiom. (mul_OSNo_distrL) We take the following as an axiom:
∀z w u, OSNo z → OSNo w → OSNo u → z ⨯ (w + u) = z ⨯ w + z ⨯ u
In Proofgold the corresponding term root is 78f00f... and proposition id is 0d8b00...
L112
Axiom. (mul_OSNo_distrR) We take the following as an axiom:
∀z w u, OSNo z → OSNo w → OSNo u → (z + w) ⨯ u = z ⨯ u + w ⨯ u
In Proofgold the corresponding term root is f3a994... and proposition id is 76bd4b...
L113
Axiom. (minus_mul_OSNo_distrR) We take the following as an axiom:
∀z w, OSNo z → OSNo w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is 54ee0d... and proposition id is 65f43c...
L114
Axiom. (minus_mul_OSNo_distrL) We take the following as an axiom:
∀z w, OSNo z → OSNo w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is bfdb51... and proposition id is 2ef898...
L115
Axiom. (exp_OSNo_nat_0) We take the following as an axiom:
∀z, z0 = 1
In Proofgold the corresponding term root is 469625... and proposition id is 0dfdbe...
L116
Axiom. (exp_OSNo_nat_S) We take the following as an axiom:
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
In Proofgold the corresponding term root is 340b9f... and proposition id is e25374...
L117
Axiom. (exp_OSNo_nat_1) We take the following as an axiom:
∀z, OSNo z → z1 = z
In Proofgold the corresponding term root is f5712c... and proposition id is e64119...
L118
Axiom. (exp_OSNo_nat_2) We take the following as an axiom:
∀z, OSNo z → z2 = z ⨯ z
In Proofgold the corresponding term root is 6ad2c8... and proposition id is b8a62a...
L119
Axiom. (OSNo_exp_OSNo_nat) We take the following as an axiom:
∀z, OSNo z → ∀n, nat_p n → OSNo (zn)
In Proofgold the corresponding term root is 9fea84... and proposition id is ccc319...
L120
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
In Proofgold the corresponding term root is dcf334... and proposition id is 57e838...
L121
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)
In Proofgold the corresponding term root is eac30d... and proposition id is 5eecfb...
L122
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)
In Proofgold the corresponding term root is b2c7cb... and proposition id is 394006...
L123
Definition. We define Octonion_i0 to be pa 0 1 of type set.
In Proofgold the corresponding term root is 53fb1a... and object id is c8bb3f...
L124
Definition. We define Octonion_i3 to be pa 0 (- Complex_i) of type set.
In Proofgold the corresponding term root is ad3e24... and object id is f0f0f0...
L125
Definition. We define Octonion_i5 to be pa 0 (- Quaternion_k) of type set.
In Proofgold the corresponding term root is 23c235... and object id is 764d12...
L126
Definition. We define Octonion_i6 to be pa 0 (- Quaternion_j) of type set.
In Proofgold the corresponding term root is 6111ba... and object id is d882ec...
L127
Let i0 ≝ Octonion_i0
L128
Let i1 ≝ Complex_i
L129
Let i2 ≝ Quaternion_j
L130
Let i3 ≝ Octonion_i3
L131
Let i4 ≝ Quaternion_k
L132
Let i5 ≝ Octonion_i5
L133
Let i6 ≝ Octonion_i6
L134
Axiom. (OSNo_Complex_i) We take the following as an axiom:
OSNo i
In Proofgold the corresponding term root is af3f4b... and proposition id is 12bbc0...
L135
Axiom. (OSNo_Quaternion_j) We take the following as an axiom:
OSNo j
In Proofgold the corresponding term root is 77f80f... and proposition id is c8c165...
L136
Axiom. (OSNo_Quaternion_k) We take the following as an axiom:
OSNo k
In Proofgold the corresponding term root is 9b69f6... and proposition id is eba5fb...
L137
Axiom. (OSNo_Octonion_i0) We take the following as an axiom:
OSNo i0
In Proofgold the corresponding term root is e6c8dc... and proposition id is 45658b...
L138
Axiom. (OSNo_Octonion_i3) We take the following as an axiom:
OSNo i3
In Proofgold the corresponding term root is 39dd06... and proposition id is 428549...
L139
Axiom. (OSNo_Octonion_i5) We take the following as an axiom:
OSNo i5
In Proofgold the corresponding term root is 55ce63... and proposition id is e92a7a...
L140
Axiom. (OSNo_Octonion_i6) We take the following as an axiom:
OSNo i6
In Proofgold the corresponding term root is 73ed2a... and proposition id is d0f581...
L141
Axiom. (OSNo_p0_i0) We take the following as an axiom:
p0 i0 = 0
In Proofgold the corresponding term root is c9a02f... and proposition id is 444265...
L142
Axiom. (OSNo_p1_i0) We take the following as an axiom:
p1 i0 = 1
In Proofgold the corresponding term root is 6bb51f... and proposition id is 17a56f...
L143
Axiom. (OSNo_p0_i3) We take the following as an axiom:
p0 i3 = 0
In Proofgold the corresponding term root is 784dc9... and proposition id is 27f5a3...
L144
Axiom. (OSNo_p1_i3) We take the following as an axiom:
p1 i3 = - i
In Proofgold the corresponding term root is 097faa... and proposition id is 6371c8...
L145
Axiom. (OSNo_p0_i5) We take the following as an axiom:
p0 i5 = 0
In Proofgold the corresponding term root is 597589... and proposition id is c4b46c...
L146
Axiom. (OSNo_p1_i5) We take the following as an axiom:
p1 i5 = - k
In Proofgold the corresponding term root is ef1afc... and proposition id is 9bf42c...
L147
Axiom. (OSNo_p0_i6) We take the following as an axiom:
p0 i6 = 0
In Proofgold the corresponding term root is bf6e13... and proposition id is 183aad...
L148
Axiom. (OSNo_p1_i6) We take the following as an axiom:
p1 i6 = - j
In Proofgold the corresponding term root is 50991b... and proposition id is 78f3bd...
L149
Axiom. (Octonion_i1_sqr) We take the following as an axiom:
i1 ⨯ i1 = :-: 1
In Proofgold the corresponding term root is 2cf2b7... and proposition id is 701b4a...
L150
Axiom. (Octonion_i2_sqr) We take the following as an axiom:
i2 ⨯ i2 = :-: 1
In Proofgold the corresponding term root is 52dca5... and proposition id is 46db7e...
L151
Axiom. (Octonion_i4_sqr) We take the following as an axiom:
i4 ⨯ i4 = :-: 1
In Proofgold the corresponding term root is e85aa9... and proposition id is f8d60f...
L152
Axiom. (Octonion_i0_sqr) We take the following as an axiom:
i0 ⨯ i0 = :-: 1
In Proofgold the corresponding term root is 6e1738... and proposition id is 4f5642...
L153
Axiom. (Octonion_i3_sqr) We take the following as an axiom:
i3 ⨯ i3 = :-: 1
In Proofgold the corresponding term root is 8c0727... and proposition id is 24bf69...
L154
Axiom. (Octonion_i5_sqr) We take the following as an axiom:
i5 ⨯ i5 = :-: 1
In Proofgold the corresponding term root is 19b120... and proposition id is 474ccf...
L155
Axiom. (Octonion_i6_sqr) We take the following as an axiom:
i6 ⨯ i6 = :-: 1
In Proofgold the corresponding term root is 97f9e7... and proposition id is 12af41...
L156
Axiom. (Octonion_i1_i2) We take the following as an axiom:
i1 ⨯ i2 = i4
In Proofgold the corresponding term root is 54f62e... and proposition id is fd7e6b...
L157
Axiom. (Octonion_i2_i1) We take the following as an axiom:
i2 ⨯ i1 = :-: i4
In Proofgold the corresponding term root is a29e37... and proposition id is f1a9c7...
L158
Axiom. (Octonion_i2_i4) We take the following as an axiom:
i2 ⨯ i4 = i1
In Proofgold the corresponding term root is 32f52e... and proposition id is 60c4d4...
L159
Axiom. (Octonion_i4_i2) We take the following as an axiom:
i4 ⨯ i2 = :-: i1
In Proofgold the corresponding term root is 0c684d... and proposition id is 294b23...
L160
Axiom. (Octonion_i4_i1) We take the following as an axiom:
i4 ⨯ i1 = i2
In Proofgold the corresponding term root is fe2349... and proposition id is f00e84...
L161
Axiom. (Octonion_i1_i4) We take the following as an axiom:
i1 ⨯ i4 = :-: i2
In Proofgold the corresponding term root is 6ef84c... and proposition id is 48faff...
L162
Axiom. (Octonion_i2_i3) We take the following as an axiom:
i2 ⨯ i3 = i5
In Proofgold the corresponding term root is 69b316... and proposition id is 7ee827...
L163
Axiom. (Octonion_i3_i2) We take the following as an axiom:
i3 ⨯ i2 = :-: i5
In Proofgold the corresponding term root is 189ce1... and proposition id is ba3701...
L164
Axiom. (Octonion_i3_i5) We take the following as an axiom:
i3 ⨯ i5 = i2
In Proofgold the corresponding term root is 0c085c... and proposition id is 54e1ef...
L165
Axiom. (Octonion_i5_i3) We take the following as an axiom:
i5 ⨯ i3 = :-: i2
In Proofgold the corresponding term root is e8fde0... and proposition id is 9faab2...
L166
Axiom. (Octonion_i5_i2) We take the following as an axiom:
i5 ⨯ i2 = i3
In Proofgold the corresponding term root is 346b35... and proposition id is 40996f...
L167
Axiom. (Octonion_i2_i5) We take the following as an axiom:
i2 ⨯ i5 = :-: i3
In Proofgold the corresponding term root is 2d78a7... and proposition id is f300cd...
L168
Axiom. (Octonion_i3_i4) We take the following as an axiom:
i3 ⨯ i4 = i6
In Proofgold the corresponding term root is 511ac9... and proposition id is 73693c...
L169
Axiom. (Octonion_i4_i3) We take the following as an axiom:
i4 ⨯ i3 = :-: i6
In Proofgold the corresponding term root is e373e5... and proposition id is b2ad1d...
L170
Axiom. (Octonion_i4_i6) We take the following as an axiom:
i4 ⨯ i6 = i3
In Proofgold the corresponding term root is 620e03... and proposition id is 7c49f7...
L171
Axiom. (Octonion_i6_i4) We take the following as an axiom:
i6 ⨯ i4 = :-: i3
In Proofgold the corresponding term root is 121f61... and proposition id is 0b4e69...
L172
Axiom. (Octonion_i6_i3) We take the following as an axiom:
i6 ⨯ i3 = i4
In Proofgold the corresponding term root is d3cc9f... and proposition id is 9b6ce9...
L173
Axiom. (Octonion_i3_i6) We take the following as an axiom:
i3 ⨯ i6 = :-: i4
In Proofgold the corresponding term root is 575da0... and proposition id is 517b53...
L174
Axiom. (Octonion_i4_i5) We take the following as an axiom:
i4 ⨯ i5 = i0
In Proofgold the corresponding term root is 360332... and proposition id is fc370d...
L175
Axiom. (Octonion_i5_i4) We take the following as an axiom:
i5 ⨯ i4 = :-: i0
In Proofgold the corresponding term root is beff8b... and proposition id is afcfe9...
L176
Axiom. (Octonion_i5_i0) We take the following as an axiom:
i5 ⨯ i0 = i4
In Proofgold the corresponding term root is adfd5d... and proposition id is e39b44...
L177
Axiom. (Octonion_i0_i5) We take the following as an axiom:
i0 ⨯ i5 = :-: i4
In Proofgold the corresponding term root is 498fb6... and proposition id is 0b796b...
L178
Axiom. (Octonion_i0_i4) We take the following as an axiom:
i0 ⨯ i4 = i5
In Proofgold the corresponding term root is 133131... and proposition id is 3686a2...
L179
Axiom. (Octonion_i4_i0) We take the following as an axiom:
i4 ⨯ i0 = :-: i5
In Proofgold the corresponding term root is 01a797... and proposition id is 529327...
L180
Axiom. (Octonion_i5_i6) We take the following as an axiom:
i5 ⨯ i6 = i1
In Proofgold the corresponding term root is f51c6c... and proposition id is bd260d...
L181
Axiom. (Octonion_i6_i5) We take the following as an axiom:
i6 ⨯ i5 = :-: i1
In Proofgold the corresponding term root is b9e439... and proposition id is b85ae9...
L182
Axiom. (Octonion_i6_i1) We take the following as an axiom:
i6 ⨯ i1 = i5
In Proofgold the corresponding term root is e457ad... and proposition id is a0a7b9...
L183
Axiom. (Octonion_i1_i6) We take the following as an axiom:
i1 ⨯ i6 = :-: i5
In Proofgold the corresponding term root is c1b4e0... and proposition id is bd93b5...
L184
Axiom. (Octonion_i1_i5) We take the following as an axiom:
i1 ⨯ i5 = i6
In Proofgold the corresponding term root is 1e9e88... and proposition id is 3b1993...
L185
Axiom. (Octonion_i5_i1) We take the following as an axiom:
i5 ⨯ i1 = :-: i6
In Proofgold the corresponding term root is 5e4738... and proposition id is 547b1a...
L186
Axiom. (Octonion_i6_i0) We take the following as an axiom:
i6 ⨯ i0 = i2
In Proofgold the corresponding term root is 73d83a... and proposition id is c60735...
L187
Axiom. (Octonion_i0_i6) We take the following as an axiom:
i0 ⨯ i6 = :-: i2
In Proofgold the corresponding term root is 7f039d... and proposition id is dc4654...
L188
Axiom. (Octonion_i0_i2) We take the following as an axiom:
i0 ⨯ i2 = i6
In Proofgold the corresponding term root is 95da86... and proposition id is b659de...
L189
Axiom. (Octonion_i2_i0) We take the following as an axiom:
i2 ⨯ i0 = :-: i6
In Proofgold the corresponding term root is cafa53... and proposition id is 330a2a...
L190
Axiom. (Octonion_i2_i6) We take the following as an axiom:
i2 ⨯ i6 = i0
In Proofgold the corresponding term root is 787314... and proposition id is b9cfda...
L191
Axiom. (Octonion_i6_i2) We take the following as an axiom:
i6 ⨯ i2 = :-: i0
In Proofgold the corresponding term root is 158a18... and proposition id is cd6dcf...
L192
Axiom. (Octonion_i0_i1) We take the following as an axiom:
i0 ⨯ i1 = i3
In Proofgold the corresponding term root is b43708... and proposition id is 251b34...
L193
Axiom. (Octonion_i1_i0) We take the following as an axiom:
i1 ⨯ i0 = :-: i3
In Proofgold the corresponding term root is 9cb018... and proposition id is 9165d8...
L194
Axiom. (Octonion_i1_i3) We take the following as an axiom:
i1 ⨯ i3 = i0
In Proofgold the corresponding term root is 3cc4e3... and proposition id is f71c20...
L195
Axiom. (Octonion_i3_i1) We take the following as an axiom:
i3 ⨯ i1 = :-: i0
In Proofgold the corresponding term root is 2603e9... and proposition id is 105f8c...
L196
Axiom. (Octonion_i3_i0) We take the following as an axiom:
i3 ⨯ i0 = i1
In Proofgold the corresponding term root is 902425... and proposition id is cf0eac...
L197
Axiom. (Octonion_i0_i3) We take the following as an axiom:
i0 ⨯ i3 = :-: i1
In Proofgold the corresponding term root is 73d689... and proposition id is c0f00e...
End of Section SurOctonions
Beginning of Section Octonions
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_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.
L203
Let i0 ≝ Octonion_i0
L204
Let i1 ≝ Complex_i
L205
Let i2 ≝ Quaternion_j
L206
Let i3 ≝ Octonion_i3
L207
Let i4 ≝ Quaternion_k
L208
Let i5 ≝ Octonion_i5
L209
Let i6 ≝ Octonion_i6
L210
Let i ≝ Complex_i
L211
Let j ≝ Quaternion_j
L212
Let k ≝ Quaternion_k
L213
Let p0 : set → set ≝ OSNo_proj0
L214
Let p1 : set → set ≝ OSNo_proj1
L215
Let pa : set → set → set ≝ HSNo_pair
L216
Definition. We define octonion to be {pa (u 0) (u 1)|u ∈ quaternion ⨯ quaternion} of type set.
In Proofgold the corresponding term root is 6ebcf6... and object id is 7c2d1f...
L217
Axiom. (octonion_I) We take the following as an axiom:
∀x y ∈ quaternion, pa x y ∈ octonion
In Proofgold the corresponding term root is f43249... and proposition id is dd28a1...
L218
Axiom. (octonion_E) We take the following as an axiom:
∀z ∈ octonion, ∀p : prop, (∀x y ∈ quaternion, z = pa x y → p) → p
In Proofgold the corresponding term root is a7e8fb... and proposition id is eacc79...
L219
Axiom. (octonion_OSNo) We take the following as an axiom:
∀z ∈ octonion, OSNo z
In Proofgold the corresponding term root is 9d2e4f... and proposition id is 7590f8...
L220
Axiom. (quaternion_octonion) We take the following as an axiom:
quaternion ⊆ octonion
In Proofgold the corresponding term root is 07aea1... and proposition id is a740e9...
L221
Axiom. (octonion_0) We take the following as an axiom:
0 ∈ octonion
In Proofgold the corresponding term root is b78b5b... and proposition id is 27f55c...
L222
Axiom. (octonion_1) We take the following as an axiom:
1 ∈ octonion
In Proofgold the corresponding term root is 6b24ca... and proposition id is 0db162...
L223
Axiom. (octonion_i) We take the following as an axiom:
i ∈ octonion
In Proofgold the corresponding term root is 19312b... and proposition id is 8de3fa...
L224
Axiom. (octonion_j) We take the following as an axiom:
j ∈ octonion
In Proofgold the corresponding term root is 7c86a8... and proposition id is 72f255...
L225
Axiom. (octonion_k) We take the following as an axiom:
k ∈ octonion
In Proofgold the corresponding term root is 18b0b4... and proposition id is b1a0f0...
L226
Axiom. (octonion_i0) We take the following as an axiom:
i0 ∈ octonion
In Proofgold the corresponding term root is 920cc3... and proposition id is 92ff8b...
L227
Axiom. (octonion_i3) We take the following as an axiom:
i3 ∈ octonion
In Proofgold the corresponding term root is b1ffb8... and proposition id is a130b1...
L228
Axiom. (octonion_i5) We take the following as an axiom:
i5 ∈ octonion
In Proofgold the corresponding term root is 4f9ec6... and proposition id is 269f68...
L229
Axiom. (octonion_i6) We take the following as an axiom:
i6 ∈ octonion
In Proofgold the corresponding term root is 57dd50... and proposition id is 70b59d...
L230
Axiom. (octonion_p0_eq) We take the following as an axiom:
∀x y ∈ quaternion, p0 (pa x y) = x
In Proofgold the corresponding term root is d31937... and proposition id is d69485...
L231
Axiom. (octonion_p1_eq) We take the following as an axiom:
∀x y ∈ quaternion, p1 (pa x y) = y
In Proofgold the corresponding term root is 6ca6c3... and proposition id is f4be43...
L232
Axiom. (octonion_p0_quaternion) We take the following as an axiom:
∀z ∈ octonion, p0 z ∈ quaternion
In Proofgold the corresponding term root is 63ea34... and proposition id is e55972...
L233
Axiom. (octonion_p1_quaternion) We take the following as an axiom:
∀z ∈ octonion, p1 z ∈ quaternion
In Proofgold the corresponding term root is de6ec0... and proposition id is ecc213...
L234
Axiom. (octonion_proj0proj1_split) We take the following as an axiom:
∀z w ∈ octonion, p0 z = p0 w → p1 z = p1 w → z = w
In Proofgold the corresponding term root is 19e8bb... and proposition id is 32b380...
L235
Axiom. (octonion_minus_OSNo) We take the following as an axiom:
∀z ∈ octonion, - z ∈ octonion
In Proofgold the corresponding term root is 5ae75b... and proposition id is 41d946...
L236
Axiom. (octonion_conj_OSNo) We take the following as an axiom:
∀z ∈ octonion, conj_OSNo z ∈ octonion
In Proofgold the corresponding term root is b7a7a4... and proposition id is d72ac7...
L237
Axiom. (octonion_add_OSNo) We take the following as an axiom:
∀z w ∈ octonion, z + w ∈ octonion
In Proofgold the corresponding term root is 8e6d64... and proposition id is f59ccf...
L238
Axiom. (octonion_mul_OSNo) We take the following as an axiom:
∀z w ∈ octonion, z * w ∈ octonion
In Proofgold the corresponding term root is 1d3e8a... and proposition id is b76bb1...
L239
Axiom. (quaternion_p0_eq') We take the following as an axiom:
∀x ∈ quaternion, p0 x = x
In Proofgold the corresponding term root is 6b0e75... and proposition id is fc55a6...
L240
Axiom. (quaternion_p1_eq') We take the following as an axiom:
∀x ∈ quaternion, p1 x = 0
In Proofgold the corresponding term root is 7e57a1... and proposition id is d3a12f...
End of Section Octonions