Beginning of Section SurQuaternions

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.

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...

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.

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.

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.

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...

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.

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.

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.

Theorem. (HSNo_0)

HSNo 0

In Proofgold the corresponding term root is 27cacb... and proposition id is d3c9ac...

Proof:
Proof not loaded.

Theorem. (HSNo_1)

HSNo 1

In Proofgold the corresponding term root is 3065de... and proposition id is ca7c07...

Proof:
Proof not loaded.

Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {3}

Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.

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.

Let i ≝ Complex_i

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...

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...

Let j ≝ Quaternion_j

Let k ≝ Quaternion_k

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...

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...

Let p0 : set → set ≝ HSNo_proj0

Let p1 : set → set ≝ HSNo_proj1

Let pa : set → set → set ≝ CSNo_pair

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.

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.

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.

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.

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.

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.

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.

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.

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...

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.

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...

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...

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...

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...

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...

Let plus' ≝ add_HSNo

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.

Theorem. (HSNo_Complex_i)

HSNo i

In Proofgold the corresponding term root is 1c2523... and proposition id is 9eee28...

Proof:
Proof not loaded.

Theorem. (HSNo_Quaternion_j)

HSNo j

In Proofgold the corresponding term root is 498a34... and proposition id is 4e668f...

Proof:
Proof not loaded.

Theorem. (HSNo_Quaternion_k)

HSNo k

In Proofgold the corresponding term root is 5a2d44... and proposition id is 7b6e43...

Proof:
Proof not loaded.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Theorem. (HSNo_p0_0)

p0 0 = 0

In Proofgold the corresponding term root is 6b350d... and proposition id is f0ff58...

Proof:
Proof not loaded.

Theorem. (HSNo_p1_0)

p1 0 = 0

In Proofgold the corresponding term root is ba0409... and proposition id is 1878d5...

Proof:
Proof not loaded.

Theorem. (HSNo_p0_1)

p0 1 = 1

In Proofgold the corresponding term root is 4dd8fa... and proposition id is b0bea3...

Proof:
Proof not loaded.

Theorem. (HSNo_p1_1)

p1 1 = 0

In Proofgold the corresponding term root is 93fc91... and proposition id is 3f14ef...

Proof:
Proof not loaded.

Theorem. (HSNo_p0_i)

p0 i = i

In Proofgold the corresponding term root is 905afa... and proposition id is 50a227...

Proof:
Proof not loaded.

Theorem. (HSNo_p1_i)

p1 i = 0

In Proofgold the corresponding term root is 768a8d... and proposition id is 7ea9df...

Proof:
Proof not loaded.

Theorem. (HSNo_p0_j)

p0 j = 0

In Proofgold the corresponding term root is 767fd7... and proposition id is 21c475...

Proof:
Proof not loaded.

Theorem. (HSNo_p1_j)

p1 j = 1

In Proofgold the corresponding term root is 3b95bd... and proposition id is abaaec...

Proof:
Proof not loaded.

Theorem. (HSNo_p0_k)

p0 k = 0

In Proofgold the corresponding term root is e603b4... and proposition id is 8baec9...

Proof:
Proof not loaded.

Theorem. (HSNo_p1_k)

p1 k = i

In Proofgold the corresponding term root is 80ea56... and proposition id is 575ab4...

Proof:
Proof not loaded.

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.

Theorem. (minus_HSNo_0)

:-: 0 = 0

In Proofgold the corresponding term root is 176f59... and proposition id is 776989...

Proof:
Proof not loaded.

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.

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.

Theorem. (conj_HSNo_0)

0 '' = 0

In Proofgold the corresponding term root is 0665e6... and proposition id is 1a59ff...

Proof:
Proof not loaded.

Theorem. (conj_HSNo_1)

1 '' = 1

In Proofgold the corresponding term root is 6faceb... and proposition id is 3cd551...

Proof:
Proof not loaded.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Theorem. (exp_HSNo_nat_0)

∀z, z⁰ = 1

In Proofgold the corresponding term root is a8e4e1... and proposition id is 858195...

Proof:
Proof not loaded.

Theorem. (exp_HSNo_nat_S)

∀z n, nat_p n → z^{(ordsucc n)} = z ⨯ zⁿ

In Proofgold the corresponding term root is 5c2375... and proposition id is 5ccd45...

Proof:
Proof not loaded.

Theorem. (exp_HSNo_nat_1)

