Beginning of Section SurOctonions
Theorem. (octonion_tag_fresh)
∀x, HSNo x → ∀u ∈ x, {4} ∉ u
In Proofgold the corresponding term root is b25e72... and proposition id is 9cf79c...
Proof:
Let z be given.
Assume Hz.
Apply Sing_nat_fresh_extension 4 nat_4 In_1_4 z to the current goal.
We will prove ExtendedSNoElt_ 4 z.
An exact proof term for the current goal is HSNo_ExtendedSNoElt_4 z Hz.
∎
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...
Theorem. (HSNo_pair_0)
∀x, HSNo_pair x 0 = x
In Proofgold the corresponding term root is 121f87... and proposition id is 367405...
Proof:
An exact proof term for the current goal is pair_tag_0 {4} HSNo octonion_tag_fresh.
∎
Theorem. (HSNo_pair_prop_1)
∀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...
Proof:
An exact proof term for the current goal is pair_tag_prop_1 {4} HSNo octonion_tag_fresh.
∎
Theorem. (HSNo_pair_prop_2)
∀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...
Proof:
An exact proof term for the current goal is pair_tag_prop_2 {4} HSNo octonion_tag_fresh.
∎
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...
Theorem. (OSNo_I)
∀x y, HSNo x → HSNo y → OSNo (HSNo_pair x y)
In Proofgold the corresponding term root is afb109... and proposition id is 1fdc97...
Proof:
An exact proof term for the current goal is CD_carr_I {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_E)
∀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...
Proof:
An exact proof term for the current goal is CD_carr_E {4} HSNo octonion_tag_fresh.
∎
Theorem. (HSNo_OSNo)
∀x, HSNo x → OSNo x
In Proofgold the corresponding term root is 4fae92... and proposition id is 097009...
Proof:
An exact proof term for the current goal is CD_carr_0ext {4} HSNo octonion_tag_fresh HSNo_0.
∎
Theorem. (OSNo_0)
OSNo 0
In Proofgold the corresponding term root is 6ebd11... and proposition id is 819fb5...
Proof:
Apply HSNo_OSNo to the current goal.
An exact proof term for the current goal is HSNo_0.
∎
Theorem. (OSNo_1)
OSNo 1
In Proofgold the corresponding term root is 76552d... and proposition id is a6d6f8...
Proof:
Apply HSNo_OSNo to the current goal.
An exact proof term for the current goal is HSNo_1.
∎
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {4}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
Theorem. (OSNo_ExtendedSNoElt_5)
∀z, OSNo z → ExtendedSNoElt_ 5 z
In Proofgold the corresponding term root is 5f1c66... and proposition id is 8a0ec8...
Proof:
Let z be given.
Assume Hz.
Apply OSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx: HSNo x.
Assume Hy: HSNo y.
Assume Hzxy: z = HSNo_pair x y.
Let v be given.
Assume Hv: v ∈ ⋃ (HSNo_pair x y).
Apply UnionE_impred (HSNo_pair x y) v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ HSNo_pair x y.
Apply binunionE x {w ''|w ∈ y} u H2 to the current goal.
Assume H3: u ∈ x.
We prove the intermediate claim L1: v ∈ ⋃ x.
An exact proof term for the current goal is UnionI x v u H1 H3.
We will prove ordinal v ∨ ∃i ∈ 5, v = {i}.
An exact proof term for the current goal is extension_SNoElt_mon 4 5 (ordsuccI1 4) x (HSNo_ExtendedSNoElt_4 x Hx) v L1.
Assume H3: u ∈ {w ''|w ∈ y}.
Apply ReplE_impred y ctag u H3 to the current goal.
Let w be given.
Assume Hw: w ∈ y.
Assume H4: u = w ''.
We prove the intermediate claim L2: v ∈ w ''.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE w {{4}} v L2 to the current goal.
Assume H5: v ∈ w.
We prove the intermediate claim L3: v ∈ ⋃ y.
An exact proof term for the current goal is UnionI y v w H5 Hw.
An exact proof term for the current goal is extension_SNoElt_mon 4 5 (ordsuccI1 4) y (HSNo_ExtendedSNoElt_4 y Hy) v L3.
Assume H5: v ∈ {{4}}.
We will prove ordinal v ∨ ∃i ∈ 5, v = {i}.
Apply orIR to the current goal.
We use 4 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 4 ∈ 5.
An exact proof term for the current goal is In_4_5.
We will prove v = {4}.
An exact proof term for the current goal is SingE {4} v H5.
∎
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_HSNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_HSNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_HSNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_HSNo.
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term conj_HSNo.
Let i ≝ Complex_i
Let j ≝ Quaternion_j
Let k ≝ Quaternion_k
Definition. We define OSNo_proj0 to be CD_proj0 {4} HSNo of type set → set.
In Proofgold the corresponding term root is 13b462... and object id is a29720...
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...
Let p0 : set → set ≝ OSNo_proj0
Let p1 : set → set ≝ OSNo_proj1
Let pa : set → set → set ≝ HSNo_pair
Theorem. (OSNo_proj0_1)
∀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...
Proof:
An exact proof term for the current goal is CD_proj0_1 {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj0_2)
∀x y, HSNo x → HSNo y → p0 (pa x y) = x
In Proofgold the corresponding term root is b97eaa... and proposition id is 37276d...
Proof:
An exact proof term for the current goal is CD_proj0_2 {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj1_1)
∀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...
Proof:
An exact proof term for the current goal is CD_proj1_1 {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj1_2)
∀x y, HSNo x → HSNo y → p1 (pa x y) = y
In Proofgold the corresponding term root is 00b55f... and proposition id is ad4890...
Proof:
An exact proof term for the current goal is CD_proj1_2 {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj0R)
∀z, OSNo z → HSNo (p0 z)
In Proofgold the corresponding term root is d79361... and proposition id is bb9e47...
Proof:
An exact proof term for the current goal is CD_proj0R {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj1R)
∀z, OSNo z → HSNo (p1 z)
In Proofgold the corresponding term root is 010b9d... and proposition id is 7e4dac...
Proof:
An exact proof term for the current goal is CD_proj1R {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj0p1)
∀z, OSNo z → z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is 5c4035... and proposition id is d5f2d3...
Proof:
An exact proof term for the current goal is CD_proj0proj1_eta {4} HSNo octonion_tag_fresh.
∎
Theorem. (OSNo_proj0proj1_split)
∀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...
Proof:
An exact proof term for the current goal is CD_proj0proj1_split {4} HSNo octonion_tag_fresh.
∎
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...
Theorem. (OSNoLev_ordinal)
∀z, OSNo z → ordinal (OSNoLev z)
In Proofgold the corresponding term root is 49d6e6... and proposition id is 9886f3...
Proof:
Let z be given.
Assume Hz.
Apply OSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx Hy.
Assume Hzxy: z = pa x y.
We will prove ordinal (HSNoLev (p0 (pa x y)) ∪ HSNoLev (p1 (pa x y))).
rewrite the current goal using OSNo_proj0_2 x y Hx Hy (from left to right).
rewrite the current goal using OSNo_proj1_2 x y Hx Hy (from left to right).
We will prove ordinal (HSNoLev x ∪ HSNoLev y).
An exact proof term for the current goal is ordinal_binunion (HSNoLev x) (HSNoLev y) (HSNoLev_ordinal x Hx) (HSNoLev_ordinal y Hy).
∎
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...
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...
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...
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...
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...
Let plus' ≝ add_OSNo
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.
Theorem. (OSNo_minus_OSNo)
∀z, OSNo z → OSNo (minus_OSNo z)
In Proofgold the corresponding term root is 5239a5... and proposition id is 33ab42...
Proof:
An exact proof term for the current goal is CD_minus_CD {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo.
∎
Theorem. (minus_OSNo_proj0)
∀z, OSNo z → p0 (:-: z) = - p0 z
In Proofgold the corresponding term root is 537bbd... and proposition id is bf0daa...
Proof:
An exact proof term for the current goal is CD_minus_proj0 {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo.
∎
Theorem. (minus_OSNo_proj1)
∀z, OSNo z → p1 (:-: z) = - p1 z
In Proofgold the corresponding term root is 34ff58... and proposition id is 0637f8...
Proof:
An exact proof term for the current goal is CD_minus_proj1 {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo.
∎
Theorem. (OSNo_conj_OSNo)
∀z, OSNo z → OSNo (conj_OSNo z)
In Proofgold the corresponding term root is 0bd248... and proposition id is 4a891d...
Proof:
An exact proof term for the current goal is CD_conj_CD {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo conj_HSNo HSNo_conj_HSNo.
∎
Theorem. (conj_OSNo_proj0)
∀z, OSNo z → p0 (z '') = (p0 z) '
In Proofgold the corresponding term root is 9f0c90... and proposition id is 9f6dc7...
Proof:
An exact proof term for the current goal is CD_conj_proj0 {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo conj_HSNo HSNo_conj_HSNo.
∎
Theorem. (conj_OSNo_proj1)
∀z, OSNo z → p1 (z '') = - p1 z
In Proofgold the corresponding term root is 0b0356... and proposition id is 88571e...
Proof:
An exact proof term for the current goal is CD_conj_proj1 {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo conj_HSNo HSNo_conj_HSNo.
∎
Theorem. (OSNo_add_OSNo)
∀z w, OSNo z → OSNo w → OSNo (add_OSNo z w)
In Proofgold the corresponding term root is d59847... and proposition id is 96e815...
Proof:
An exact proof term for the current goal is CD_add_CD {4} HSNo octonion_tag_fresh add_HSNo HSNo_add_HSNo.
∎
Theorem. (add_OSNo_proj0)
∀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...
Proof:
An exact proof term for the current goal is CD_add_proj0 {4} HSNo octonion_tag_fresh add_HSNo HSNo_add_HSNo.
∎
Theorem. (add_OSNo_proj1)
∀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...
Proof:
An exact proof term for the current goal is CD_add_proj1 {4} HSNo octonion_tag_fresh add_HSNo HSNo_add_HSNo.
∎
Theorem. (OSNo_mul_OSNo)
∀z w, OSNo z → OSNo w → OSNo (z ⨯ w)
In Proofgold the corresponding term root is 121ca3... and proposition id is 965453...
Proof:
An exact proof term for the current goal is CD_mul_CD {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo.
∎
Theorem. (mul_OSNo_proj0)
∀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...
Proof:
An exact proof term for the current goal is CD_mul_proj0 {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo.
∎
Theorem. (mul_OSNo_proj1)
∀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...
Proof:
An exact proof term for the current goal is CD_mul_proj1 {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo.
∎
Theorem. (HSNo_OSNo_proj0)
∀x, HSNo x → p0 x = x
In Proofgold the corresponding term root is 3841a4... and proposition id is 5dc42a...
Proof:
An exact proof term for the current goal is CD_proj0_F {4} HSNo octonion_tag_fresh HSNo_0.
∎
Theorem. (HSNo_OSNo_proj1)
∀x, HSNo x → p1 x = 0
In Proofgold the corresponding term root is c0d013... and proposition id is 1ce9ac...
Proof:
An exact proof term for the current goal is CD_proj1_F {4} HSNo octonion_tag_fresh HSNo_0.
∎
Theorem. (OSNo_p0_0)
p0 0 = 0
In Proofgold the corresponding term root is 6e03c2... and proposition id is 50bfb2...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj0 0 HSNo_0.
∎
Theorem. (OSNo_p1_0)
p1 0 = 0
In Proofgold the corresponding term root is 6a2ee2... and proposition id is 5b3474...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj1 0 HSNo_0.
∎
Theorem. (OSNo_p0_1)
p0 1 = 1
In Proofgold the corresponding term root is 6166b0... and proposition id is e0ed62...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj0 1 HSNo_1.
∎
Theorem. (OSNo_p1_1)
p1 1 = 0
In Proofgold the corresponding term root is decdcd... and proposition id is 52bcba...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj1 1 HSNo_1.
∎
Theorem. (OSNo_p0_i)
p0 i = i
In Proofgold the corresponding term root is d61cfb... and proposition id is 092df0...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj0 i HSNo_Complex_i.
∎
Theorem. (OSNo_p1_i)
p1 i = 0
In Proofgold the corresponding term root is 041303... and proposition id is 0ea4e3...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj1 i HSNo_Complex_i.
∎
Theorem. (OSNo_p0_j)
p0 j = j
In Proofgold the corresponding term root is abf3bd... and proposition id is a67029...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj0 j HSNo_Quaternion_j.
∎
Theorem. (OSNo_p1_j)
p1 j = 0
In Proofgold the corresponding term root is d50e95... and proposition id is 2eedc2...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj1 j HSNo_Quaternion_j.
∎
Theorem. (OSNo_p0_k)
p0 k = k
In Proofgold the corresponding term root is 7d823a... and proposition id is 669c9a...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj0 k HSNo_Quaternion_k.
∎
Theorem. (OSNo_p1_k)
p1 k = 0
In Proofgold the corresponding term root is 3ff0b5... and proposition id is 1b52cc...
Proof:
An exact proof term for the current goal is HSNo_OSNo_proj1 k HSNo_Quaternion_k.
∎
Theorem. (minus_OSNo_minus_HSNo)
∀x, HSNo x → :-: x = - x
In Proofgold the corresponding term root is ad664f... and proposition id is aba4f2...
Proof:
An exact proof term for the current goal is CD_minus_F_eq {4} HSNo octonion_tag_fresh minus_HSNo HSNo_0 minus_HSNo_0.
∎
Theorem. (minus_OSNo_0)
:-: 0 = 0
In Proofgold the corresponding term root is 82bb0f... and proposition id is 86b97f...
Proof:
rewrite the current goal using minus_OSNo_minus_HSNo 0 HSNo_0 (from left to right).
An exact proof term for the current goal is minus_HSNo_0.
∎
Theorem. (conj_OSNo_conj_HSNo)
∀x, HSNo x → x '' = x '
In Proofgold the corresponding term root is 8cc42b... and proposition id is 071fef...
Proof:
An exact proof term for the current goal is CD_conj_F_eq {4} HSNo octonion_tag_fresh minus_HSNo HSNo_0 minus_HSNo_0 conj_HSNo.
∎
Theorem. (conj_OSNo_0)
0 '' = 0
In Proofgold the corresponding term root is 898c21... and proposition id is 41501c...
Proof:
rewrite the current goal using conj_OSNo_conj_HSNo 0 HSNo_0 (from left to right).
An exact proof term for the current goal is conj_HSNo_0.
∎
Theorem. (conj_OSNo_1)
1 '' = 1
In Proofgold the corresponding term root is eb7536... and proposition id is 657772...
Proof:
rewrite the current goal using conj_OSNo_conj_HSNo 1 HSNo_1 (from left to right).
An exact proof term for the current goal is conj_HSNo_1.
∎
Theorem. (add_OSNo_add_HSNo)
∀x y, HSNo x → HSNo y → x + y = x + y
In Proofgold the corresponding term root is c83899... and proposition id is b499cd...
Proof:
An exact proof term for the current goal is CD_add_F_eq {4} HSNo octonion_tag_fresh add_HSNo HSNo_0 (add_HSNo_0L 0 HSNo_0).
∎
Theorem. (mul_OSNo_mul_HSNo)
∀x y, HSNo x → HSNo y → x ⨯ y = x * y
In Proofgold the corresponding term root is 7fa435... and proposition id is 1eaaef...
Proof:
An exact proof term for the current goal is CD_mul_F_eq {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 HSNo_conj_HSNo HSNo_mul_HSNo minus_HSNo_0 add_HSNo_0R mul_HSNo_0L mul_HSNo_0R.
∎
Theorem. (minus_OSNo_invol)
∀z, OSNo z → :-: :-: z = z
In Proofgold the corresponding term root is 0a5f21... and proposition id is 101363...
Proof:
An exact proof term for the current goal is CD_minus_invol {4} HSNo octonion_tag_fresh minus_HSNo HSNo_minus_HSNo minus_HSNo_invol.
∎
Theorem. (conj_OSNo_invol)
∀z, OSNo z → z '' '' = z
In Proofgold the corresponding term root is 93265e... and proposition id is 468f13...
Proof:
An exact proof term for the current goal is CD_conj_invol {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo HSNo_minus_HSNo HSNo_conj_HSNo minus_HSNo_invol conj_HSNo_invol.
∎
Theorem. (conj_minus_OSNo)
∀z, OSNo z → (:-: z) '' = :-: (z '')
In Proofgold the corresponding term root is 7ff953... and proposition id is 66cbb8...
Proof:
An exact proof term for the current goal is CD_conj_minus {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo HSNo_minus_HSNo HSNo_conj_HSNo conj_minus_HSNo.
∎
Theorem. (minus_add_OSNo)
∀z w, OSNo z → OSNo w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is 77b3e0... and proposition id is d27c28...
Proof:
An exact proof term for the current goal is CD_minus_add {4} HSNo octonion_tag_fresh minus_HSNo add_HSNo HSNo_minus_HSNo HSNo_add_HSNo minus_add_HSNo.
∎
Theorem. (conj_add_OSNo)
∀z w, OSNo z → OSNo w → (z + w) '' = z '' + w ''
In Proofgold the corresponding term root is 35c199... and proposition id is 02f2b8...
Proof:
An exact proof term for the current goal is CD_conj_add {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo minus_add_HSNo conj_add_HSNo.
∎
Theorem. (add_OSNo_com)
∀z w, OSNo z → OSNo w → z + w = w + z
In Proofgold the corresponding term root is a80b65... and proposition id is 2dee60...
Proof:
An exact proof term for the current goal is CD_add_com {4} HSNo octonion_tag_fresh add_HSNo add_HSNo_com.
∎
Theorem. (add_OSNo_assoc)
∀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...
Proof:
Apply CD_add_assoc {4} HSNo octonion_tag_fresh add_HSNo HSNo_add_HSNo add_HSNo_assoc to the current goal.
∎
Theorem. (add_OSNo_0L)
∀z, OSNo z → add_OSNo 0 z = z
In Proofgold the corresponding term root is 7b12c3... and proposition id is cb288a...
Proof:
An exact proof term for the current goal is CD_add_0L {4} HSNo octonion_tag_fresh add_HSNo HSNo_0 add_HSNo_0L.
∎
Theorem. (add_OSNo_0R)
∀z, OSNo z → add_OSNo z 0 = z
In Proofgold the corresponding term root is 206e65... and proposition id is 11264f...
Proof:
An exact proof term for the current goal is CD_add_0R {4} HSNo octonion_tag_fresh add_HSNo HSNo_0 add_HSNo_0R.
∎
Theorem. (add_OSNo_minus_OSNo_linv)
∀z, OSNo z → add_OSNo (minus_OSNo z) z = 0
In Proofgold the corresponding term root is d558dc... and proposition id is 8767d9...
Proof:
An exact proof term for the current goal is CD_add_minus_linv {4} HSNo octonion_tag_fresh minus_HSNo add_HSNo HSNo_minus_HSNo add_HSNo_minus_HSNo_linv.
∎
Theorem. (add_OSNo_minus_OSNo_rinv)
∀z, OSNo z → add_OSNo z (minus_OSNo z) = 0
In Proofgold the corresponding term root is 67ef27... and proposition id is 1f6cac...
Proof:
An exact proof term for the current goal is CD_add_minus_rinv {4} HSNo octonion_tag_fresh minus_HSNo add_HSNo HSNo_minus_HSNo add_HSNo_minus_HSNo_rinv.
∎
Theorem. (mul_OSNo_0R)
∀z, OSNo z → z ⨯ 0 = 0
In Proofgold the corresponding term root is 4efeb2... and proposition id is ee156e...
Proof:
An exact proof term for the current goal is CD_mul_0R {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 minus_HSNo_0 conj_HSNo_0 (add_HSNo_0L 0 HSNo_0) mul_HSNo_0L mul_HSNo_0R.
∎
Theorem. (mul_OSNo_0L)
∀z, OSNo z → 0 ⨯ z = 0
In Proofgold the corresponding term root is 9ff46d... and proposition id is ea206a...
Proof:
An exact proof term for the current goal is CD_mul_0L {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 HSNo_conj_HSNo minus_HSNo_0 (add_HSNo_0L 0 HSNo_0) mul_HSNo_0L mul_HSNo_0R.
∎
Theorem. (mul_OSNo_1R)
∀z, OSNo z → z ⨯ 1 = z
In Proofgold the corresponding term root is 0cf2d9... and proposition id is 71047e...
Proof:
An exact proof term for the current goal is CD_mul_1R {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 HSNo_1 minus_HSNo_0 conj_HSNo_0 conj_HSNo_1 add_HSNo_0L add_HSNo_0R mul_HSNo_0L mul_HSNo_1R.
∎
Theorem. (mul_OSNo_1L)
∀z, OSNo z → 1 ⨯ z = z
In Proofgold the corresponding term root is d299c9... and proposition id is 0048db...
Proof:
An exact proof term for the current goal is CD_mul_1L {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 HSNo_1 HSNo_conj_HSNo minus_HSNo_0 add_HSNo_0R mul_HSNo_0L mul_HSNo_0R mul_HSNo_1L mul_HSNo_1R.
∎
Theorem. (conj_mul_OSNo)
∀z w, OSNo z → OSNo w → (z ⨯ w) '' = w '' ⨯ z ''
In Proofgold the corresponding term root is 05d740... and proposition id is b7721c...
Proof:
An exact proof term for the current goal is CD_conj_mul {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo minus_HSNo_invol conj_HSNo_invol conj_minus_HSNo conj_add_HSNo minus_add_HSNo add_HSNo_com conj_mul_HSNo minus_mul_HSNo_distrR minus_mul_HSNo_distrL.
∎
Theorem. (mul_OSNo_distrL)
∀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...
Proof:
An exact proof term for the current goal is CD_add_mul_distrL {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo minus_add_HSNo conj_add_HSNo add_HSNo_assoc add_HSNo_com mul_HSNo_distrL mul_HSNo_distrR.
∎
Theorem. (mul_OSNo_distrR)
∀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...
Proof:
An exact proof term for the current goal is CD_add_mul_distrR {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo minus_add_HSNo add_HSNo_assoc add_HSNo_com mul_HSNo_distrL mul_HSNo_distrR.
∎
Theorem. (minus_mul_OSNo_distrR)
∀z w, OSNo z → OSNo w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is 54ee0d... and proposition id is 65f43c...
Proof:
An exact proof term for the current goal is CD_minus_mul_distrR {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo conj_minus_HSNo minus_add_HSNo minus_mul_HSNo_distrR minus_mul_HSNo_distrL.
∎
Theorem. (minus_mul_OSNo_distrL)
∀z w, OSNo z → OSNo w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is bfdb51... and proposition id is 2ef898...
Proof:
An exact proof term for the current goal is CD_minus_mul_distrL {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo minus_add_HSNo minus_mul_HSNo_distrR minus_mul_HSNo_distrL.
∎
Theorem. (exp_OSNo_nat_0)
∀z, z0 = 1
In Proofgold the corresponding term root is 469625... and proposition id is 0dfdbe...
Proof:
An exact proof term for the current goal is CD_exp_nat_0 {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo.
∎
Theorem. (exp_OSNo_nat_S)
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
In Proofgold the corresponding term root is 340b9f... and proposition id is e25374...
Proof:
An exact proof term for the current goal is CD_exp_nat_S {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo.
∎
Theorem. (exp_OSNo_nat_1)
∀z, OSNo z → z1 = z
In Proofgold the corresponding term root is f5712c... and proposition id is e64119...
Proof:
An exact proof term for the current goal is CD_exp_nat_1 {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 HSNo_1 minus_HSNo_0 conj_HSNo_0 conj_HSNo_1 add_HSNo_0L add_HSNo_0R mul_HSNo_0L mul_HSNo_1R.
∎
Theorem. (exp_OSNo_nat_2)
∀z, OSNo z → z2 = z ⨯ z
In Proofgold the corresponding term root is 6ad2c8... and proposition id is b8a62a...
Proof:
An exact proof term for the current goal is CD_exp_nat_2 {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_0 HSNo_1 minus_HSNo_0 conj_HSNo_0 conj_HSNo_1 add_HSNo_0L add_HSNo_0R mul_HSNo_0L mul_HSNo_1R.
∎
Theorem. (OSNo_exp_OSNo_nat)
∀z, OSNo z → ∀n, nat_p n → OSNo (zn)
In Proofgold the corresponding term root is 9fea84... and proposition id is ccc319...
Proof:
An exact proof term for the current goal is CD_exp_nat_CD {4} HSNo octonion_tag_fresh minus_HSNo conj_HSNo add_HSNo mul_HSNo HSNo_minus_HSNo HSNo_conj_HSNo HSNo_add_HSNo HSNo_mul_HSNo HSNo_0 HSNo_1.
∎
Theorem. (add_HSNo_com_3b_1_2)
∀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...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We will prove (x + y) + z = (x + z) + y.
rewrite the current goal using add_HSNo_assoc x y z Hx Hy Hz (from left to right).
We will prove x + y + z = (x + z) + y.
rewrite the current goal using add_HSNo_assoc x z y Hx Hz Hy (from left to right).
We will prove x + y + z = x + z + y.
Use f_equal.
An exact proof term for the current goal is add_HSNo_com y z Hy Hz.
∎
Theorem. (add_HSNo_com_4_inner_mid)
∀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...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_HSNo_assoc (x + y) z w (HSNo_add_HSNo x y Hx Hy) Hz Hw (from right to left).
We will prove ((x + y) + z) + w = (x + z) + (y + w).
rewrite the current goal using add_HSNo_com_3b_1_2 x y z Hx Hy Hz (from left to right).
We will prove ((x + z) + y) + w = (x + z) + (y + w).
An exact proof term for the current goal is add_HSNo_assoc (x + z) y w (HSNo_add_HSNo x z Hx Hz) Hy Hw.
∎
Theorem. (add_HSNo_rotate_4_0312)
∀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...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_HSNo_com z w Hz Hw (from left to right).
We will prove (x + y) + (w + z) = (x + w) + (y + z).
An exact proof term for the current goal is add_HSNo_com_4_inner_mid x y w z Hx Hy Hw Hz.
∎
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...
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...
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...
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...
Let i0 ≝ Octonion_i0
Let i1 ≝ Complex_i
Let i2 ≝ Quaternion_j
Let i3 ≝ Octonion_i3
Let i4 ≝ Quaternion_k
Let i5 ≝ Octonion_i5
Let i6 ≝ Octonion_i6
Theorem. (OSNo_Complex_i)
OSNo i
In Proofgold the corresponding term root is af3f4b... and proposition id is 12bbc0...
Proof:
Apply HSNo_OSNo to the current goal.
An exact proof term for the current goal is HSNo_Complex_i.
∎
Theorem. (OSNo_Quaternion_j)
OSNo j
In Proofgold the corresponding term root is 77f80f... and proposition id is c8c165...
Proof:
Apply HSNo_OSNo to the current goal.
An exact proof term for the current goal is HSNo_Quaternion_j.
∎
Theorem. (OSNo_Quaternion_k)
OSNo k
In Proofgold the corresponding term root is 9b69f6... and proposition id is eba5fb...
Proof:
Apply HSNo_OSNo to the current goal.
An exact proof term for the current goal is HSNo_Quaternion_k.
∎
Theorem. (OSNo_Octonion_i0)
OSNo i0
In Proofgold the corresponding term root is e6c8dc... and proposition id is 45658b...
Proof:
An exact proof term for the current goal is OSNo_I 0 1 HSNo_0 HSNo_1.
∎
Theorem. (OSNo_Octonion_i3)
OSNo i3
In Proofgold the corresponding term root is 39dd06... and proposition id is 428549...
Proof:
An exact proof term for the current goal is OSNo_I 0 (- i) HSNo_0 (HSNo_minus_HSNo i HSNo_Complex_i).
∎
Theorem. (OSNo_Octonion_i5)
OSNo i5
In Proofgold the corresponding term root is 55ce63... and proposition id is e92a7a...
Proof:
An exact proof term for the current goal is OSNo_I 0 (- k) HSNo_0 (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎
Theorem. (OSNo_Octonion_i6)
OSNo i6
In Proofgold the corresponding term root is 73ed2a... and proposition id is d0f581...
Proof:
An exact proof term for the current goal is OSNo_I 0 (- j) HSNo_0 (HSNo_minus_HSNo j HSNo_Quaternion_j).
∎
Theorem. (OSNo_p0_i0)
p0 i0 = 0
In Proofgold the corresponding term root is c9a02f... and proposition id is 444265...
Proof:
An exact proof term for the current goal is OSNo_proj0_2 0 1 HSNo_0 HSNo_1.
∎
Theorem. (OSNo_p1_i0)
p1 i0 = 1
In Proofgold the corresponding term root is 6bb51f... and proposition id is 17a56f...
Proof:
An exact proof term for the current goal is OSNo_proj1_2 0 1 HSNo_0 HSNo_1.
∎
Theorem. (OSNo_p0_i3)
p0 i3 = 0
In Proofgold the corresponding term root is 784dc9... and proposition id is 27f5a3...
Proof:
An exact proof term for the current goal is OSNo_proj0_2 0 (- i) HSNo_0 (HSNo_minus_HSNo i HSNo_Complex_i).
∎
Theorem. (OSNo_p1_i3)
p1 i3 = - i
In Proofgold the corresponding term root is 097faa... and proposition id is 6371c8...
Proof:
An exact proof term for the current goal is OSNo_proj1_2 0 (- i) HSNo_0 (HSNo_minus_HSNo i HSNo_Complex_i).
∎
Theorem. (OSNo_p0_i5)
p0 i5 = 0
In Proofgold the corresponding term root is 597589... and proposition id is c4b46c...
Proof:
An exact proof term for the current goal is OSNo_proj0_2 0 (- k) HSNo_0 (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎
Theorem. (OSNo_p1_i5)
p1 i5 = - k
In Proofgold the corresponding term root is ef1afc... and proposition id is 9bf42c...
Proof:
An exact proof term for the current goal is OSNo_proj1_2 0 (- k) HSNo_0 (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎
Theorem. (OSNo_p0_i6)
p0 i6 = 0
In Proofgold the corresponding term root is bf6e13... and proposition id is 183aad...
Proof:
An exact proof term for the current goal is OSNo_proj0_2 0 (- j) HSNo_0 (HSNo_minus_HSNo j HSNo_Quaternion_j).
∎
Theorem. (OSNo_p1_i6)
p1 i6 = - j
In Proofgold the corresponding term root is 50991b... and proposition id is 78f3bd...
Proof:
An exact proof term for the current goal is OSNo_proj1_2 0 (- j) HSNo_0 (HSNo_minus_HSNo j HSNo_Quaternion_j).
∎
Theorem. (Octonion_i1_sqr)
i1 ⨯ i1 = :-: 1
In Proofgold the corresponding term root is 2cf2b7... and proposition id is 701b4a...
Proof:
rewrite the current goal using mul_OSNo_mul_HSNo i i HSNo_Complex_i HSNo_Complex_i (from left to right).
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We will prove i * i = - 1.
An exact proof term for the current goal is Quaternion_i_sqr.
∎
Theorem. (Octonion_i2_sqr)
i2 ⨯ i2 = :-: 1
In Proofgold the corresponding term root is 52dca5... and proposition id is 46db7e...
Proof:
rewrite the current goal using mul_OSNo_mul_HSNo j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We will prove j * j = - 1.
An exact proof term for the current goal is Quaternion_j_sqr.
∎
Theorem. (Octonion_i4_sqr)
i4 ⨯ i4 = :-: 1
In Proofgold the corresponding term root is e85aa9... and proposition id is f8d60f...
Proof:
rewrite the current goal using mul_OSNo_mul_HSNo k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We will prove k * k = - 1.
An exact proof term for the current goal is Quaternion_k_sqr.
∎
Theorem. (Octonion_i0_sqr)
i0 ⨯ i0 = :-: 1
In Proofgold the corresponding term root is 6e1738... and proposition id is 4f5642...
Proof:
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We prove the intermediate claim Li0i0: OSNo (i0 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i0 OSNo_Octonion_i0 OSNo_Octonion_i0.
We will prove i0 ⨯ i0 = - 1.
We prove the intermediate claim L1: HSNo (- 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply OSNo_proj0proj1_split (i0 ⨯ i0) (- 1) Li0i0 (HSNo_OSNo (- 1) L1) to the current goal.
We will prove p0 (i0 ⨯ i0) = p0 (- 1).
rewrite the current goal using HSNo_OSNo_proj0 (- 1) L1 (from left to right).
We will prove p0 (i0 ⨯ i0) = - 1.
rewrite the current goal using mul_OSNo_proj0 i0 i0 OSNo_Octonion_i0 OSNo_Octonion_i0 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - (1 ' * 1) = - 1.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
We will prove 0 + - (1 ' * 1) = - 1.
rewrite the current goal using conj_HSNo_id_SNo 1 SNo_1 (from left to right).
We will prove 0 + - (1 * 1) = - 1.
rewrite the current goal using mul_HSNo_1L 1 HSNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_HSNo_0L (- 1) L1.
We will prove p1 (i0 ⨯ i0) = p1 (- 1).
rewrite the current goal using HSNo_OSNo_proj1 (- 1) L1 (from left to right).
We will prove p1 (i0 ⨯ i0) = 0.
rewrite the current goal using mul_OSNo_proj1 i0 i0 OSNo_Octonion_i0 OSNo_Octonion_i0 (from left to right).
We will prove p1 i0 * p0 i0 + p1 i0 * p0 i0 ' = 0.
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 1 * 0 + 1 * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i3_sqr)
i3 ⨯ i3 = :-: 1
In Proofgold the corresponding term root is 8c0727... and proposition id is 24bf69...
Proof:
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We prove the intermediate claim Li3i3: OSNo (i3 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i3 OSNo_Octonion_i3 OSNo_Octonion_i3.
We will prove i3 ⨯ i3 = - 1.
We prove the intermediate claim L1: HSNo (- 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply OSNo_proj0proj1_split (i3 ⨯ i3) (- 1) Li3i3 (HSNo_OSNo (- 1) L1) to the current goal.
We will prove p0 (i3 ⨯ i3) = p0 (- 1).
rewrite the current goal using HSNo_OSNo_proj0 (- 1) L1 (from left to right).
We will prove p0 (i3 ⨯ i3) = - 1.
rewrite the current goal using mul_OSNo_proj0 i3 i3 OSNo_Octonion_i3 OSNo_Octonion_i3 (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
We will prove 0 + - ((- i) ' * (- i)) = - 1.
rewrite the current goal using conj_minus_HSNo i HSNo_Complex_i (from left to right).
We will prove 0 + - ((- i ') * (- i)) = - 1.
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
We will prove 0 + - (i * (- i)) = - 1.
rewrite the current goal using minus_mul_HSNo_distrR i i HSNo_Complex_i HSNo_Complex_i (from left to right).
We will prove 0 + - - i * i = - 1.
rewrite the current goal using minus_HSNo_invol (i * i) (HSNo_mul_HSNo i i HSNo_Complex_i HSNo_Complex_i) (from left to right).
rewrite the current goal using Quaternion_i_sqr (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_HSNo_0L (- 1) L1.
We will prove p1 (i3 ⨯ i3) = p1 (- 1).
rewrite the current goal using HSNo_OSNo_proj1 (- 1) L1 (from left to right).
We will prove p1 (i3 ⨯ i3) = 0.
rewrite the current goal using mul_OSNo_proj1 i3 i3 OSNo_Octonion_i3 OSNo_Octonion_i3 (from left to right).
We will prove p1 i3 * p0 i3 + p1 i3 * p0 i3 ' = 0.
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove (- i) * 0 + (- i) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
We will prove (- i) * 0 + (- i) * 0 = 0.
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i5_sqr)
i5 ⨯ i5 = :-: 1
In Proofgold the corresponding term root is 19b120... and proposition id is 474ccf...
Proof:
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We prove the intermediate claim Li5i5: OSNo (i5 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i5 OSNo_Octonion_i5 OSNo_Octonion_i5.
We will prove i5 ⨯ i5 = - 1.
We prove the intermediate claim L1: HSNo (- 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply OSNo_proj0proj1_split (i5 ⨯ i5) (- 1) Li5i5 (HSNo_OSNo (- 1) L1) to the current goal.
We will prove p0 (i5 ⨯ i5) = p0 (- 1).
rewrite the current goal using HSNo_OSNo_proj0 (- 1) L1 (from left to right).
We will prove p0 (i5 ⨯ i5) = - 1.
rewrite the current goal using mul_OSNo_proj0 i5 i5 OSNo_Octonion_i5 OSNo_Octonion_i5 (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
We will prove 0 + - ((- k) ' * (- k)) = - 1.
rewrite the current goal using conj_minus_HSNo k HSNo_Quaternion_k (from left to right).
We will prove 0 + - ((- k ') * (- k)) = - 1.
rewrite the current goal using conj_HSNo_k (from left to right).
We will prove 0 + - ((- - k) * (- k)) = - 1.
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
We will prove 0 + - (k * (- k)) = - 1.
rewrite the current goal using minus_mul_HSNo_distrR k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
We will prove 0 + - - (k * k) = - 1.
rewrite the current goal using Quaternion_k_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_HSNo_0L (- 1) L1.
We will prove p1 (i5 ⨯ i5) = p1 (- 1).
rewrite the current goal using HSNo_OSNo_proj1 (- 1) L1 (from left to right).
We will prove p1 (i5 ⨯ i5) = 0.
rewrite the current goal using mul_OSNo_proj1 i5 i5 OSNo_Octonion_i5 OSNo_Octonion_i5 (from left to right).
We will prove p1 i5 * p0 i5 + p1 i5 * p0 i5 ' = 0.
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove (- k) * 0 + (- k) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i6_sqr)
i6 ⨯ i6 = :-: 1
In Proofgold the corresponding term root is 97f9e7... and proposition id is 12af41...
Proof:
rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).
We prove the intermediate claim Li6i6: OSNo (i6 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i6 OSNo_Octonion_i6 OSNo_Octonion_i6.
We will prove i6 ⨯ i6 = - 1.
We prove the intermediate claim L1: HSNo (- 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply OSNo_proj0proj1_split (i6 ⨯ i6) (- 1) Li6i6 (HSNo_OSNo (- 1) L1) to the current goal.
We will prove p0 (i6 ⨯ i6) = p0 (- 1).
rewrite the current goal using HSNo_OSNo_proj0 (- 1) L1 (from left to right).
We will prove p0 (i6 ⨯ i6) = - 1.
rewrite the current goal using mul_OSNo_proj0 i6 i6 OSNo_Octonion_i6 OSNo_Octonion_i6 (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
We will prove 0 + - ((- j) ' * (- j)) = - 1.
rewrite the current goal using conj_minus_HSNo j HSNo_Quaternion_j (from left to right).
We will prove 0 + - ((- j ') * (- j)) = - 1.
rewrite the current goal using conj_HSNo_j (from left to right).
We will prove 0 + - ((- - j) * (- j)) = - 1.
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
We will prove 0 + - (j * (- j)) = - 1.
rewrite the current goal using minus_mul_HSNo_distrR j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).
We will prove 0 + - - (j * j) = - 1.
rewrite the current goal using Quaternion_j_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_HSNo_0L (- 1) L1.
We will prove p1 (i6 ⨯ i6) = p1 (- 1).
rewrite the current goal using HSNo_OSNo_proj1 (- 1) L1 (from left to right).
We will prove p1 (i6 ⨯ i6) = 0.
rewrite the current goal using mul_OSNo_proj1 i6 i6 OSNo_Octonion_i6 OSNo_Octonion_i6 (from left to right).
We will prove p1 i6 * p0 i6 + p1 i6 * p0 i6 ' = 0.
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove (- j) * 0 + (- j) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i1_i2)
i1 ⨯ i2 = i4
In Proofgold the corresponding term root is 54f62e... and proposition id is fd7e6b...
Proof:
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li1i2: OSNo (i1 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i1 i2 ?? ??.
Apply OSNo_proj0proj1_split (i1 ⨯ i2) i4 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using mul_OSNo_proj0 i1 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove i * j + - (0 ' * 0) = k.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (i * j) (HSNo_mul_HSNo i j HSNo_Complex_i HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is Quaternion_i_j.
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using mul_OSNo_proj1 i1 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * i + 0 * j ' = 0.
rewrite the current goal using mul_HSNo_0L (j ') (HSNo_conj_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using mul_HSNo_0L i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i2_i1)
i2 ⨯ i1 = :-: i4
In Proofgold the corresponding term root is a29e37... and proposition id is f1a9c7...
Proof:
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li2i1: OSNo (i2 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i2 i1 ?? ??.
Apply OSNo_proj0proj1_split (i2 ⨯ i1) (:-: i4) ?? (OSNo_minus_OSNo i4 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i4 ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using mul_OSNo_proj0 i2 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove j * i + - (0 ' * 0) = - k.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (j * i) (HSNo_mul_HSNo j i HSNo_Quaternion_j HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is Quaternion_j_i.
rewrite the current goal using minus_OSNo_proj1 i4 ?? (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using mul_OSNo_proj1 i2 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * j + 0 * i ' = - 0.
rewrite the current goal using mul_HSNo_0L (i ') (HSNo_conj_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using mul_HSNo_0L j HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i2_i4)
i2 ⨯ i4 = i1
In Proofgold the corresponding term root is 32f52e... and proposition id is 60c4d4...
Proof:
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li2i4: OSNo (i2 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i2 i4 ?? ??.
Apply OSNo_proj0proj1_split (i2 ⨯ i4) i1 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i2 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove j * k + - (0 ' * 0) = i.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (j * k) (HSNo_mul_HSNo j k HSNo_Quaternion_j HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is Quaternion_j_k.
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i2 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * j + 0 * k ' = 0.
rewrite the current goal using mul_HSNo_0L (k ') (HSNo_conj_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using mul_HSNo_0L j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i4_i2)
i4 ⨯ i2 = :-: i1
In Proofgold the corresponding term root is 0c684d... and proposition id is 294b23...
Proof:
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li4i2: OSNo (i4 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i2 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i2) (:-: i1) ?? (OSNo_minus_OSNo i1 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i1 ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i4 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove k * j + - (0 ' * 0) = - i.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (k * j) (HSNo_mul_HSNo k j HSNo_Quaternion_k HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is Quaternion_k_j.
rewrite the current goal using minus_OSNo_proj1 i1 ?? (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i4 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * k + 0 * j ' = - 0.
rewrite the current goal using mul_HSNo_0L (j ') (HSNo_conj_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i4_i1)
i4 ⨯ i1 = i2
In Proofgold the corresponding term root is fe2349... and proposition id is f00e84...
Proof:
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li4i1: OSNo (i4 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i1 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i1) i2 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i4 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove k * i + - (0 ' * 0) = j.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (k * i) (HSNo_mul_HSNo k i HSNo_Quaternion_k HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is Quaternion_k_i.
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i4 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * k + 0 * i ' = 0.
rewrite the current goal using mul_HSNo_0L (i ') (HSNo_conj_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i1_i4)
i1 ⨯ i4 = :-: i2
In Proofgold the corresponding term root is 6ef84c... and proposition id is 48faff...
Proof:
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li1i4: OSNo (i1 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i1 i4 ?? ??.
Apply OSNo_proj0proj1_split (i1 ⨯ i4) (:-: i2) ?? (OSNo_minus_OSNo i2 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i2 ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i1 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove i * k + - (0 ' * 0) = - j.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using add_HSNo_0R (i * k) (HSNo_mul_HSNo i k HSNo_Complex_i HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is Quaternion_i_k.
rewrite the current goal using minus_OSNo_proj1 i2 ?? (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i1 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * i + 0 * k ' = - 0.
rewrite the current goal using mul_HSNo_0L (k ') (HSNo_conj_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using mul_HSNo_0L i HSNo_Complex_i (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i2_i3)
i2 ⨯ i3 = i5
In Proofgold the corresponding term root is 69b316... and proposition id is 7ee827...
Proof:
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li2i3: OSNo (i2 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i2 i3 ?? ??.
Apply OSNo_proj0proj1_split (i2 ⨯ i3) i5 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i2 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove j * 0 + - ((- i) ' * 0) = 0.
rewrite the current goal using mul_HSNo_0R j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0R ((- i) ') (HSNo_conj_HSNo (- i) (HSNo_minus_HSNo i HSNo_Complex_i)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i2 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove (- i) * j + 0 * 0 ' = (- k).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i j HSNo_Complex_i HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_i_j (from left to right).
An exact proof term for the current goal is add_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎
Theorem. (Octonion_i3_i2)
i3 ⨯ i2 = :-: i5
In Proofgold the corresponding term root is 189ce1... and proposition id is ba3701...
Proof:
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li3i2: OSNo (i3 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i2 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i2) (:-: i5) ?? (OSNo_minus_OSNo i5 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i5 ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove 0 * j + - (0 ' * (- i)) = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i5 ?? (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove 0 * 0 + (- i) * j ' = - (- k).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i (- j) HSNo_Complex_i (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR i j HSNo_Complex_i HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_i_j (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L k HSNo_Quaternion_k.
∎
Theorem. (Octonion_i3_i5)
i3 ⨯ i5 = i2
In Proofgold the corresponding term root is 0c085c... and proposition id is 54e1ef...
Proof:
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li3i5: OSNo (i3 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i5 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i5) i2 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove 0 * 0 + - ((- k) ' * (- i)) = j.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo k HSNo_Quaternion_k (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
We will prove 0 + - (k * (- i)) = j.
rewrite the current goal using minus_mul_HSNo_distrR k i HSNo_Quaternion_k HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_k_i (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L j HSNo_Quaternion_j.
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove (- k) * 0 + (- i) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i5_i3)
i5 ⨯ i3 = :-: i2
In Proofgold the corresponding term root is e8fde0... and proposition id is 9faab2...
Proof:
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li5i3: OSNo (i5 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i3 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i3) (:-: i2) ?? (OSNo_minus_OSNo i2 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i2 ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove 0 * 0 + - ((- i) ' * (- k)) = - j.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo i HSNo_Complex_i (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
We will prove 0 + - (i * (- k)) = - j.
rewrite the current goal using minus_mul_HSNo_distrR i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_i_k (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j).
rewrite the current goal using minus_OSNo_proj1 i2 ?? (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove (- i) * 0 + (- k) * 0 ' = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i5_i2)
i5 ⨯ i2 = i3
In Proofgold the corresponding term root is 346b35... and proposition id is 40996f...
Proof:
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li5i2: OSNo (i5 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i2 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i2) i3 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * j + - (0 ' * (- k)) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * 0 + (- k) * j ' = (- i).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR (- k) j (HSNo_minus_HSNo k HSNo_Quaternion_k) HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL k j HSNo_Quaternion_k HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_k_j (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i).
∎
Theorem. (Octonion_i2_i5)
i2 ⨯ i5 = :-: i3
In Proofgold the corresponding term root is 2d78a7... and proposition id is f300cd...
Proof:
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li2i5: OSNo (i2 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i2 i5 ?? ??.
Apply OSNo_proj0proj1_split (i2 ⨯ i5) (:-: i3) ?? (OSNo_minus_OSNo i3 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i3 ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i2 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove j * 0 + - ((- k) ' * 0) = - 0.
rewrite the current goal using mul_HSNo_0R j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0R ((- k) ') (HSNo_conj_HSNo (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i3 ?? (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i2 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove (- k) * j + 0 * 0 ' = - (- i).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL k j HSNo_Quaternion_k HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_k_j (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0R i HSNo_Complex_i.
∎
Theorem. (Octonion_i3_i4)
i3 ⨯ i4 = i6
In Proofgold the corresponding term root is 511ac9... and proposition id is 73693c...
Proof:
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li3i4: OSNo (i3 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i4 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i4) i6 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * k + - (0 ' * (- i)) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * 0 + (- i) * k ' = (- j).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR (- i) k (HSNo_minus_HSNo i HSNo_Complex_i) HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_i_k (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j).
∎
Theorem. (Octonion_i4_i3)
i4 ⨯ i3 = :-: i6
In Proofgold the corresponding term root is e373e5... and proposition id is b2ad1d...
Proof:
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li4i3: OSNo (i4 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i3 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i3) (:-: i6) ?? (OSNo_minus_OSNo i6 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i6 ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i4 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove k * 0 + - ((- i) ' * 0) = - 0.
rewrite the current goal using mul_HSNo_0R k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0R ((- i) ') (HSNo_conj_HSNo (- i) (HSNo_minus_HSNo i HSNo_Complex_i)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i6 ?? (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i4 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove (- i) * k + 0 * 0 ' = - (- j).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
We will prove - i * k + 0 = - - j.
rewrite the current goal using Quaternion_i_k (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0R j HSNo_Quaternion_j.
∎
Theorem. (Octonion_i4_i6)
i4 ⨯ i6 = i3
In Proofgold the corresponding term root is 620e03... and proposition id is 7c49f7...
Proof:
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li4i6: OSNo (i4 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i6 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i6) i3 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i4 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove k * 0 + - ((- j) ' * 0) = 0.
rewrite the current goal using mul_HSNo_0R k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0R ((- j) ') (HSNo_conj_HSNo (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i4 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove (- j) * k + 0 * 0 ' = (- i).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j k HSNo_Quaternion_j HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_j_k (from left to right).
An exact proof term for the current goal is add_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i).
∎
Theorem. (Octonion_i6_i4)
i6 ⨯ i4 = :-: i3
In Proofgold the corresponding term root is 121f61... and proposition id is 0b4e69...
Proof:
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li6i4: OSNo (i6 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i4 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i4) (:-: i3) ?? (OSNo_minus_OSNo i3 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i3 ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove 0 * k + - (0 ' * (- j)) = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i3 ?? (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove 0 * 0 + (- j) * k ' = - (- i).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR (- j) k (HSNo_minus_HSNo j HSNo_Quaternion_j) HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j k HSNo_Quaternion_j HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_j_k (from left to right).
We will prove 0 + - - i = - - i.
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L i HSNo_Complex_i.
∎
Theorem. (Octonion_i6_i3)
i6 ⨯ i3 = i4
In Proofgold the corresponding term root is d3cc9f... and proposition id is 9b6ce9...
Proof:
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li6i3: OSNo (i6 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i3 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i3) i4 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove 0 * 0 + - ((- i) ' * (- j)) = k.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo i HSNo_Complex_i (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
We will prove 0 + - (i * (- j)) = k.
rewrite the current goal using minus_mul_HSNo_distrR i j HSNo_Complex_i HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_i_j (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L k HSNo_Quaternion_k.
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove (- i) * 0 + (- j) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i3_i6)
i3 ⨯ i6 = :-: i4
In Proofgold the corresponding term root is 575da0... and proposition id is 517b53...
Proof:
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li3i6: OSNo (i3 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i6 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i6) (:-: i4) ?? (OSNo_minus_OSNo i4 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i4 ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove 0 * 0 + - ((- j) ' * (- i)) = - k.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo j HSNo_Quaternion_j (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
We will prove 0 + - (j * (- i)) = - k.
rewrite the current goal using minus_mul_HSNo_distrR j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_j_i (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
rewrite the current goal using minus_OSNo_proj1 i4 ?? (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove (- j) * 0 + (- i) * 0 ' = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i4_i5)
i4 ⨯ i5 = i0
In Proofgold the corresponding term root is 360332... and proposition id is fc370d...
Proof:
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li4i5: OSNo (i4 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i5 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i5) i0 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i4 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove k * 0 + - ((- k) ' * 0) = 0.
rewrite the current goal using mul_HSNo_0R k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0R ((- k) ') (HSNo_conj_HSNo (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i4 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove (- k) * k + 0 * 0 ' = 1.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_k_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0R 1 HSNo_1.
∎
Theorem. (Octonion_i5_i4)
i5 ⨯ i4 = :-: i0
In Proofgold the corresponding term root is beff8b... and proposition id is afcfe9...
Proof:
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li5i4: OSNo (i5 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i4 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i4) (:-: i0) ?? (OSNo_minus_OSNo i0 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i0 ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove 0 * k + - (0 ' * (- k)) = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i0 ?? (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove 0 * 0 + (- k) * k ' = - 1.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
We will prove 0 + (- k) * (- k) = - 1.
rewrite the current goal using minus_mul_HSNo_distrL k (- k) HSNo_Quaternion_k (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
We will prove 0 + - - k * k = - 1.
rewrite the current goal using Quaternion_k_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- 1) (HSNo_minus_HSNo 1 HSNo_1).
∎
Theorem. (Octonion_i5_i0)
i5 ⨯ i0 = i4
In Proofgold the corresponding term root is adfd5d... and proposition id is e39b44...
Proof:
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li5i0: OSNo (i5 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i0 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i0) i4 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - (1 ' * (- k)) = k.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_id_SNo 1 SNo_1 (from left to right).
rewrite the current goal using mul_HSNo_1L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
We will prove 0 + - - k = k.
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L k HSNo_Quaternion_k.
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 1 * 0 + (- k) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i0_i5)
i0 ⨯ i5 = :-: i4
In Proofgold the corresponding term root is 498fb6... and proposition id is 0b796b...
Proof:
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li0i5: OSNo (i0 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i5 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i5) (:-: i4) ?? (OSNo_minus_OSNo i4 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i4 ?? (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - ((- k) ' * 1) = - k.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo k HSNo_Quaternion_k (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
We will prove 0 + - (k * 1) = - k.
rewrite the current goal using mul_HSNo_1R k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
rewrite the current goal using minus_OSNo_proj1 i4 ?? (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove (- k) * 0 + 1 * 0 ' = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i0_i4)
i0 ⨯ i4 = i5
In Proofgold the corresponding term root is 133131... and proposition id is 3686a2...
Proof:
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li0i4: OSNo (i0 ⨯ i4).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i4 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i4) i5 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * k + - (0 ' * 1) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0L 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i4 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 0 * 0 + 1 * k ' = (- k).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_1L (k ') (HSNo_conj_HSNo k HSNo_Quaternion_k) (from left to right).
We will prove 0 + k ' = (- k).
rewrite the current goal using conj_HSNo_k (from left to right).
We will prove 0 + - k = (- k).
An exact proof term for the current goal is add_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎
Theorem. (Octonion_i4_i0)
i4 ⨯ i0 = :-: i5
In Proofgold the corresponding term root is 01a797... and proposition id is 529327...
Proof:
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li4: OSNo i4.
An exact proof term for the current goal is OSNo_Quaternion_k.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li4i0: OSNo (i4 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i4 i0 ?? ??.
Apply OSNo_proj0proj1_split (i4 ⨯ i0) (:-: i5) ?? (OSNo_minus_OSNo i5 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i5 ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i4 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove k * 0 + - (1 ' * 0) = - 0.
rewrite the current goal using mul_HSNo_0R k HSNo_Quaternion_k (from left to right).
rewrite the current goal using mul_HSNo_0R (1 ') (HSNo_conj_HSNo 1 HSNo_1) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i5 ?? (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i4 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_k (from left to right).
rewrite the current goal using OSNo_p1_k (from left to right).
We will prove 1 * k + 0 * 0 ' = - (- k).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_1L k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0R k HSNo_Quaternion_k.
∎
Theorem. (Octonion_i5_i6)
i5 ⨯ i6 = i1
In Proofgold the corresponding term root is f51c6c... and proposition id is bd260d...
Proof:
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li5i6: OSNo (i5 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i6 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i6) i1 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove 0 * 0 + - ((- j) ' * (- k)) = i.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo j HSNo_Quaternion_j (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
We will prove 0 + - (j * (- k)) = i.
rewrite the current goal using minus_mul_HSNo_distrR j k HSNo_Quaternion_j HSNo_Quaternion_k (from left to right).
rewrite the current goal using Quaternion_j_k (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L i HSNo_Complex_i.
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove (- j) * 0 + (- k) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i6_i5)
i6 ⨯ i5 = :-: i1
In Proofgold the corresponding term root is b9e439... and proposition id is b85ae9...
Proof:
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li6i5: OSNo (i6 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i5 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i5) (:-: i1) ?? (OSNo_minus_OSNo i1 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i1 ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove 0 * 0 + - ((- k) ' * (- j)) = - i.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo k HSNo_Quaternion_k (from left to right).
rewrite the current goal using conj_HSNo_k (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
We will prove 0 + - (k * (- j)) = - i.
rewrite the current goal using minus_mul_HSNo_distrR k j HSNo_Quaternion_k HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_k_j (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i).
rewrite the current goal using minus_OSNo_proj1 i1 ?? (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove (- k) * 0 + (- j) * 0 ' = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i6_i1)
i6 ⨯ i1 = i5
In Proofgold the corresponding term root is e457ad... and proposition id is a0a7b9...
Proof:
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li6i1: OSNo (i6 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i1 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i1) i5 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * i + - (0 ' * (- j)) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * 0 + (- j) * i ' = (- k).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j (- i) HSNo_Quaternion_j (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_j_i (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k).
∎
Theorem. (Octonion_i1_i6)
i1 ⨯ i6 = :-: i5
In Proofgold the corresponding term root is c1b4e0... and proposition id is bd93b5...
Proof:
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li1i6: OSNo (i1 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i1 i6 ?? ??.
Apply OSNo_proj0proj1_split (i1 ⨯ i6) (:-: i5) ?? (OSNo_minus_OSNo i5 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i5 ?? (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i1 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove i * 0 + - ((- j) ' * 0) = - 0.
rewrite the current goal using mul_HSNo_0R i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0R ((- j) ') (HSNo_conj_HSNo (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i5 ?? (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i1 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove (- j) * i + 0 * 0 ' = - (- k).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_j_i (from left to right).
rewrite the current goal using minus_HSNo_invol k HSNo_Quaternion_k (from left to right).
We will prove k + 0 = k.
An exact proof term for the current goal is add_HSNo_0R k HSNo_Quaternion_k.
∎
Theorem. (Octonion_i1_i5)
i1 ⨯ i5 = i6
In Proofgold the corresponding term root is 1e9e88... and proposition id is 3b1993...
Proof:
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li1i5: OSNo (i1 ⨯ i5).
An exact proof term for the current goal is OSNo_mul_OSNo i1 i5 ?? ??.
Apply OSNo_proj0proj1_split (i1 ⨯ i5) i6 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i1 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove i * 0 + - ((- k) ' * 0) = 0.
rewrite the current goal using mul_HSNo_0R i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0R ((- k) ') (HSNo_conj_HSNo (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i1 i5 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove (- k) * i + 0 * 0 ' = (- j).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL k i HSNo_Quaternion_k HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_k_i (from left to right).
An exact proof term for the current goal is add_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j).
∎
Theorem. (Octonion_i5_i1)
i5 ⨯ i1 = :-: i6
In Proofgold the corresponding term root is 5e4738... and proposition id is 547b1a...
Proof:
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li5: OSNo i5.
An exact proof term for the current goal is OSNo_Octonion_i5.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li5i1: OSNo (i5 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i5 i1 ?? ??.
Apply OSNo_proj0proj1_split (i5 ⨯ i1) (:-: i6) ?? (OSNo_minus_OSNo i6 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i6 ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i5 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove 0 * i + - (0 ' * (- k)) = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0L (- k) (HSNo_minus_HSNo k HSNo_Quaternion_k) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i6 ?? (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i5 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i5 (from left to right).
rewrite the current goal using OSNo_p1_i5 (from left to right).
We will prove 0 * 0 + (- k) * i ' = - (- j).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL k (- i) HSNo_Quaternion_k (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR k i HSNo_Quaternion_k HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_k_i (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L j HSNo_Quaternion_j.
∎
Theorem. (Octonion_i6_i0)
i6 ⨯ i0 = i2
In Proofgold the corresponding term root is 73d83a... and proposition id is c60735...
Proof:
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li6i0: OSNo (i6 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i0 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i0) i2 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - (1 ' * (- j)) = j.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_id_SNo 1 SNo_1 (from left to right).
rewrite the current goal using mul_HSNo_1L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L j HSNo_Quaternion_j.
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 1 * 0 + (- j) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i0_i6)
i0 ⨯ i6 = :-: i2
In Proofgold the corresponding term root is 7f039d... and proposition id is dc4654...
Proof:
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li0i6: OSNo (i0 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i6 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i6) (:-: i2) ?? (OSNo_minus_OSNo i2 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i2 ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - ((- j) ' * 1) = - j.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo j HSNo_Quaternion_j (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
We will prove 0 + - (j * 1) = - j.
rewrite the current goal using mul_HSNo_1R j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j).
rewrite the current goal using minus_OSNo_proj1 i2 ?? (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove (- j) * 0 + 1 * 0 ' = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i0_i2)
i0 ⨯ i2 = i6
In Proofgold the corresponding term root is 95da86... and proposition id is b659de...
Proof:
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li0i2: OSNo (i0 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i2 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i2) i6 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * j + - (0 ' * 1) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 0 * 0 + 1 * j ' = (- j).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_1L (j ') (HSNo_conj_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using add_HSNo_0L (j ') (HSNo_conj_HSNo j HSNo_Quaternion_j) (from left to right).
We will prove j ' = - j.
An exact proof term for the current goal is conj_HSNo_j.
∎
Theorem. (Octonion_i2_i0)
i2 ⨯ i0 = :-: i6
In Proofgold the corresponding term root is cafa53... and proposition id is 330a2a...
Proof:
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li2i0: OSNo (i2 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i2 i0 ?? ??.
Apply OSNo_proj0proj1_split (i2 ⨯ i0) (:-: i6) ?? (OSNo_minus_OSNo i6 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i6 ?? (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i2 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove j * 0 + - (1 ' * 0) = - 0.
rewrite the current goal using mul_HSNo_0R j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0R (1 ') (HSNo_conj_HSNo 1 HSNo_1) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i6 ?? (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i2 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
We will prove 1 * j + 0 * 0 ' = - (- j).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_invol j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_1L j HSNo_Quaternion_j (from left to right).
An exact proof term for the current goal is add_HSNo_0R j HSNo_Quaternion_j.
∎
Theorem. (Octonion_i2_i6)
i2 ⨯ i6 = i0
In Proofgold the corresponding term root is 787314... and proposition id is b9cfda...
Proof:
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li2i6: OSNo (i2 ⨯ i6).
An exact proof term for the current goal is OSNo_mul_OSNo i2 i6 ?? ??.
Apply OSNo_proj0proj1_split (i2 ⨯ i6) i0 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i2 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove j * 0 + - ((- j) ' * 0) = 0.
rewrite the current goal using mul_HSNo_0R j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0R ((- j) ') (HSNo_conj_HSNo (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i2 i6 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove (- j) * j + 0 * 0 ' = 1.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_j_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0R 1 HSNo_1.
∎
Theorem. (Octonion_i6_i2)
i6 ⨯ i2 = :-: i0
In Proofgold the corresponding term root is 158a18... and proposition id is cd6dcf...
Proof:
We prove the intermediate claim Li2: OSNo i2.
An exact proof term for the current goal is OSNo_Quaternion_j.
We prove the intermediate claim Li6: OSNo i6.
An exact proof term for the current goal is OSNo_Octonion_i6.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li6i2: OSNo (i6 ⨯ i2).
An exact proof term for the current goal is OSNo_mul_OSNo i6 i2 ?? ??.
Apply OSNo_proj0proj1_split (i6 ⨯ i2) (:-: i0) ?? (OSNo_minus_OSNo i0 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i0 ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i6 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove 0 * j + - (0 ' * (- j)) = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L j HSNo_Quaternion_j (from left to right).
rewrite the current goal using mul_HSNo_0L (- j) (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i0 ?? (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i6 i2 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_j (from left to right).
rewrite the current goal using OSNo_p1_j (from left to right).
rewrite the current goal using OSNo_p0_i6 (from left to right).
rewrite the current goal using OSNo_p1_i6 (from left to right).
We will prove 0 * 0 + (- j) * j ' = - 1.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_j (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL j (- j) HSNo_Quaternion_j (HSNo_minus_HSNo j HSNo_Quaternion_j) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).
rewrite the current goal using Quaternion_j_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- 1) (HSNo_minus_HSNo 1 HSNo_1).
∎
Theorem. (Octonion_i0_i1)
i0 ⨯ i1 = i3
In Proofgold the corresponding term root is b43708... and proposition id is 251b34...
Proof:
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li0i1: OSNo (i0 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i1 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i1) i3 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * i + - (0 ' * 1) = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 0 * 0 + 1 * i ' = (- i).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_1L (i ') (HSNo_conj_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using add_HSNo_0L (i ') (HSNo_conj_HSNo i HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is conj_HSNo_i.
∎
Theorem. (Octonion_i1_i0)
i1 ⨯ i0 = :-: i3
In Proofgold the corresponding term root is 9cb018... and proposition id is 9165d8...
Proof:
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li1i0: OSNo (i1 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i1 i0 ?? ??.
Apply OSNo_proj0proj1_split (i1 ⨯ i0) (:-: i3) ?? (OSNo_minus_OSNo i3 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i3 ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i1 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove i * 0 + - (1 ' * 0) = - 0.
rewrite the current goal using mul_HSNo_0R i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0R (1 ') (HSNo_conj_HSNo 1 HSNo_1) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i3 ?? (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i1 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
We will prove 1 * i + 0 * 0 ' = - (- i).
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_1L i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0R i HSNo_Complex_i.
∎
Theorem. (Octonion_i1_i3)
i1 ⨯ i3 = i0
In Proofgold the corresponding term root is 3cc4e3... and proposition id is f71c20...
Proof:
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li1i3: OSNo (i1 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i1 i3 ?? ??.
Apply OSNo_proj0proj1_split (i1 ⨯ i3) i0 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i1 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove i * 0 + - ((- i) ' * 0) = 0.
rewrite the current goal using mul_HSNo_0R i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0R ((- i) ') (HSNo_conj_HSNo (- i) (HSNo_minus_HSNo i HSNo_Complex_i)) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i1 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove (- i) * i + 0 * 0 ' = 1.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i i HSNo_Complex_i HSNo_Complex_i (from left to right).
We will prove - i * i + 0 = 1.
rewrite the current goal using Quaternion_i_sqr (from left to right).
We will prove - - 1 + 0 = 1.
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0R 1 HSNo_1.
∎
Theorem. (Octonion_i3_i1)
i3 ⨯ i1 = :-: i0
In Proofgold the corresponding term root is 2603e9... and proposition id is 105f8c...
Proof:
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li3i1: OSNo (i3 ⨯ i1).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i1 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i1) (:-: i0) ?? (OSNo_minus_OSNo i0 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i0 ?? (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove 0 * i + - (0 ' * (- i)) = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0L i HSNo_Complex_i (from left to right).
rewrite the current goal using mul_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
rewrite the current goal using minus_OSNo_proj1 i0 ?? (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i1 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
We will prove 0 * 0 + (- i) * i ' = - 1.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_mul_HSNo_distrL i (- i) HSNo_Complex_i (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_mul_HSNo_distrR i i HSNo_Complex_i HSNo_Complex_i (from left to right).
rewrite the current goal using Quaternion_i_sqr (from left to right).
rewrite the current goal using minus_HSNo_invol 1 HSNo_1 (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- 1) (HSNo_minus_HSNo 1 HSNo_1).
∎
Theorem. (Octonion_i3_i0)
i3 ⨯ i0 = i1
In Proofgold the corresponding term root is 902425... and proposition id is cf0eac...
Proof:
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li3i0: OSNo (i3 ⨯ i0).
An exact proof term for the current goal is OSNo_mul_OSNo i3 i0 ?? ??.
Apply OSNo_proj0proj1_split (i3 ⨯ i0) i1 ?? ?? to the current goal.
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i3 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - (1 ' * (- i)) = i.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_HSNo_id_SNo 1 SNo_1 (from left to right).
rewrite the current goal using mul_HSNo_1L (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L i HSNo_Complex_i.
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i3 i0 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 1 * 0 + (- i) * 0 ' = 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
Theorem. (Octonion_i0_i3)
i0 ⨯ i3 = :-: i1
In Proofgold the corresponding term root is 73d689... and proposition id is c0f00e...
Proof:
We prove the intermediate claim Li3: OSNo i3.
An exact proof term for the current goal is OSNo_Octonion_i3.
We prove the intermediate claim Li0: OSNo i0.
An exact proof term for the current goal is OSNo_Octonion_i0.
We prove the intermediate claim Li1: OSNo i1.
An exact proof term for the current goal is OSNo_Complex_i.
We prove the intermediate claim Li0i3: OSNo (i0 ⨯ i3).
An exact proof term for the current goal is OSNo_mul_OSNo i0 i3 ?? ??.
Apply OSNo_proj0proj1_split (i0 ⨯ i3) (:-: i1) ?? (OSNo_minus_OSNo i1 ??) to the current goal.
rewrite the current goal using minus_OSNo_proj0 i1 ?? (from left to right).
rewrite the current goal using OSNo_p0_i (from left to right).
rewrite the current goal using mul_OSNo_proj0 i0 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove 0 * 0 + - ((- i) ' * 1) = - i.
rewrite the current goal using mul_HSNo_0L 0 HSNo_0 (from left to right).
rewrite the current goal using conj_minus_HSNo i HSNo_Complex_i (from left to right).
rewrite the current goal using conj_HSNo_i (from left to right).
rewrite the current goal using minus_HSNo_invol i HSNo_Complex_i (from left to right).
We will prove 0 + - (i * 1) = - i.
rewrite the current goal using mul_HSNo_1R i HSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_HSNo_0L (- i) (HSNo_minus_HSNo i HSNo_Complex_i).
rewrite the current goal using minus_OSNo_proj1 i1 ?? (from left to right).
rewrite the current goal using OSNo_p1_i (from left to right).
rewrite the current goal using mul_OSNo_proj1 i0 i3 ?? ?? (from left to right).
rewrite the current goal using OSNo_p0_i3 (from left to right).
rewrite the current goal using OSNo_p1_i3 (from left to right).
rewrite the current goal using OSNo_p0_i0 (from left to right).
rewrite the current goal using OSNo_p1_i0 (from left to right).
We will prove (- i) * 0 + 1 * 0 ' = - 0.
rewrite the current goal using conj_HSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R 1 HSNo_1 (from left to right).
rewrite the current goal using minus_HSNo_0 (from left to right).
rewrite the current goal using mul_HSNo_0R (- i) (HSNo_minus_HSNo i HSNo_Complex_i) (from left to right).
An exact proof term for the current goal is add_HSNo_0L 0 HSNo_0.
∎
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.
Let i0 ≝ Octonion_i0
Let i1 ≝ Complex_i
Let i2 ≝ Quaternion_j
Let i3 ≝ Octonion_i3
Let i4 ≝ Quaternion_k
Let i5 ≝ Octonion_i5
Let i6 ≝ Octonion_i6
Let i ≝ Complex_i
Let j ≝ Quaternion_j
Let k ≝ Quaternion_k
Let p0 : set → set ≝ OSNo_proj0
Let p1 : set → set ≝ OSNo_proj1
Let pa : set → set → set ≝ HSNo_pair
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...
Theorem. (octonion_I)
∀x y ∈ quaternion, pa x y ∈ octonion
In Proofgold the corresponding term root is f43249... and proposition id is dd28a1...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We will prove pa x y ∈ octonion.
rewrite the current goal using tuple_2_0_eq x y (from right to left).
rewrite the current goal using tuple_2_1_eq x y (from right to left) at position 2.
We will prove pa ((x,y) 0) ((x,y) 1) ∈ octonion.
Apply ReplI (quaternion ⨯ quaternion) (λu ⇒ pa (u 0) (u 1)) to the current goal.
We will prove (x,y) ∈ quaternion ⨯ quaternion.
An exact proof term for the current goal is tuple_2_setprod quaternion quaternion x Hx y Hy.
∎
Theorem. (octonion_E)
∀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...
Proof:
Let z be given.
Assume Hz.
Let p be given.
Assume Hp.
Apply ReplE_impred (quaternion ⨯ quaternion) (λu ⇒ pa (u 0) (u 1)) z Hz to the current goal.
Let u be given.
Assume Hu: u ∈ quaternion ⨯ quaternion.
Assume Hzu: z = pa (u 0) (u 1).
An exact proof term for the current goal is Hp (u 0) (ap0_Sigma quaternion (λ_ ⇒ quaternion) u Hu) (u 1) (ap1_Sigma quaternion (λ_ ⇒ quaternion) u Hu) Hzu.
∎
Theorem. (octonion_OSNo)
∀z ∈ octonion, OSNo z
In Proofgold the corresponding term root is 9d2e4f... and proposition id is 7590f8...
Proof:
Let z be given.
Assume Hz.
Apply octonion_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Assume Hzxy: z = pa x y.
We will prove OSNo z.
rewrite the current goal using Hzxy (from left to right).
Apply OSNo_I to the current goal.
An exact proof term for the current goal is quaternion_HSNo x Hx.
An exact proof term for the current goal is quaternion_HSNo y Hy.
∎
Theorem. (quaternion_octonion)
quaternion ⊆ octonion
In Proofgold the corresponding term root is 07aea1... and proposition id is a740e9...
Proof:
Let x be given.
Assume Hx: x ∈ quaternion.
We will prove x ∈ octonion.
rewrite the current goal using HSNo_pair_0 x (from right to left).
We will prove pa x 0 ∈ octonion.
Apply octonion_I to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is quaternion_0.
∎
Theorem. (octonion_0)
0 ∈ octonion
In Proofgold the corresponding term root is b78b5b... and proposition id is 27f55c...
Proof:
An exact proof term for the current goal is quaternion_octonion 0 quaternion_0.
∎
Theorem. (octonion_1)
1 ∈ octonion
In Proofgold the corresponding term root is 6b24ca... and proposition id is 0db162...
Proof:
An exact proof term for the current goal is quaternion_octonion 1 quaternion_1.
∎
Theorem. (octonion_i)
i ∈ octonion
In Proofgold the corresponding term root is 19312b... and proposition id is 8de3fa...
Proof:
An exact proof term for the current goal is quaternion_octonion i quaternion_i.
∎
Theorem. (octonion_j)
j ∈ octonion
In Proofgold the corresponding term root is 7c86a8... and proposition id is 72f255...
Proof:
An exact proof term for the current goal is quaternion_octonion j quaternion_j.
∎
Theorem. (octonion_k)
k ∈ octonion
In Proofgold the corresponding term root is 18b0b4... and proposition id is b1a0f0...
Proof:
An exact proof term for the current goal is quaternion_octonion k quaternion_k.
∎
Theorem. (octonion_i0)
i0 ∈ octonion
In Proofgold the corresponding term root is 920cc3... and proposition id is 92ff8b...
Proof:
We will prove pa 0 1 ∈ octonion.
Apply octonion_I to the current goal.
An exact proof term for the current goal is quaternion_0.
An exact proof term for the current goal is quaternion_1.
∎
Theorem. (octonion_i3)
i3 ∈ octonion
In Proofgold the corresponding term root is b1ffb8... and proposition id is a130b1...
Proof:
We will prove pa 0 (minus_HSNo i) ∈ octonion.
Apply octonion_I to the current goal.
An exact proof term for the current goal is quaternion_0.
Apply quaternion_minus_HSNo to the current goal.
An exact proof term for the current goal is quaternion_i.
∎
Theorem. (octonion_i5)
i5 ∈ octonion
In Proofgold the corresponding term root is 4f9ec6... and proposition id is 269f68...
Proof:
We will prove pa 0 (minus_HSNo k) ∈ octonion.
Apply octonion_I to the current goal.
An exact proof term for the current goal is quaternion_0.
Apply quaternion_minus_HSNo to the current goal.
An exact proof term for the current goal is quaternion_k.
∎
Theorem. (octonion_i6)
i6 ∈ octonion
In Proofgold the corresponding term root is 57dd50... and proposition id is 70b59d...
Proof:
We will prove pa 0 (minus_HSNo j) ∈ octonion.
Apply octonion_I to the current goal.
An exact proof term for the current goal is quaternion_0.
Apply quaternion_minus_HSNo to the current goal.
An exact proof term for the current goal is quaternion_j.
∎
Theorem. (octonion_p0_eq)
∀x y ∈ quaternion, p0 (pa x y) = x
In Proofgold the corresponding term root is d31937... and proposition id is d69485...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
An exact proof term for the current goal is OSNo_proj0_2 x y (quaternion_HSNo x Hx) (quaternion_HSNo y Hy).
∎
Theorem. (octonion_p1_eq)
∀x y ∈ quaternion, p1 (pa x y) = y
In Proofgold the corresponding term root is 6ca6c3... and proposition id is f4be43...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
An exact proof term for the current goal is OSNo_proj1_2 x y (quaternion_HSNo x Hx) (quaternion_HSNo y Hy).
∎
Theorem. (octonion_p0_quaternion)
∀z ∈ octonion, p0 z ∈ quaternion
In Proofgold the corresponding term root is 63ea34... and proposition id is e55972...
Proof:
Let z be given.
Assume Hz.
Apply octonion_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
We will prove p0 (pa x y) ∈ quaternion.
rewrite the current goal using octonion_p0_eq x Hx y Hy (from left to right).
We will prove x ∈ quaternion.
An exact proof term for the current goal is Hx.
∎
Theorem. (octonion_p1_quaternion)
∀z ∈ octonion, p1 z ∈ quaternion
In Proofgold the corresponding term root is de6ec0... and proposition id is ecc213...
Proof:
Let z be given.
Assume Hz.
Apply octonion_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
We will prove p1 (pa x y) ∈ quaternion.
rewrite the current goal using octonion_p1_eq x Hx y Hy (from left to right).
We will prove y ∈ quaternion.
An exact proof term for the current goal is Hy.
∎
Theorem. (octonion_proj0proj1_split)
∀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...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
An exact proof term for the current goal is OSNo_proj0proj1_split z w (octonion_OSNo z Hz) (octonion_OSNo w Hw).
∎
Theorem. (octonion_minus_OSNo)
∀z ∈ octonion, - z ∈ octonion
In Proofgold the corresponding term root is 5ae75b... and proposition id is 41d946...
Proof:
Let z be given.
Assume Hz.
We will prove pa (minus_HSNo (p0 z)) (minus_HSNo (p1 z)) ∈ octonion.
Apply octonion_I to the current goal.
Apply quaternion_minus_HSNo to the current goal.
An exact proof term for the current goal is octonion_p0_quaternion z Hz.
Apply quaternion_minus_HSNo to the current goal.
An exact proof term for the current goal is octonion_p1_quaternion z Hz.
∎
Theorem. (octonion_conj_OSNo)
∀z ∈ octonion, conj_OSNo z ∈ octonion
In Proofgold the corresponding term root is b7a7a4... and proposition id is d72ac7...
Proof:
Let z be given.
Assume Hz.
We will prove pa (conj_HSNo (p0 z)) (minus_HSNo (p1 z)) ∈ octonion.
Apply octonion_I to the current goal.
Apply quaternion_conj_HSNo to the current goal.
An exact proof term for the current goal is octonion_p0_quaternion z Hz.
Apply quaternion_minus_HSNo to the current goal.
An exact proof term for the current goal is octonion_p1_quaternion z Hz.
∎
Theorem. (octonion_add_OSNo)
∀z w ∈ octonion, z + w ∈ octonion
In Proofgold the corresponding term root is 8e6d64... and proposition id is f59ccf...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_HSNo (p0 z) (p0 w)) (add_HSNo (p1 z) (p1 w)) ∈ octonion.
Apply octonion_I to the current goal.
Apply quaternion_add_HSNo to the current goal.
An exact proof term for the current goal is octonion_p0_quaternion z Hz.
An exact proof term for the current goal is octonion_p0_quaternion w Hw.
Apply quaternion_add_HSNo to the current goal.
An exact proof term for the current goal is octonion_p1_quaternion z Hz.
An exact proof term for the current goal is octonion_p1_quaternion w Hw.
∎
Theorem. (octonion_mul_OSNo)
∀z w ∈ octonion, z * w ∈ octonion
In Proofgold the corresponding term root is 1d3e8a... and proposition id is b76bb1...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_HSNo (mul_HSNo (p0 z) (p0 w)) (minus_HSNo (mul_HSNo (conj_HSNo (p1 w)) (p1 z)))) (add_HSNo (mul_HSNo (p1 w) (p0 z)) (mul_HSNo (p1 z) (conj_HSNo (p0 w)))) ∈ octonion.
We prove the intermediate claim Lz0: p0 z ∈ quaternion.
An exact proof term for the current goal is octonion_p0_quaternion z Hz.
We prove the intermediate claim Lz1: p1 z ∈ quaternion.
An exact proof term for the current goal is octonion_p1_quaternion z Hz.
We prove the intermediate claim Lw0: p0 w ∈ quaternion.
An exact proof term for the current goal is octonion_p0_quaternion w Hw.
We prove the intermediate claim Lw1: p1 w ∈ quaternion.
An exact proof term for the current goal is octonion_p1_quaternion w Hw.
Apply octonion_I to the current goal.
Apply quaternion_add_HSNo to the current goal.
Apply quaternion_mul_HSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply quaternion_minus_HSNo to the current goal.
Apply quaternion_mul_HSNo to the current goal.
Apply quaternion_conj_HSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply quaternion_add_HSNo to the current goal.
Apply quaternion_mul_HSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply quaternion_mul_HSNo to the current goal.
An exact proof term for the current goal is ??.
Apply quaternion_conj_HSNo to the current goal.
An exact proof term for the current goal is ??.
∎
Theorem. (quaternion_p0_eq')
∀x ∈ quaternion, p0 x = x
In Proofgold the corresponding term root is 6b0e75... and proposition id is fc55a6...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using HSNo_pair_0 x (from right to left) at position 1.
An exact proof term for the current goal is octonion_p0_eq x Hx 0 quaternion_0.
∎
Theorem. (quaternion_p1_eq')
∀x ∈ quaternion, p1 x = 0
In Proofgold the corresponding term root is 7e57a1... and proposition id is d3a12f...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using HSNo_pair_0 x (from right to left).
An exact proof term for the current goal is octonion_p1_eq x Hx 0 quaternion_0.
∎
End of Section Octonions