Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: HSNo (mul_HSNo Quaternion_k Quaternion_k)
Apply HSNo_mul_HSNo with Quaternion_k, Quaternion_k leaving 2 subgoals.
The subproof is completed by applying HSNo_Quaternion_k.
The subproof is completed by applying HSNo_Quaternion_k.
Claim L1: HSNo (minus_HSNo 1)
Apply HSNo_minus_HSNo with 1.
The subproof is completed by applying HSNo_1.
Apply HSNo_proj0proj1_split with mul_HSNo Quaternion_k Quaternion_k, minus_HSNo 1 leaving 4 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply mul_HSNo_proj0 with Quaternion_k, Quaternion_k, λ x0 x1 . x1 = HSNo_proj0 (minus_HSNo 1) leaving 3 subgoals.
The subproof is completed by applying HSNo_Quaternion_k.
The subproof is completed by applying HSNo_Quaternion_k.
Apply minus_HSNo_proj0 with 1, λ x0 x1 . add_CSNo (mul_CSNo (HSNo_proj0 Quaternion_k) (HSNo_proj0 Quaternion_k)) (minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj1 Quaternion_k)) (HSNo_proj1 Quaternion_k))) = x1 leaving 2 subgoals.
The subproof is completed by applying HSNo_1.
Apply HSNo_p0_k with λ x0 x1 . add_CSNo (mul_CSNo x1 x1) (minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj1 Quaternion_k)) (HSNo_proj1 Quaternion_k))) = minus_CSNo (HSNo_proj0 1).
Apply HSNo_p1_k with λ x0 x1 . add_CSNo (mul_CSNo 0 0) (minus_CSNo (mul_CSNo (conj_CSNo x1) x1)) = minus_CSNo (HSNo_proj0 1).
Apply CSNo_HSNo_proj0 with 1, λ x0 x1 . add_CSNo (mul_CSNo 0 0) (minus_CSNo (mul_CSNo (conj_CSNo Complex_i) Complex_i)) = minus_CSNo x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_1.
Apply mul_CSNo_0L with 0, λ x0 x1 . add_CSNo x1 (minus_CSNo (mul_CSNo (conj_CSNo Complex_i) Complex_i)) = minus_CSNo 1 leaving 2 subgoals.
The subproof is completed by applying CSNo_0.
Apply conj_CSNo_i with λ x0 x1 . add_CSNo 0 (minus_CSNo (mul_CSNo x1 Complex_i)) = minus_CSNo 1.
Apply minus_mul_CSNo_distrL with minus_CSNo Complex_i, Complex_i, λ x0 x1 . add_CSNo 0 x0 = minus_CSNo 1 leaving 3 subgoals.
Apply CSNo_minus_CSNo with Complex_i.
The subproof is completed by applying CSNo_Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Apply minus_CSNo_invol with Complex_i, λ x0 x1 . add_CSNo 0 (mul_CSNo x1 Complex_i) = minus_CSNo 1 leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
Apply Complex_i_sqr with λ x0 x1 . add_CSNo 0 x1 = minus_CSNo 1.
Apply add_CSNo_0L with minus_CSNo 1.
Apply CSNo_minus_CSNo with 1.
The subproof is completed by applying CSNo_1.
Apply mul_HSNo_proj1 with Quaternion_k, Quaternion_k, λ x0 x1 . x1 = HSNo_proj1 (minus_HSNo 1) leaving 3 subgoals.
The subproof is completed by applying HSNo_Quaternion_k.
The subproof is completed by applying HSNo_Quaternion_k.
Apply minus_HSNo_proj1 with 1, λ x0 x1 . add_CSNo (mul_CSNo (HSNo_proj1 Quaternion_k) (HSNo_proj0 Quaternion_k)) (mul_CSNo (HSNo_proj1 Quaternion_k) (conj_CSNo (HSNo_proj0 Quaternion_k))) = x1 leaving 2 subgoals.
The subproof is completed by applying HSNo_1.
Apply HSNo_p1_1 with λ x0 x1 . add_CSNo (mul_CSNo (HSNo_proj1 Quaternion_k) (HSNo_proj0 Quaternion_k)) (mul_CSNo (HSNo_proj1 Quaternion_k) (conj_CSNo (HSNo_proj0 Quaternion_k))) = minus_CSNo x1.
Apply minus_CSNo_0 with λ x0 x1 . add_CSNo (mul_CSNo (HSNo_proj1 Quaternion_k) (HSNo_proj0 Quaternion_k)) (mul_CSNo (HSNo_proj1 Quaternion_k) (conj_CSNo (HSNo_proj0 Quaternion_k))) = x1.
Apply HSNo_p0_k with λ x0 x1 . add_CSNo (mul_CSNo (HSNo_proj1 Quaternion_k) x1) (mul_CSNo (HSNo_proj1 Quaternion_k) (conj_CSNo x1)) = 0.
Apply HSNo_p1_k with λ x0 x1 . add_CSNo (mul_CSNo x1 0) (mul_CSNo x1 (conj_CSNo 0)) = 0.
Apply conj_CSNo_0 with λ x0 x1 . add_CSNo (mul_CSNo Complex_i 0) (mul_CSNo Complex_i x1) = 0.
Apply mul_CSNo_0R with Complex_i, λ x0 x1 . add_CSNo x1 x1 = 0 leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
Apply add_CSNo_0L with 0.
The subproof is completed by applying CSNo_0.
■