Beginning of Section SurQuaternions
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** $I sig/Part4.mgs ***)
(*** $I sig/Part5.mgs ***)
(*** $I sig/Part6.mgs ***)
(*** $I sig/Part7.mgs ***)
(*** $I sig/Part8.mgs ***)
(*** $I sig/Part9.mgs ***)
(*** $I sig/Part10.mgs ***)
(*** $I sig/Part11.mgs ***)
(*** $I sig/Part12.mgs ***)
L15
Theorem. (quaternion_tag_fresh)
∀z, CSNo z → ∀u ∈ z, {3} ∉ u
In Proofgold the corresponding term root is 202f04... and proposition id is cbed07...
Proof:
Proof not loaded.
(*** Part 13 ***)
L22
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...
L24
Theorem. (CSNo_pair_0)
∀x, CSNo_pair x 0 = x
In Proofgold the corresponding term root is 4db8eb... and proposition id is abfae9...
Proof:
Proof not loaded.
L28
Theorem. (CSNo_pair_prop_1)
∀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...
Proof:
Proof not loaded.
L32
Theorem. (CSNo_pair_prop_2)
∀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...
Proof:
Proof not loaded.
L36
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...
L38
Theorem. (HSNo_I)
∀x y, CSNo x → CSNo y → HSNo (CSNo_pair x y)
In Proofgold the corresponding term root is 17ad60... and proposition id is 8476c5...
Proof:
Proof not loaded.
L42
Theorem. (HSNo_E)
∀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...
Proof:
Proof not loaded.
L49
Theorem. (CSNo_HSNo)
∀x, CSNo x → HSNo x
In Proofgold the corresponding term root is 307398... and proposition id is 0db147...
Proof:
Proof not loaded.
L53
Theorem. (HSNo_0)
HSNo 0
In Proofgold the corresponding term root is 27cacb... and proposition id is d3c9ac...
Proof:
Proof not loaded.
L57
Theorem. (HSNo_1)
HSNo 1
In Proofgold the corresponding term root is 3065de... and proposition id is ca7c07...
Proof:
Proof not loaded.
L61
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {3}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
L64
Theorem. (HSNo_ExtendedSNoElt_4)
∀z, HSNo z → ExtendedSNoElt_ 4 z
In Proofgold the corresponding term root is 4407d8... and proposition id is d88675...
Proof:
Proof not loaded.
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.
L109
Let i ≝ Complex_i
L111
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...
L112
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...
L113
Let j ≝ Quaternion_j
L115
Let k ≝ Quaternion_k
L116
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...
L118
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...
L119
Let p0 : set → set ≝ HSNo_proj0
L121
Let p1 : set → set ≝ HSNo_proj1
L122
Let pa : set → set → set ≝ CSNo_pair
L123
Theorem. (HSNo_proj0_1)
∀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...
Proof:
Proof not loaded.
L127
Theorem. (HSNo_proj0_2)
∀x y, CSNo x → CSNo y → p0 (pa x y) = x
In Proofgold the corresponding term root is 9ffb4a... and proposition id is 57a042...
Proof:
Proof not loaded.
L131
Theorem. (HSNo_proj1_1)
∀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...
Proof:
Proof not loaded.
L135
Theorem. (HSNo_proj1_2)
∀x y, CSNo x → CSNo y → p1 (pa x y) = y
In Proofgold the corresponding term root is 2c4d65... and proposition id is b8596e...
Proof:
Proof not loaded.
L139
Theorem. (HSNo_proj0R)
∀z, HSNo z → CSNo (p0 z)
In Proofgold the corresponding term root is dfba9c... and proposition id is d5b6be...
Proof:
Proof not loaded.
L143
Theorem. (HSNo_proj1R)
∀z, HSNo z → CSNo (p1 z)
In Proofgold the corresponding term root is 88c956... and proposition id is 4c5b7f...
Proof:
Proof not loaded.
L147
Theorem. (HSNo_proj0p1)
∀z, HSNo z → z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is 099ef1... and proposition id is cd06de...
Proof:
Proof not loaded.
L151
Theorem. (HSNo_proj0proj1_split)
∀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...
Proof:
Proof not loaded.
L155
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...
L157
Theorem. (HSNoLev_ordinal)
∀z, HSNo z → ordinal (HSNoLev z)
In Proofgold the corresponding term root is 5fdf84... and proposition id is c12b44...
Proof:
Proof not loaded.
L170
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...
L172
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...
L173
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...
L174
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...
L175
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...
L176
Let plus' ≝ add_HSNo
L178
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.
L185
Theorem. (HSNo_Complex_i)
HSNo i
In Proofgold the corresponding term root is 1c2523... and proposition id is 9eee28...
Proof:
Proof not loaded.
L189
Theorem. (HSNo_Quaternion_j)
HSNo j
In Proofgold the corresponding term root is 498a34... and proposition id is 4e668f...
Proof:
Proof not loaded.
L196
Theorem. (HSNo_Quaternion_k)
HSNo k
In Proofgold the corresponding term root is 5a2d44... and proposition id is 7b6e43...
Proof:
Proof not loaded.
L203
Theorem. (HSNo_minus_HSNo)
∀z, HSNo z → HSNo (minus_HSNo z)
In Proofgold the corresponding term root is e82f65... and proposition id is f8d185...
Proof:
Proof not loaded.
L207
Theorem. (minus_HSNo_proj0)
∀z, HSNo z → p0 (:-: z) = - p0 z
In Proofgold the corresponding term root is 0f68d7... and proposition id is b166fc...
Proof:
Proof not loaded.
L211
Theorem. (minus_HSNo_proj1)
∀z, HSNo z → p1 (:-: z) = - p1 z
In Proofgold the corresponding term root is 26353b... and proposition id is bd1384...
Proof:
Proof not loaded.
L215
Theorem. (HSNo_conj_HSNo)
∀z, HSNo z → HSNo (conj_HSNo z)
In Proofgold the corresponding term root is 2747f5... and proposition id is 67a2db...
Proof:
Proof not loaded.
L219
Theorem. (conj_HSNo_proj0)
∀z, HSNo z → p0 (z '') = (p0 z) '
In Proofgold the corresponding term root is c3731a... and proposition id is b3ff6d...
Proof:
Proof not loaded.
L223
Theorem. (conj_HSNo_proj1)
∀z, HSNo z → p1 (z '') = - p1 z
In Proofgold the corresponding term root is 07def3... and proposition id is 686476...
Proof:
Proof not loaded.
L227
Theorem. (HSNo_add_HSNo)
∀z w, HSNo z → HSNo w → HSNo (add_HSNo z w)
In Proofgold the corresponding term root is 37bb2a... and proposition id is 1f7aba...
Proof:
Proof not loaded.
L231
Theorem. (add_HSNo_proj0)
∀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...
Proof:
Proof not loaded.
L235
Theorem. (add_HSNo_proj1)
∀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...
Proof:
Proof not loaded.
L239
Theorem. (HSNo_mul_HSNo)
∀z w, HSNo z → HSNo w → HSNo (z ⨯ w)
In Proofgold the corresponding term root is 25d347... and proposition id is 5382cd...
Proof:
Proof not loaded.
L243
Theorem. (mul_HSNo_proj0)
∀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...
Proof:
Proof not loaded.
L247
Theorem. (mul_HSNo_proj1)
∀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...
Proof:
Proof not loaded.
L251
Theorem. (CSNo_HSNo_proj0)
∀x, CSNo x → p0 x = x
In Proofgold the corresponding term root is 60fe35... and proposition id is 7639bd...
Proof:
Proof not loaded.
L255
Theorem. (CSNo_HSNo_proj1)
∀x, CSNo x → p1 x = 0
In Proofgold the corresponding term root is 15d87b... and proposition id is 952144...
Proof:
Proof not loaded.
L259
Theorem. (HSNo_p0_0)
p0 0 = 0
In Proofgold the corresponding term root is 6b350d... and proposition id is f0ff58...
Proof:
Proof not loaded.
L263
Theorem. (HSNo_p1_0)
p1 0 = 0
In Proofgold the corresponding term root is ba0409... and proposition id is 1878d5...
Proof:
Proof not loaded.
L267
Theorem. (HSNo_p0_1)
p0 1 = 1
In Proofgold the corresponding term root is 4dd8fa... and proposition id is b0bea3...
Proof:
Proof not loaded.
L271
Theorem. (HSNo_p1_1)
p1 1 = 0
In Proofgold the corresponding term root is 93fc91... and proposition id is 3f14ef...
Proof:
Proof not loaded.
L275
Theorem. (HSNo_p0_i)
p0 i = i
In Proofgold the corresponding term root is 905afa... and proposition id is 50a227...
Proof:
Proof not loaded.
L279
Theorem. (HSNo_p1_i)
p1 i = 0
In Proofgold the corresponding term root is 768a8d... and proposition id is 7ea9df...
Proof:
Proof not loaded.
L283
Theorem. (HSNo_p0_j)
p0 j = 0
In Proofgold the corresponding term root is 767fd7... and proposition id is 21c475...
Proof:
Proof not loaded.
L287
Theorem. (HSNo_p1_j)
p1 j = 1
In Proofgold the corresponding term root is 3b95bd... and proposition id is abaaec...
Proof:
Proof not loaded.
L291
Theorem. (HSNo_p0_k)
p0 k = 0
In Proofgold the corresponding term root is e603b4... and proposition id is 8baec9...
Proof:
Proof not loaded.
L295
Theorem. (HSNo_p1_k)
p1 k = i
In Proofgold the corresponding term root is 80ea56... and proposition id is 575ab4...
Proof:
Proof not loaded.
L299
Theorem. (minus_HSNo_minus_CSNo)
∀x, CSNo x → :-: x = - x
In Proofgold the corresponding term root is a9014c... and proposition id is 7b42d4...
Proof:
Proof not loaded.
L303
Theorem. (minus_HSNo_0)
:-: 0 = 0
In Proofgold the corresponding term root is 176f59... and proposition id is 776989...
Proof:
Proof not loaded.
L308
Theorem. (conj_HSNo_conj_CSNo)
∀x, CSNo x → x '' = x '
In Proofgold the corresponding term root is 64571f... and proposition id is 7817d5...
Proof:
Proof not loaded.
L312
Theorem. (conj_HSNo_id_SNo)
∀x, SNo x → x '' = x
In Proofgold the corresponding term root is ebe6df... and proposition id is 58d64a...
Proof:
Proof not loaded.
L319
Theorem. (conj_HSNo_0)
0 '' = 0
In Proofgold the corresponding term root is 0665e6... and proposition id is 1a59ff...
Proof:
Proof not loaded.
L324
Theorem. (conj_HSNo_1)
1 '' = 1
In Proofgold the corresponding term root is 6faceb... and proposition id is 3cd551...
Proof:
Proof not loaded.
L329
Theorem. (add_HSNo_add_CSNo)
∀x y, CSNo x → CSNo y → x + y = x + y
In Proofgold the corresponding term root is 6e3971... and proposition id is b05210...
Proof:
Proof not loaded.
L333
Theorem. (mul_HSNo_mul_CSNo)
∀x y, CSNo x → CSNo y → x ⨯ y = x * y
In Proofgold the corresponding term root is c8a0d0... and proposition id is e84c3f...
Proof:
Proof not loaded.
L337
Theorem. (minus_HSNo_invol)
∀z, HSNo z → :-: :-: z = z
In Proofgold the corresponding term root is 91a264... and proposition id is d5104e...
Proof:
Proof not loaded.
L341
Theorem. (conj_HSNo_invol)
∀z, HSNo z → z '' '' = z
In Proofgold the corresponding term root is 8faa1e... and proposition id is 3cc997...
Proof:
Proof not loaded.
L345
Theorem. (conj_minus_HSNo)
∀z, HSNo z → (:-: z) '' = :-: (z '')
In Proofgold the corresponding term root is ad72ab... and proposition id is 97ffd3...
Proof:
Proof not loaded.
L349
Theorem. (minus_add_HSNo)
∀z w, HSNo z → HSNo w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is ea90cf... and proposition id is 5c75f8...
Proof:
Proof not loaded.
L353
Theorem. (conj_add_HSNo)
∀z w, HSNo z → HSNo w → (z + w) '' = z '' + w ''
In Proofgold the corresponding term root is 777e84... and proposition id is ec65d2...
Proof:
Proof not loaded.
L357
Theorem. (add_HSNo_com)
∀z w, HSNo z → HSNo w → z + w = w + z
In Proofgold the corresponding term root is e30f23... and proposition id is a91741...
Proof:
Proof not loaded.
L361
Theorem. (add_HSNo_assoc)
∀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...
Proof:
Proof not loaded.
L365
Theorem. (add_HSNo_0L)
∀z, HSNo z → add_HSNo 0 z = z
In Proofgold the corresponding term root is 18376d... and proposition id is 1b0119...
Proof:
Proof not loaded.
L369
Theorem. (add_HSNo_0R)
∀z, HSNo z → add_HSNo z 0 = z
In Proofgold the corresponding term root is 5a9044... and proposition id is 0c0186...
Proof:
Proof not loaded.
L373
Theorem. (add_HSNo_minus_HSNo_linv)
∀z, HSNo z → add_HSNo (minus_HSNo z) z = 0
In Proofgold the corresponding term root is 2161be... and proposition id is c0a796...
Proof:
Proof not loaded.
L377
Theorem. (add_HSNo_minus_HSNo_rinv)
∀z, HSNo z → add_HSNo z (minus_HSNo z) = 0
In Proofgold the corresponding term root is e16e72... and proposition id is f52141...
Proof:
Proof not loaded.
L381
Theorem. (mul_HSNo_0R)
∀z, HSNo z → z ⨯ 0 = 0
In Proofgold the corresponding term root is c6c5df... and proposition id is a6c3c2...
Proof:
Proof not loaded.
L385
Theorem. (mul_HSNo_0L)
∀z, HSNo z → 0 ⨯ z = 0
In Proofgold the corresponding term root is d9f510... and proposition id is 2984ec...
Proof:
Proof not loaded.
L389
Theorem. (mul_HSNo_1R)
∀z, HSNo z → z ⨯ 1 = z
In Proofgold the corresponding term root is ec38b4... and proposition id is 896e80...
Proof:
Proof not loaded.
L393
Theorem. (mul_HSNo_1L)
∀z, HSNo z → 1 ⨯ z = z
In Proofgold the corresponding term root is 80a90e... and proposition id is 4c64b4...
Proof:
Proof not loaded.
L397
Theorem. (conj_mul_HSNo)
∀z w, HSNo z → HSNo w → (z ⨯ w) '' = w '' ⨯ z ''
In Proofgold the corresponding term root is 64a2e5... and proposition id is 225be1...
Proof:
Proof not loaded.
L401
Theorem. (mul_HSNo_distrL)
∀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...
Proof:
Proof not loaded.
L405
Theorem. (mul_HSNo_distrR)
∀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...
Proof:
Proof not loaded.
L409
Theorem. (minus_mul_HSNo_distrR)
∀z w, HSNo z → HSNo w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is e18e00... and proposition id is 122e5c...
Proof:
Proof not loaded.
L413
Theorem. (minus_mul_HSNo_distrL)
∀z w, HSNo z → HSNo w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is e48f25... and proposition id is e67e13...
Proof:
Proof not loaded.
L417
Theorem. (exp_HSNo_nat_0)
∀z, z0 = 1
In Proofgold the corresponding term root is a8e4e1... and proposition id is 858195...
Proof:
Proof not loaded.
L421
Theorem. (exp_HSNo_nat_S)
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
In Proofgold the corresponding term root is 5c2375... and proposition id is 5ccd45...
Proof:
Proof not loaded.
L425
Theorem. (exp_HSNo_nat_1)
∀z, HSNo z → z1 = z
In Proofgold the corresponding term root is 83d5ec... and proposition id is 209eff...
Proof:
Proof not loaded.
L429
Theorem. (exp_HSNo_nat_2)
∀z, HSNo z → z2 = z ⨯ z
In Proofgold the corresponding term root is 0756a0... and proposition id is dd7b0e...
Proof:
Proof not loaded.
L433
Theorem. (HSNo_exp_HSNo_nat)
∀z, HSNo z → ∀n, nat_p n → HSNo (zn)
In Proofgold the corresponding term root is dfb84a... and proposition id is cfcd35...
Proof:
Proof not loaded.
L437
Theorem. (add_CSNo_com_3b_1_2)
∀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...
Proof:
Proof not loaded.
L450
Theorem. (add_CSNo_com_4_inner_mid)
∀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...
Proof:
Proof not loaded.
L461
Theorem. (add_CSNo_rotate_4_0312)
∀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...
Proof:
Proof not loaded.
L468
Theorem. (Quaternion_i_sqr)
i ⨯ i = :-: 1
In Proofgold the corresponding term root is ab7a70... and proposition id is 6ce0c7...
Proof:
Proof not loaded.
L475
Theorem. (Quaternion_j_sqr)
j ⨯ j = :-: 1
In Proofgold the corresponding term root is b4236f... and proposition id is 9f0956...
Proof:
Proof not loaded.
L507
Theorem. (Quaternion_k_sqr)
k ⨯ k = :-: 1
In Proofgold the corresponding term root is 0298ee... and proposition id is c4384d...
Proof:
Proof not loaded.
L544
Theorem. (Quaternion_i_j)
i ⨯ j = k
In Proofgold the corresponding term root is 0337aa... and proposition id is b64eb9...
Proof:
Proof not loaded.
L571
Theorem. (Quaternion_j_k)
j ⨯ k = i
In Proofgold the corresponding term root is 4089fd... and proposition id is 2d01eb...
Proof:
Proof not loaded.
L600
Theorem. (Quaternion_k_i)
k ⨯ i = j
In Proofgold the corresponding term root is 7fb308... and proposition id is da5ded...
Proof:
Proof not loaded.
L633
Theorem. (Quaternion_j_i)
j ⨯ i = :-: k
In Proofgold the corresponding term root is 134bae... and proposition id is 411eda...
Proof:
Proof not loaded.
L663
Theorem. (Quaternion_k_j)
k ⨯ j = :-: i
In Proofgold the corresponding term root is a2b355... and proposition id is 80ed56...
Proof:
Proof not loaded.
L693
Theorem. (Quaternion_i_k)
i ⨯ k = :-: j
In Proofgold the corresponding term root is 987b31... and proposition id is 0343db...
Proof:
Proof not loaded.
L721
Theorem. (add_CSNo_rotate_3_1)
∀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...
Proof:
Proof not loaded.
L735
Theorem. (mul_CSNo_rotate_3_1)
∀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...
Proof:
Proof not loaded.
L749
Theorem. (mul_HSNo_assoc)
∀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...
Proof:
Proof not loaded.
L1325
Theorem. (conj_HSNo_i)
i '' = :-: i
In Proofgold the corresponding term root is 04e5d9... and proposition id is f2cf1e...
Proof:
Proof not loaded.
L1332
Theorem. (conj_HSNo_j)
j '' = :-: j
In Proofgold the corresponding term root is 6cfb40... and proposition id is b0aea8...
Proof:
Proof not loaded.
L1349
Theorem. (conj_HSNo_k)
k '' = :-: k
In Proofgold the corresponding term root is dfb947... and proposition id is 1f19c7...
Proof:
Proof not loaded.
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.
L1374
Let i ≝ Complex_i
L1376
Let j ≝ Quaternion_j
L1377
Let k ≝ Quaternion_k
L1378
Let p0 : set → set ≝ HSNo_proj0
L1379
Let p1 : set → set ≝ HSNo_proj1
L1380
Let pa : set → set → set ≝ CSNo_pair
L1381
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...
L1383
Theorem. (quaternion_I)
∀x y ∈ complex, pa x y ∈ quaternion
In Proofgold the corresponding term root is 5f5747... and proposition id is afcd2e...
Proof:
Proof not loaded.
L1394
Theorem. (quaternion_E)
∀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...
Proof:
Proof not loaded.
L1407
Theorem. (quaternion_HSNo)
∀z ∈ quaternion, HSNo z
In Proofgold the corresponding term root is 076f3c... and proposition id is 0af764...
Proof:
Proof not loaded.
L1418
Theorem. (complex_quaternion)
complex ⊆ quaternion
In Proofgold the corresponding term root is a6a6d6... and proposition id is da2811...
Proof:
Proof not loaded.
L1428
Theorem. (quaternion_0)
0 ∈ quaternion
In Proofgold the corresponding term root is e063de... and proposition id is ff7551...
Proof:
Proof not loaded.
L1432
Theorem. (quaternion_1)
1 ∈ quaternion
In Proofgold the corresponding term root is 82d4bb... and proposition id is f8553f...
Proof:
Proof not loaded.
L1436
Theorem. (quaternion_i)
i ∈ quaternion
In Proofgold the corresponding term root is 2065ce... and proposition id is 885152...
Proof:
Proof not loaded.
L1440
Theorem. (quaternion_j)
j ∈ quaternion
In Proofgold the corresponding term root is 66ccff... and proposition id is 539f92...
Proof:
Proof not loaded.
L1447
Theorem. (quaternion_k)
k ∈ quaternion
In Proofgold the corresponding term root is 8d9436... and proposition id is 57d22f...
Proof:
Proof not loaded.
L1454
Theorem. (quaternion_p0_eq)
∀x y ∈ complex, p0 (pa x y) = x
In Proofgold the corresponding term root is ffc962... and proposition id is be9c4d...
Proof:
Proof not loaded.
L1459
Theorem. (quaternion_p1_eq)
∀x y ∈ complex, p1 (pa x y) = y
In Proofgold the corresponding term root is f0d565... and proposition id is 24c854...
Proof:
Proof not loaded.
L1464
Theorem. (quaternion_p0_complex)
∀z ∈ quaternion, p0 z ∈ complex
In Proofgold the corresponding term root is a3df14... and proposition id is e1e097...
Proof:
Proof not loaded.
L1473
Theorem. (quaternion_p1_complex)
∀z ∈ quaternion, p1 z ∈ complex
In Proofgold the corresponding term root is ac15b9... and proposition id is 32dd4d...
Proof:
Proof not loaded.
L1482
Theorem. (quaternion_proj0proj1_split)
∀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...
Proof:
Proof not loaded.
L1487
Theorem. (quaternion_minus_HSNo)
∀z ∈ quaternion, - z ∈ quaternion
In Proofgold the corresponding term root is 8bff4e... and proposition id is df6a64...
Proof:
Proof not loaded.
L1495
Theorem. (quaternion_conj_HSNo)
∀z ∈ quaternion, conj_HSNo z ∈ quaternion
In Proofgold the corresponding term root is ef83a8... and proposition id is 51db63...
Proof:
Proof not loaded.
L1503
Theorem. (quaternion_add_HSNo)
∀z w ∈ quaternion, z + w ∈ quaternion
In Proofgold the corresponding term root is 2c4b19... and proposition id is 93e3ed...
Proof:
Proof not loaded.
L1515
Theorem. (quaternion_mul_HSNo)
∀z w ∈ quaternion, z * w ∈ quaternion
In Proofgold the corresponding term root is c05871... and proposition id is f8fd5d...
Proof:
Proof not loaded.
L1545
Theorem. (complex_p0_eq)
∀x ∈ complex, p0 x = x
In Proofgold the corresponding term root is 6a7777... and proposition id is 3e2e1f...
Proof:
Proof not loaded.
L1551
Theorem. (complex_p1_eq)
∀x ∈ complex, p1 x = 0
In Proofgold the corresponding term root is 498737... and proposition id is d0861d...
Proof:
Proof not loaded.
End of Section Quaternions