∀z, HSNo z → z¹ = z

In Proofgold the corresponding term root is 83d5ec... and proposition id is 209eff...

Proof:
Proof not loaded.

Theorem. (exp_HSNo_nat_2)

∀z, HSNo z → z² = z ⨯ z

In Proofgold the corresponding term root is 0756a0... and proposition id is dd7b0e...

Proof:
Proof not loaded.

Theorem. (HSNo_exp_HSNo_nat)

∀z, HSNo z → ∀n, nat_p n → HSNo (zⁿ)

In Proofgold the corresponding term root is dfb84a... and proposition id is cfcd35...

Proof:
Proof not loaded.

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.

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.

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.

Theorem. (Quaternion_i_sqr)

i ⨯ i = :-: 1

In Proofgold the corresponding term root is ab7a70... and proposition id is 6ce0c7...

Proof:
Proof not loaded.

Theorem. (Quaternion_j_sqr)

j ⨯ j = :-: 1

In Proofgold the corresponding term root is b4236f... and proposition id is 9f0956...

Proof:
Proof not loaded.

Theorem. (Quaternion_k_sqr)

k ⨯ k = :-: 1

In Proofgold the corresponding term root is 0298ee... and proposition id is c4384d...

Proof:
Proof not loaded.

Theorem. (Quaternion_i_j)

i ⨯ j = k

In Proofgold the corresponding term root is 0337aa... and proposition id is b64eb9...

Proof:
Proof not loaded.

Theorem. (Quaternion_j_k)

j ⨯ k = i

In Proofgold the corresponding term root is 4089fd... and proposition id is 2d01eb...

Proof:
Proof not loaded.

Theorem. (Quaternion_k_i)

k ⨯ i = j

In Proofgold the corresponding term root is 7fb308... and proposition id is da5ded...

Proof:
Proof not loaded.

Theorem. (Quaternion_j_i)

j ⨯ i = :-: k

In Proofgold the corresponding term root is 134bae... and proposition id is 411eda...

Proof:
Proof not loaded.

Theorem. (Quaternion_k_j)

k ⨯ j = :-: i

In Proofgold the corresponding term root is a2b355... and proposition id is 80ed56...

Proof:
Proof not loaded.

Theorem. (Quaternion_i_k)

i ⨯ k = :-: j

In Proofgold the corresponding term root is 987b31... and proposition id is 0343db...

Proof:
Proof not loaded.

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.

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.

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.

Theorem. (conj_HSNo_i)

i '' = :-: i

In Proofgold the corresponding term root is 04e5d9... and proposition id is f2cf1e...

Proof:
Proof not loaded.

Theorem. (conj_HSNo_j)

j '' = :-: j

In Proofgold the corresponding term root is 6cfb40... and proposition id is b0aea8...

Proof:
Proof not loaded.

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.

Let i ≝ Complex_i

Let j ≝ Quaternion_j

Let k ≝ Quaternion_k

Let p0 : set → set ≝ HSNo_proj0

Let p1 : set → set ≝ HSNo_proj1

Let pa : set → set → set ≝ CSNo_pair

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...

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.

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.

Theorem. (quaternion_HSNo)

∀z ∈ quaternion, HSNo z

In Proofgold the corresponding term root is 076f3c... and proposition id is 0af764...

Proof:
Proof not loaded.

Theorem. (complex_quaternion)

complex ⊆ quaternion

In Proofgold the corresponding term root is a6a6d6... and proposition id is da2811...

Proof:
Proof not loaded.

Theorem. (quaternion_0)

0 ∈ quaternion

In Proofgold the corresponding term root is e063de... and proposition id is ff7551...

Proof:
Proof not loaded.

Theorem. (quaternion_1)

1 ∈ quaternion

In Proofgold the corresponding term root is 82d4bb... and proposition id is f8553f...

Proof:
Proof not loaded.

Theorem. (quaternion_i)

i ∈ quaternion

In Proofgold the corresponding term root is 2065ce... and proposition id is 885152...

Proof:
Proof not loaded.

Theorem. (quaternion_j)

j ∈ quaternion

In Proofgold the corresponding term root is 66ccff... and proposition id is 539f92...

Proof:
Proof not loaded.

Theorem. (quaternion_k)

k ∈ quaternion

In Proofgold the corresponding term root is 8d9436... and proposition id is 57d22f...

Proof:
Proof not loaded.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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