Beginning of Section SurQuaternions
L14
Axiom. (quaternion_tag_fresh) We take the following as an axiom:
∀z, CSNo z → ∀u ∈ z, {3} ∉ u
In Proofgold the corresponding term root is 202f04... and proposition id is cbed07...
L15
Definition. We define CSNo_pair to be pair_tag {3} of type set → set → set.
In Proofgold the corresponding term root is 6ad954... and object id is bd2d99...
L16
Axiom. (CSNo_pair_0) We take the following as an axiom:
∀x, CSNo_pair x 0 = x
In Proofgold the corresponding term root is 4db8eb... and proposition id is abfae9...
L17
Axiom. (CSNo_pair_prop_1) We take the following as an axiom:
∀x1 y1 x2 y2, CSNo x1 → CSNo x2 → CSNo_pair x1 y1 = CSNo_pair x2 y2 → x1 = x2
In Proofgold the corresponding term root is 232223... and proposition id is b34370...
L18
Axiom. (CSNo_pair_prop_2) We take the following as an axiom:
∀x1 y1 x2 y2, CSNo x1 → CSNo y1 → CSNo x2 → CSNo y2 → CSNo_pair x1 y1 = CSNo_pair x2 y2 → y1 = y2
In Proofgold the corresponding term root is 225c4f... and proposition id is 9ff93a...
L19
Definition. We define HSNo to be CD_carr {3} CSNo of type set → prop.
In Proofgold the corresponding term root is 1e7352... and object id is 89bf4d...
L20
Axiom. (HSNo_I) We take the following as an axiom:
∀x y, CSNo x → CSNo y → HSNo (CSNo_pair x y)
In Proofgold the corresponding term root is 17ad60... and proposition id is 8476c5...
L21
Axiom. (HSNo_E) We take the following as an axiom:
∀z, HSNo z → ∀p : set → prop, (∀x y, CSNo x → CSNo y → z = CSNo_pair x y → p (CSNo_pair x y)) → p z
In Proofgold the corresponding term root is 318e94... and proposition id is a9207a...
L22
Axiom. (CSNo_HSNo) We take the following as an axiom:
∀x, CSNo x → HSNo x
In Proofgold the corresponding term root is 307398... and proposition id is 0db147...
L23
Axiom. (HSNo_0) We take the following as an axiom:
HSNo 0
In Proofgold the corresponding term root is 27cacb... and proposition id is d3c9ac...
L24
Axiom. (HSNo_1) We take the following as an axiom:
HSNo 1
In Proofgold the corresponding term root is 3065de... and proposition id is ca7c07...
L25
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {3}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
L27
Axiom. (HSNo_ExtendedSNoElt_4) We take the following as an axiom:
∀z, HSNo z → ExtendedSNoElt_ 4 z
In Proofgold the corresponding term root is 4407d8... and proposition id is d88675...
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.
L33
Let i ≝ Complex_i
L34
Definition. We define Quaternion_j to be CSNo_pair 0 1 of type set.
In Proofgold the corresponding term root is c0b7d8... and object id is 834439...
L35
Definition. We define Quaternion_k to be CSNo_pair 0 i of type set.
In Proofgold the corresponding term root is 7dfb3a... and object id is 3ae5b3...
L36
Let j ≝ Quaternion_j
L37
Let k ≝ Quaternion_k
L38
Definition. We define HSNo_proj0 to be CD_proj0 {3} CSNo of type set → set.
In Proofgold the corresponding term root is 93f0b6... and object id is 0380b7...
L39
Definition. We define HSNo_proj1 to be CD_proj1 {3} CSNo of type set → set.
In Proofgold the corresponding term root is bc3d4d... and object id is c8e617...
L40
Let p0 : set → set ≝ HSNo_proj0
L41
Let p1 : set → set ≝ HSNo_proj1
L42
Let pa : set → set → set ≝ CSNo_pair
L43
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
In Proofgold the corresponding term root is 47baad... and proposition id is d8e2ef...
L44
Axiom. (HSNo_proj0_2) We take the following as an axiom:
∀x y, CSNo x → CSNo y → p0 (pa x y) = x
In Proofgold the corresponding term root is 9ffb4a... and proposition id is 57a042...
L45
Axiom. (HSNo_proj1_1) We take the following as an axiom:
∀z, HSNo z → CSNo (p1 z) ∧ z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is d65060... and proposition id is b38fa3...
L46
Axiom. (HSNo_proj1_2) We take the following as an axiom:
∀x y, CSNo x → CSNo y → p1 (pa x y) = y
In Proofgold the corresponding term root is 2c4d65... and proposition id is b8596e...
L47
Axiom. (HSNo_proj0R) We take the following as an axiom:
∀z, HSNo z → CSNo (p0 z)
In Proofgold the corresponding term root is dfba9c... and proposition id is d5b6be...
L48
Axiom. (HSNo_proj1R) We take the following as an axiom:
∀z, HSNo z → CSNo (p1 z)
In Proofgold the corresponding term root is 88c956... and proposition id is 4c5b7f...
L49
Axiom. (HSNo_proj0p1) We take the following as an axiom:
∀z, HSNo z → z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is 099ef1... and proposition id is cd06de...
L50
Axiom. (HSNo_proj0proj1_split) We take the following as an axiom:
∀z w, HSNo z → HSNo w → p0 z = p0 w → p1 z = p1 w → z = w
In Proofgold the corresponding term root is 878bb6... and proposition id is 4cfedf...
L51
Definition. We define HSNoLev to be λz ⇒ CSNoLev (p0 z) ∪ CSNoLev (p1 z) of type set → set.
In Proofgold the corresponding term root is 7ed157... and object id is c05a12...
L52
Axiom. (HSNoLev_ordinal) We take the following as an axiom:
∀z, HSNo z → ordinal (HSNoLev z)
In Proofgold the corresponding term root is 5fdf84... and proposition id is c12b44...
L53
Definition. We define minus_HSNo to be CD_minus {3} CSNo minus_CSNo of type set → set.
In Proofgold the corresponding term root is f59664... and object id is b481a7...
L54
Definition. We define conj_HSNo to be CD_conj {3} CSNo minus_CSNo conj_CSNo of type set → set.
In Proofgold the corresponding term root is 87fd0c... and object id is 66366c...
L55
Definition. We define add_HSNo to be CD_add {3} CSNo add_CSNo of type set → set → set.
In Proofgold the corresponding term root is a3bb10... and object id is 3681e1...
L56
Definition. We define mul_HSNo to be CD_mul {3} CSNo minus_CSNo conj_CSNo add_CSNo mul_CSNo of type set → set → set.
In Proofgold the corresponding term root is e7bde6... and object id is 34cbed...
L57
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.
In Proofgold the corresponding term root is b3bc74... and object id is 121913...
L58
Let plus' ≝ add_HSNo
L59
Let mult' ≝ mul_HSNo
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.
L65
Axiom. (HSNo_Complex_i) We take the following as an axiom:
HSNo i
In Proofgold the corresponding term root is 1c2523... and proposition id is 9eee28...
L66
Axiom. (HSNo_Quaternion_j) We take the following as an axiom:
HSNo j
In Proofgold the corresponding term root is 498a34... and proposition id is 4e668f...
L67
Axiom. (HSNo_Quaternion_k) We take the following as an axiom:
HSNo k
In Proofgold the corresponding term root is 5a2d44... and proposition id is 7b6e43...
L68
Axiom. (HSNo_minus_HSNo) We take the following as an axiom:
∀z, HSNo z → HSNo (minus_HSNo z)
In Proofgold the corresponding term root is e82f65... and proposition id is f8d185...
L69
Axiom. (minus_HSNo_proj0) We take the following as an axiom:
∀z, HSNo z → p0 (:-: z) = - p0 z
In Proofgold the corresponding term root is 0f68d7... and proposition id is b166fc...
L70
Axiom. (minus_HSNo_proj1) We take the following as an axiom:
∀z, HSNo z → p1 (:-: z) = - p1 z
In Proofgold the corresponding term root is 26353b... and proposition id is bd1384...
L71
Axiom. (HSNo_conj_HSNo) We take the following as an axiom:
∀z, HSNo z → HSNo (conj_HSNo z)
In Proofgold the corresponding term root is 2747f5... and proposition id is 67a2db...
L72
Axiom. (conj_HSNo_proj0) We take the following as an axiom:
∀z, HSNo z → p0 (z '') = (p0 z) '
In Proofgold the corresponding term root is c3731a... and proposition id is b3ff6d...
L73
Axiom. (conj_HSNo_proj1) We take the following as an axiom:
∀z, HSNo z → p1 (z '') = - p1 z
In Proofgold the corresponding term root is 07def3... and proposition id is 686476...
L74
Axiom. (HSNo_add_HSNo) We take the following as an axiom:
∀z w, HSNo z → HSNo w → HSNo (add_HSNo z w)
In Proofgold the corresponding term root is 37bb2a... and proposition id is 1f7aba...
L75
Axiom. (add_HSNo_proj0) We take the following as an axiom:
∀z w, HSNo z → HSNo w → p0 (plus' z w) = p0 z + p0 w
In Proofgold the corresponding term root is 3f6ec4... and proposition id is 565511...
L76
Axiom. (add_HSNo_proj1) We take the following as an axiom:
∀z w, HSNo z → HSNo w → p1 (plus' z w) = p1 z + p1 w
In Proofgold the corresponding term root is 5b2438... and proposition id is 9fce86...
L77
Axiom. (HSNo_mul_HSNo) We take the following as an axiom:
∀z w, HSNo z → HSNo w → HSNo (z ⨯ w)
In Proofgold the corresponding term root is 25d347... and proposition id is 5382cd...
L78
Axiom. (mul_HSNo_proj0) We take the following as an axiom:
∀z w, HSNo z → HSNo w → p0 (mult' z w) = p0 z * p0 w + - (p1 w ' * p1 z)
In Proofgold the corresponding term root is e081e6... and proposition id is 28f7fb...
L79
Axiom. (mul_HSNo_proj1) We take the following as an axiom:
∀z w, HSNo z → HSNo w → p1 (mult' z w) = p1 w * p0 z + p1 z * p0 w '
In Proofgold the corresponding term root is a68970... and proposition id is 7821b7...
L80
Axiom. (CSNo_HSNo_proj0) We take the following as an axiom:
∀x, CSNo x → p0 x = x
In Proofgold the corresponding term root is 60fe35... and proposition id is 7639bd...
L81
Axiom. (CSNo_HSNo_proj1) We take the following as an axiom:
∀x, CSNo x → p1 x = 0
In Proofgold the corresponding term root is 15d87b... and proposition id is 952144...
L82
Axiom. (HSNo_p0_0) We take the following as an axiom:
p0 0 = 0
In Proofgold the corresponding term root is 6b350d... and proposition id is f0ff58...
L83
Axiom. (HSNo_p1_0) We take the following as an axiom:
p1 0 = 0
In Proofgold the corresponding term root is ba0409... and proposition id is 1878d5...
L84
Axiom. (HSNo_p0_1) We take the following as an axiom:
p0 1 = 1
In Proofgold the corresponding term root is 4dd8fa... and proposition id is b0bea3...
L85
Axiom. (HSNo_p1_1) We take the following as an axiom:
p1 1 = 0
In Proofgold the corresponding term root is 93fc91... and proposition id is 3f14ef...
L86
Axiom. (HSNo_p0_i) We take the following as an axiom:
p0 i = i
In Proofgold the corresponding term root is 905afa... and proposition id is 50a227...
L87
Axiom. (HSNo_p1_i) We take the following as an axiom:
p1 i = 0
In Proofgold the corresponding term root is 768a8d... and proposition id is 7ea9df...
L88
Axiom. (HSNo_p0_j) We take the following as an axiom:
p0 j = 0
In Proofgold the corresponding term root is 767fd7... and proposition id is 21c475...
L89
Axiom. (HSNo_p1_j) We take the following as an axiom:
p1 j = 1
In Proofgold the corresponding term root is 3b95bd... and proposition id is abaaec...
L90
Axiom. (HSNo_p0_k) We take the following as an axiom:
p0 k = 0
In Proofgold the corresponding term root is e603b4... and proposition id is 8baec9...
L91
Axiom. (HSNo_p1_k) We take the following as an axiom:
p1 k = i
In Proofgold the corresponding term root is 80ea56... and proposition id is 575ab4...
L92
Axiom. (minus_HSNo_minus_CSNo) We take the following as an axiom:
∀x, CSNo x → :-: x = - x
In Proofgold the corresponding term root is a9014c... and proposition id is 7b42d4...
L93
Axiom. (minus_HSNo_0) We take the following as an axiom:
:-: 0 = 0
In Proofgold the corresponding term root is 176f59... and proposition id is 776989...
L94
Axiom. (conj_HSNo_conj_CSNo) We take the following as an axiom:
∀x, CSNo x → x '' = x '
In Proofgold the corresponding term root is 64571f... and proposition id is 7817d5...
L95
Axiom. (conj_HSNo_id_SNo) We take the following as an axiom:
∀x, SNo x → x '' = x
In Proofgold the corresponding term root is ebe6df... and proposition id is 58d64a...
L96
Axiom. (conj_HSNo_0) We take the following as an axiom:
0 '' = 0
In Proofgold the corresponding term root is 0665e6... and proposition id is 1a59ff...
L97
Axiom. (conj_HSNo_1) We take the following as an axiom:
1 '' = 1
In Proofgold the corresponding term root is 6faceb... and proposition id is 3cd551...
L98
Axiom. (add_HSNo_add_CSNo) We take the following as an axiom:
∀x y, CSNo x → CSNo y → x + y = x + y
In Proofgold the corresponding term root is 6e3971... and proposition id is b05210...
L99
Axiom. (mul_HSNo_mul_CSNo) We take the following as an axiom:
∀x y, CSNo x → CSNo y → x ⨯ y = x * y
In Proofgold the corresponding term root is c8a0d0... and proposition id is e84c3f...
L100
Axiom. (minus_HSNo_invol) We take the following as an axiom:
∀z, HSNo z → :-: :-: z = z
In Proofgold the corresponding term root is 91a264... and proposition id is d5104e...
L101
Axiom. (conj_HSNo_invol) We take the following as an axiom:
∀z, HSNo z → z '' '' = z
In Proofgold the corresponding term root is 8faa1e... and proposition id is 3cc997...
L102
Axiom. (conj_minus_HSNo) We take the following as an axiom:
∀z, HSNo z → (:-: z) '' = :-: (z '')
In Proofgold the corresponding term root is ad72ab... and proposition id is 97ffd3...
L103
Axiom. (minus_add_HSNo) We take the following as an axiom:
∀z w, HSNo z → HSNo w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is ea90cf... and proposition id is 5c75f8...
L104
Axiom. (conj_add_HSNo) We take the following as an axiom:
∀z w, HSNo z → HSNo w → (z + w) '' = z '' + w ''
In Proofgold the corresponding term root is 777e84... and proposition id is ec65d2...
L105
Axiom. (add_HSNo_com) We take the following as an axiom:
∀z w, HSNo z → HSNo w → z + w = w + z
In Proofgold the corresponding term root is e30f23... and proposition id is a91741...
L106
Axiom. (add_HSNo_assoc) We take the following as an axiom:
∀z w v, HSNo z → HSNo w → HSNo v → (z + w) + v = z + (w + v)
In Proofgold the corresponding term root is 2ad3fc... and proposition id is a6a347...
L107
Axiom. (add_HSNo_0L) We take the following as an axiom:
∀z, HSNo z → add_HSNo 0 z = z
In Proofgold the corresponding term root is 18376d... and proposition id is 1b0119...
L108
Axiom. (add_HSNo_0R) We take the following as an axiom:
∀z, HSNo z → add_HSNo z 0 = z
In Proofgold the corresponding term root is 5a9044... and proposition id is 0c0186...
L109
Axiom. (add_HSNo_minus_HSNo_linv) We take the following as an axiom:
∀z, HSNo z → add_HSNo (minus_HSNo z) z = 0
In Proofgold the corresponding term root is 2161be... and proposition id is c0a796...
L110
Axiom. (add_HSNo_minus_HSNo_rinv) We take the following as an axiom:
∀z, HSNo z → add_HSNo z (minus_HSNo z) = 0
In Proofgold the corresponding term root is e16e72... and proposition id is f52141...
L111
Axiom. (mul_HSNo_0R) We take the following as an axiom:
∀z, HSNo z → z ⨯ 0 = 0
In Proofgold the corresponding term root is c6c5df... and proposition id is a6c3c2...
L112
Axiom. (mul_HSNo_0L) We take the following as an axiom:
∀z, HSNo z → 0 ⨯ z = 0
In Proofgold the corresponding term root is d9f510... and proposition id is 2984ec...
L113
Axiom. (mul_HSNo_1R) We take the following as an axiom:
∀z, HSNo z → z ⨯ 1 = z
In Proofgold the corresponding term root is ec38b4... and proposition id is 896e80...
L114
Axiom. (mul_HSNo_1L) We take the following as an axiom:
∀z, HSNo z → 1 ⨯ z = z
In Proofgold the corresponding term root is 80a90e... and proposition id is 4c64b4...
L115
Axiom. (conj_mul_HSNo) We take the following as an axiom:
∀z w, HSNo z → HSNo w → (z ⨯ w) '' = w '' ⨯ z ''
In Proofgold the corresponding term root is 64a2e5... and proposition id is 225be1...
L116
Axiom. (mul_HSNo_distrL) We take the following as an axiom:
∀z w u, HSNo z → HSNo w → HSNo u → z ⨯ (w + u) = z ⨯ w + z ⨯ u
In Proofgold the corresponding term root is 347c37... and proposition id is 0d4990...
L117
Axiom. (mul_HSNo_distrR) We take the following as an axiom:
∀z w u, HSNo z → HSNo w → HSNo u → (z + w) ⨯ u = z ⨯ u + w ⨯ u
In Proofgold the corresponding term root is c716fd... and proposition id is 7dee08...
L118
Axiom. (minus_mul_HSNo_distrR) We take the following as an axiom:
∀z w, HSNo z → HSNo w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is e18e00... and proposition id is 122e5c...
L119
Axiom. (minus_mul_HSNo_distrL) We take the following as an axiom:
∀z w, HSNo z → HSNo w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is e48f25... and proposition id is e67e13...
L120
Axiom. (exp_HSNo_nat_0) We take the following as an axiom:
∀z, z0 = 1
In Proofgold the corresponding term root is a8e4e1... and proposition id is 858195...
L121
Axiom. (exp_HSNo_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 5c2375... and proposition id is 5ccd45...
L122
Axiom. (exp_HSNo_nat_1) We take the following as an axiom:
∀z, HSNo z → z1 = z
In Proofgold the corresponding term root is 83d5ec... and proposition id is 209eff...
L123
Axiom. (exp_HSNo_nat_2) We take the following as an axiom:
∀z, HSNo z → z2 = z ⨯ z
In Proofgold the corresponding term root is 0756a0... and proposition id is dd7b0e...
L124
Axiom. (HSNo_exp_HSNo_nat) We take the following as an axiom:
∀z, HSNo z → ∀n, nat_p n → HSNo (zn)
In Proofgold the corresponding term root is dfb84a... and proposition id is cfcd35...
L125
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
In Proofgold the corresponding term root is e361b0... and proposition id is 4b207f...
L126
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)
In Proofgold the corresponding term root is 458601... and proposition id is fbf900...
L127
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)
In Proofgold the corresponding term root is fbee7e... and proposition id is 6a0798...
L128
Axiom. (Quaternion_i_sqr) We take the following as an axiom:
i ⨯ i = :-: 1
In Proofgold the corresponding term root is ab7a70... and proposition id is 6ce0c7...
L129
Axiom. (Quaternion_j_sqr) We take the following as an axiom:
j ⨯ j = :-: 1
In Proofgold the corresponding term root is b4236f... and proposition id is 9f0956...
L130
Axiom. (Quaternion_k_sqr) We take the following as an axiom:
k ⨯ k = :-: 1
In Proofgold the corresponding term root is 0298ee... and proposition id is c4384d...
L131
Axiom. (Quaternion_i_j) We take the following as an axiom:
i ⨯ j = k
In Proofgold the corresponding term root is 0337aa... and proposition id is b64eb9...
L132
Axiom. (Quaternion_j_k) We take the following as an axiom:
j ⨯ k = i
In Proofgold the corresponding term root is 4089fd... and proposition id is 2d01eb...
L133
Axiom. (Quaternion_k_i) We take the following as an axiom:
k ⨯ i = j
In Proofgold the corresponding term root is 7fb308... and proposition id is da5ded...
L134
Axiom. (Quaternion_j_i) We take the following as an axiom:
j ⨯ i = :-: k
In Proofgold the corresponding term root is 134bae... and proposition id is 411eda...
L135
Axiom. (Quaternion_k_j) We take the following as an axiom:
k ⨯ j = :-: i
In Proofgold the corresponding term root is a2b355... and proposition id is 80ed56...
L136
Axiom. (Quaternion_i_k) We take the following as an axiom:
i ⨯ k = :-: j
In Proofgold the corresponding term root is 987b31... and proposition id is 0343db...
L137
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
In Proofgold the corresponding term root is ef39c1... and proposition id is 271f1c...
L138
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
In Proofgold the corresponding term root is caf07e... and proposition id is 0a85fc...
L139
Axiom. (mul_HSNo_assoc) We take the following as an axiom:
∀z w v, HSNo z → HSNo w → HSNo v → z ⨯ (w ⨯ v) = (z ⨯ w) ⨯ v
In Proofgold the corresponding term root is 75e0e2... and proposition id is 980dee...
L140
Axiom. (conj_HSNo_i) We take the following as an axiom:
i '' = :-: i
In Proofgold the corresponding term root is 04e5d9... and proposition id is f2cf1e...
L141
Axiom. (conj_HSNo_j) We take the following as an axiom:
j '' = :-: j
In Proofgold the corresponding term root is 6cfb40... and proposition id is b0aea8...
L142
Axiom. (conj_HSNo_k) We take the following as an axiom:
k '' = :-: k
In Proofgold the corresponding term root is dfb947... and proposition id is 1f19c7...
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.
L148
Let i ≝ Complex_i
L149
Let j ≝ Quaternion_j
L150
Let k ≝ Quaternion_k
L151
Let p0 : set → set ≝ HSNo_proj0
L152
Let p1 : set → set ≝ HSNo_proj1
L153
Let pa : set → set → set ≝ CSNo_pair
L154
Definition. We define quaternion to be {pa (u 0) (u 1)|u ∈ complex ⨯ complex} of type set.
In Proofgold the corresponding term root is dfa313... and object id is d9a819...
L155
Axiom. (quaternion_I) We take the following as an axiom:
∀x y ∈ complex, pa x y ∈ quaternion
In Proofgold the corresponding term root is 5f5747... and proposition id is afcd2e...
L156
Axiom. (quaternion_E) We take the following as an axiom:
∀z ∈ quaternion, ∀p : prop, (∀x y ∈ complex, z = pa x y → p) → p
In Proofgold the corresponding term root is 6a5a42... and proposition id is f4d94d...
L157
Axiom. (quaternion_HSNo) We take the following as an axiom:
∀z ∈ quaternion, HSNo z
In Proofgold the corresponding term root is 076f3c... and proposition id is 0af764...
L158
Axiom. (complex_quaternion) We take the following as an axiom:
complex ⊆ quaternion
In Proofgold the corresponding term root is a6a6d6... and proposition id is da2811...
L159
Axiom. (quaternion_0) We take the following as an axiom:
0 ∈ quaternion
In Proofgold the corresponding term root is e063de... and proposition id is ff7551...
L160
Axiom. (quaternion_1) We take the following as an axiom:
1 ∈ quaternion
In Proofgold the corresponding term root is 82d4bb... and proposition id is f8553f...
L161
Axiom. (quaternion_i) We take the following as an axiom:
i ∈ quaternion
In Proofgold the corresponding term root is 2065ce... and proposition id is 885152...
L162
Axiom. (quaternion_j) We take the following as an axiom:
j ∈ quaternion
In Proofgold the corresponding term root is 66ccff... and proposition id is 539f92...
L163
Axiom. (quaternion_k) We take the following as an axiom:
k ∈ quaternion
In Proofgold the corresponding term root is 8d9436... and proposition id is 57d22f...
L164
Axiom. (quaternion_p0_eq) We take the following as an axiom:
∀x y ∈ complex, p0 (pa x y) = x
In Proofgold the corresponding term root is ffc962... and proposition id is be9c4d...
L165
Axiom. (quaternion_p1_eq) We take the following as an axiom:
∀x y ∈ complex, p1 (pa x y) = y
In Proofgold the corresponding term root is f0d565... and proposition id is 24c854...
L166
Axiom. (quaternion_p0_complex) We take the following as an axiom:
∀z ∈ quaternion, p0 z ∈ complex
In Proofgold the corresponding term root is a3df14... and proposition id is e1e097...
L167
Axiom. (quaternion_p1_complex) We take the following as an axiom:
∀z ∈ quaternion, p1 z ∈ complex
In Proofgold the corresponding term root is ac15b9... and proposition id is 32dd4d...
L168
Axiom. (quaternion_proj0proj1_split) We take the following as an axiom:
∀z w ∈ quaternion, p0 z = p0 w → p1 z = p1 w → z = w
In Proofgold the corresponding term root is 7d655c... and proposition id is 26e60b...
L169
Axiom. (quaternion_minus_HSNo) We take the following as an axiom:
∀z ∈ quaternion, - z ∈ quaternion
In Proofgold the corresponding term root is 8bff4e... and proposition id is df6a64...
L170
Axiom. (quaternion_conj_HSNo) We take the following as an axiom:
∀z ∈ quaternion, conj_HSNo z ∈ quaternion
In Proofgold the corresponding term root is ef83a8... and proposition id is 51db63...
L171
Axiom. (quaternion_add_HSNo) We take the following as an axiom:
∀z w ∈ quaternion, z + w ∈ quaternion
In Proofgold the corresponding term root is 2c4b19... and proposition id is 93e3ed...
L172
Axiom. (quaternion_mul_HSNo) We take the following as an axiom:
∀z w ∈ quaternion, z * w ∈ quaternion
In Proofgold the corresponding term root is c05871... and proposition id is f8fd5d...
L173
Axiom. (complex_p0_eq) We take the following as an axiom:
∀x ∈ complex, p0 x = x
In Proofgold the corresponding term root is 6a7777... and proposition id is 3e2e1f...
L174
Axiom. (complex_p1_eq) We take the following as an axiom:
∀x ∈ complex, p1 x = 0
In Proofgold the corresponding term root is 498737... and proposition id is d0861d...
End of Section Quaternions