Proofgold Asset

Param complex^complex : ι
Param pair_tag^pair_tag : ι → ι → ι → ι
Param CD_proj0^CD_proj0 : ι → (ι → ο) → ι → ι
Param CD_proj1^CD_proj1 : ι → (ι → ο) → ι → ι
Definition CD_conj^CD_conj := λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 . pair_tag x0 (x3 (CD_proj0 x0 x1 x4)) (x2 (CD_proj1 x0 x1 x4))
Param Sing^Sing : ι → ι
Param ordsucc^ordsucc : ι → ι
Param SNo^SNo : ι → ο
Param minus_SNo^minus_SNo : ι → ι
Definition conj_CSNo^conj_CSNo := CD_conj (Sing 2) SNo minus_SNo (λ x0 . x0)
Definition CSNo_Im^CSNo_Im := CD_proj1 (Sing 2) SNo
Definition CSNo_Re^CSNo_Re := CD_proj0 (Sing 2) SNo
Param real^real : ι
Definition SNo_pair^SNo_pair := pair_tag (Sing 2)
Known complex_I^complex_I : ∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ SNo_pair x0 x1 ∈ complex
Known complex_Re_real^{complex_Re_real} : ∀ x0 . x0 ∈ complex ⟶ CSNo_Re x0 ∈ real
Known real_minus_SNo^{real_minus_SNo} : ∀ x0 . x0 ∈ real ⟶ minus_SNo x0 ∈ real
Known complex_Im_real^{complex_Im_real} : ∀ x0 . x0 ∈ complex ⟶ CSNo_Im x0 ∈ real
Theorem complex_conj_CSNo^{complex_conj_CSNo} : ∀ x0 . x0 ∈ complex ⟶ conj_CSNo x0 ∈ complex (proof)
Param lam^Sigma : ι → (ι → ι) → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition CSNo_pair^CSNo_pair := pair_tag (Sing 3)
Param ap^ap : ι → ι → ι
Definition quaternion^quaternion := {CSNo_pair (ap x0 0) (ap x0 1)|x0 ∈ setprod complex complex}
Param If_i^If_i : ο → ι → ι → ι
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known tuple_2_setprod^{tuple_2_setprod} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ setprod x0 x1
Theorem quaternion_I^quaternion_I : ∀ x0 . x0 ∈ complex ⟶ ∀ x1 . x1 ∈ complex ⟶ CSNo_pair x0 x1 ∈ quaternion (proof)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Theorem quaternion_E^quaternion_E : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ complex ⟶ ∀ x3 . x3 ∈ complex ⟶ x0 = CSNo_pair x2 x3 ⟶ x1) ⟶ x1 (proof)
Param HSNo^HSNo : ι → ο
Param CSNo^CSNo : ι → ο
Known HSNo_I^HSNo_I : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ HSNo (CSNo_pair x0 x1)
Known complex_CSNo^complex_CSNo : ∀ x0 . x0 ∈ complex ⟶ CSNo x0
Theorem quaternion_HSNo^{quaternion_HSNo} : ∀ x0 . x0 ∈ quaternion ⟶ HSNo x0 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known CSNo_pair_0^CSNo_pair_0 : ∀ x0 . CSNo_pair x0 0 = x0
Known complex_0^complex_0 : 0 ∈ complex
Theorem complex_quaternion^{complex_quaternion} : complex ⊆ quaternion (proof)
Theorem quaternion_0^quaternion_0 : 0 ∈ quaternion (proof)
Known complex_1^complex_1 : 1 ∈ complex
Theorem quaternion_1^quaternion_1 : 1 ∈ quaternion (proof)
Param Complex_i^Complex_i : ι
Known complex_i^complex_i : Complex_i ∈ complex
Theorem quaternion_i^quaternion_i : Complex_i ∈ quaternion (proof)
Definition Quaternion_j^Quaternion_j := CSNo_pair 0 1
Theorem quaternion_j^quaternion_j : Quaternion_j ∈ quaternion (proof)
Definition Quaternion_k^Quaternion_k := CSNo_pair 0 Complex_i
Theorem quaternion_k^quaternion_k : Quaternion_k ∈ quaternion (proof)
Definition HSNo_proj0^HSNo_proj0 := CD_proj0 (Sing 3) CSNo
Known HSNo_proj0_2^HSNo_proj0_2 : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ HSNo_proj0 (CSNo_pair x0 x1) = x0
Theorem quaternion_p0_eq^{quaternion_p0_eq} : ∀ x0 . x0 ∈ complex ⟶ ∀ x1 . x1 ∈ complex ⟶ HSNo_proj0 (CSNo_pair x0 x1) = x0 (proof)
Definition HSNo_proj1^HSNo_proj1 := CD_proj1 (Sing 3) CSNo
Known HSNo_proj1_2^HSNo_proj1_2 : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ HSNo_proj1 (CSNo_pair x0 x1) = x1
Theorem quaternion_p1_eq^{quaternion_p1_eq} : ∀ x0 . x0 ∈ complex ⟶ ∀ x1 . x1 ∈ complex ⟶ HSNo_proj1 (CSNo_pair x0 x1) = x1 (proof)
Theorem quaternion_p0_complex^{quaternion_p0_complex} : ∀ x0 . x0 ∈ quaternion ⟶ HSNo_proj0 x0 ∈ complex (proof)
Theorem quaternion_p1_complex^{quaternion_p1_complex} : ∀ x0 . x0 ∈ quaternion ⟶ HSNo_proj1 x0 ∈ complex (proof)
Known HSNo_proj0proj1_split^{HSNo_proj0proj1_split} : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ HSNo_proj0 x0 = HSNo_proj0 x1 ⟶ HSNo_proj1 x0 = HSNo_proj1 x1 ⟶ x0 = x1
Theorem quaternion_proj0proj1_split^{quaternion_proj0proj1_split} : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ HSNo_proj0 x0 = HSNo_proj0 x1 ⟶ HSNo_proj1 x0 = HSNo_proj1 x1 ⟶ x0 = x1 (proof)
Definition CD_minus^CD_minus := λ x0 . λ x1 : ι → ο . λ x2 : ι → ι . λ x3 . pair_tag x0 (x2 (CD_proj0 x0 x1 x3)) (x2 (CD_proj1 x0 x1 x3))
Param minus_CSNo^minus_CSNo : ι → ι
Definition minus_HSNo^minus_HSNo := CD_minus (Sing 3) CSNo minus_CSNo
Known complex_minus_CSNo^{complex_minus_CSNo} : ∀ x0 . x0 ∈ complex ⟶ minus_CSNo x0 ∈ complex
Theorem quaternion_minus_HSNo^{quaternion_minus_HSNo} : ∀ x0 . x0 ∈ quaternion ⟶ minus_HSNo x0 ∈ quaternion (proof)
Definition conj_HSNo^conj_HSNo := CD_conj (Sing 3) CSNo minus_CSNo conj_CSNo
Theorem quaternion_conj_HSNo^{quaternion_conj_HSNo} : ∀ x0 . x0 ∈ quaternion ⟶ conj_HSNo x0 ∈ quaternion (proof)
Definition CD_add^CD_add := λ x0 . λ x1 : ι → ο . λ x2 : ι → ι → ι . λ x3 x4 . pair_tag x0 (x2 (CD_proj0 x0 x1 x3) (CD_proj0 x0 x1 x4)) (x2 (CD_proj1 x0 x1 x3) (CD_proj1 x0 x1 x4))
Param add_CSNo^add_CSNo : ι → ι → ι
Definition add_HSNo^add_HSNo := CD_add (Sing 3) CSNo add_CSNo
Known complex_add_CSNo^{complex_add_CSNo} : ∀ x0 . x0 ∈ complex ⟶ ∀ x1 . x1 ∈ complex ⟶ add_CSNo x0 x1 ∈ complex
Theorem quaternion_add_HSNo^{quaternion_add_HSNo} : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ add_HSNo x0 x1 ∈ quaternion (proof)
Definition CD_mul^CD_mul := λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 x5 : ι → ι → ι . λ x6 x7 . pair_tag x0 (x4 (x5 (CD_proj0 x0 x1 x6) (CD_proj0 x0 x1 x7)) (x2 (x5 (x3 (CD_proj1 x0 x1 x7)) (CD_proj1 x0 x1 x6)))) (x4 (x5 (CD_proj1 x0 x1 x7) (CD_proj0 x0 x1 x6)) (x5 (CD_proj1 x0 x1 x6) (x3 (CD_proj0 x0 x1 x7))))
Param mul_CSNo^mul_CSNo : ι → ι → ι
Definition mul_HSNo^mul_HSNo := CD_mul (Sing 3) CSNo minus_CSNo conj_CSNo add_CSNo mul_CSNo
Known complex_mul_CSNo^{complex_mul_CSNo} : ∀ x0 . x0 ∈ complex ⟶ ∀ x1 . x1 ∈ complex ⟶ mul_CSNo x0 x1 ∈ complex
Theorem quaternion_mul_HSNo^{quaternion_mul_HSNo} : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ mul_HSNo x0 x1 ∈ quaternion (proof)
Theorem complex_p0_eq^{complex_p0_eq} : ∀ x0 . x0 ∈ complex ⟶ HSNo_proj0 x0 = x0 (proof)
Theorem complex_p1_eq^{complex_p1_eq} : ∀ x0 . x0 ∈ complex ⟶ HSNo_proj1 x0 = 0 (proof)
Definition HSNo_pair^HSNo_pair := pair_tag (Sing 4)
Definition octonion^octonion := {HSNo_pair (ap x0 0) (ap x0 1)|x0 ∈ setprod quaternion quaternion}
Theorem octonion_I^octonion_I : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ HSNo_pair x0 x1 ∈ octonion (proof)
Theorem octonion_E^octonion_E : ∀ x0 . x0 ∈ octonion ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ quaternion ⟶ ∀ x3 . x3 ∈ quaternion ⟶ x0 = HSNo_pair x2 x3 ⟶ x1) ⟶ x1 (proof)
Param OSNo^OSNo : ι → ο
Known OSNo_I^OSNo_I : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ OSNo (HSNo_pair x0 x1)
Theorem octonion_OSNo^{octonion_OSNo} : ∀ x0 . x0 ∈ octonion ⟶ OSNo x0 (proof)
Known HSNo_pair_0^HSNo_pair_0 : ∀ x0 . HSNo_pair x0 0 = x0
Theorem quaternion_octonion^{quaternion_octonion} : quaternion ⊆ octonion (proof)
Theorem octonion_0^octonion_0 : 0 ∈ octonion (proof)
Theorem octonion_1^octonion_1 : 1 ∈ octonion (proof)
Theorem octonion_i^octonion_i : Complex_i ∈ octonion (proof)
Theorem octonion_j^octonion_j : Quaternion_j ∈ octonion (proof)
Theorem octonion_k^octonion_k : Quaternion_k ∈ octonion (proof)
Definition Octonion_i0^Octonion_i0 := HSNo_pair 0 1
Theorem octonion_i0^octonion_i0 : Octonion_i0 ∈ octonion (proof)
Definition Octonion_i3^Octonion_i3 := HSNo_pair 0 (minus_HSNo Complex_i)
Theorem octonion_i3^octonion_i3 : Octonion_i3 ∈ octonion (proof)
Definition Octonion_i5^Octonion_i5 := HSNo_pair 0 (minus_HSNo Quaternion_k)
Theorem octonion_i5^octonion_i5 : Octonion_i5 ∈ octonion (proof)
Definition Octonion_i6^Octonion_i6 := HSNo_pair 0 (minus_HSNo Quaternion_j)
Theorem octonion_i6^octonion_i6 : Octonion_i6 ∈ octonion (proof)
Definition OSNo_proj0^OSNo_proj0 := CD_proj0 (Sing 4) HSNo
Known OSNo_proj0_2^OSNo_proj0_2 : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ OSNo_proj0 (HSNo_pair x0 x1) = x0
Theorem octonion_p0_eq^{octonion_p0_eq} : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ OSNo_proj0 (HSNo_pair x0 x1) = x0 (proof)
Definition OSNo_proj1^OSNo_proj1 := CD_proj1 (Sing 4) HSNo
Known OSNo_proj1_2^OSNo_proj1_2 : ∀ x0 x1 . HSNo x0 ⟶ HSNo x1 ⟶ OSNo_proj1 (HSNo_pair x0 x1) = x1
Theorem octonion_p1_eq^{octonion_p1_eq} : ∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ OSNo_proj1 (HSNo_pair x0 x1) = x1 (proof)
Theorem octonion_p0_quaternion^{octonion_p0_quaternion} : ∀ x0 . x0 ∈ octonion ⟶ OSNo_proj0 x0 ∈ quaternion (proof)
Theorem octonion_p1_quaternion^{octonion_p1_quaternion} : ∀ x0 . x0 ∈ octonion ⟶ OSNo_proj1 x0 ∈ quaternion (proof)
Known OSNo_proj0proj1_split^{OSNo_proj0proj1_split} : ∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj0 x0 = OSNo_proj0 x1 ⟶ OSNo_proj1 x0 = OSNo_proj1 x1 ⟶ x0 = x1
Theorem octonion_proj0proj1_split^{octonion_proj0proj1_split} : ∀ x0 . x0 ∈ octonion ⟶ ∀ x1 . x1 ∈ octonion ⟶ OSNo_proj0 x0 = OSNo_proj0 x1 ⟶ OSNo_proj1 x0 = OSNo_proj1 x1 ⟶ x0 = x1 (proof)
Definition minus_OSNo^minus_OSNo := CD_minus (Sing 4) HSNo minus_HSNo
Theorem octonion_minus_OSNo^{octonion_minus_OSNo} : ∀ x0 . x0 ∈ octonion ⟶ minus_OSNo x0 ∈ octonion (proof)
Definition conj_OSNo^conj_OSNo := CD_conj (Sing 4) HSNo minus_HSNo conj_HSNo
Theorem octonion_conj_OSNo^{octonion_conj_OSNo} : ∀ x0 . x0 ∈ octonion ⟶ conj_OSNo x0 ∈ octonion (proof)
Definition add_OSNo^add_OSNo := CD_add (Sing 4) HSNo add_HSNo
Theorem octonion_add_OSNo^{octonion_add_OSNo} : ∀ x0 . x0 ∈ octonion ⟶ ∀ x1 . x1 ∈ octonion ⟶ add_OSNo x0 x1 ∈ octonion (proof)
Definition mul_OSNo^mul_OSNo := CD_mul (Sing 4) HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo
Theorem octonion_mul_OSNo^{octonion_mul_OSNo} : ∀ x0 . x0 ∈ octonion ⟶ ∀ x1 . x1 ∈ octonion ⟶ mul_OSNo x0 x1 ∈ octonion (proof)
Theorem quaternion_p0_eq'^{quaternion_p0_eq} : ∀ x0 . x0 ∈ quaternion ⟶ OSNo_proj0 x0 = x0 (proof)
Theorem quaternion_p1_eq'^{quaternion_p1_eq} : ∀ x0 . x0 ∈ quaternion ⟶ OSNo_proj1 x0 = 0 (proof)