Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: OSNo Quaternion_j
The subproof is completed by applying OSNo_Quaternion_j.
Claim L1: OSNo Quaternion_k
The subproof is completed by applying OSNo_Quaternion_k.
Claim L2: OSNo Complex_i
The subproof is completed by applying OSNo_Complex_i.
Claim L3: OSNo (mul_OSNo Quaternion_k Quaternion_j)
Apply OSNo_mul_OSNo with Quaternion_k, Quaternion_j leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L0.
Apply OSNo_proj0proj1_split with mul_OSNo Quaternion_k Quaternion_j, minus_OSNo Complex_i leaving 4 subgoals.
The subproof is completed by applying L3.
Apply OSNo_minus_OSNo with Complex_i.
The subproof is completed by applying L2.
Apply minus_OSNo_proj0 with Complex_i, λ x0 x1 . OSNo_proj0 (mul_OSNo Quaternion_k Quaternion_j) = x1 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply OSNo_p0_i with λ x0 x1 . OSNo_proj0 (mul_OSNo Quaternion_k Quaternion_j) = minus_HSNo x1.
Apply mul_OSNo_proj0 with Quaternion_k, Quaternion_j, λ x0 x1 . x1 = minus_HSNo Complex_i leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L0.
Apply OSNo_p0_j with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj0 Quaternion_k) x1) (minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 Quaternion_j)) (OSNo_proj1 Quaternion_k))) = minus_HSNo Complex_i.
Apply OSNo_p1_j with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj0 Quaternion_k) Quaternion_j) (minus_HSNo (mul_HSNo (conj_HSNo x1) (OSNo_proj1 Quaternion_k))) = minus_HSNo Complex_i.
Apply OSNo_p0_k with λ x0 x1 . add_HSNo (mul_HSNo x1 Quaternion_j) (minus_HSNo (mul_HSNo (conj_HSNo 0) (OSNo_proj1 Quaternion_k))) = minus_HSNo Complex_i.
Apply OSNo_p1_k with λ x0 x1 . add_HSNo (mul_HSNo Quaternion_k Quaternion_j) (minus_HSNo (mul_HSNo (conj_HSNo 0) x1)) = minus_HSNo Complex_i.
Apply conj_HSNo_id_SNo with 0, λ x0 x1 . add_HSNo (mul_HSNo Quaternion_k Quaternion_j) (minus_HSNo (mul_HSNo x1 0)) = minus_HSNo Complex_i leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply mul_HSNo_0R with 0, λ x0 x1 . add_HSNo (mul_HSNo Quaternion_k Quaternion_j) (minus_HSNo x1) = minus_HSNo Complex_i leaving 2 subgoals.
The subproof is completed by applying HSNo_0.
Apply minus_HSNo_0 with λ x0 x1 . add_HSNo (mul_HSNo Quaternion_k Quaternion_j) x1 = minus_HSNo Complex_i.
Apply add_HSNo_0R with mul_HSNo Quaternion_k Quaternion_j, λ x0 x1 . x1 = minus_HSNo Complex_i leaving 2 subgoals.
Apply HSNo_mul_HSNo with Quaternion_k, Quaternion_j leaving 2 subgoals.
The subproof is completed by applying HSNo_Quaternion_k.
The subproof is completed by applying HSNo_Quaternion_j.
The subproof is completed by applying Quaternion_k_j.
Apply minus_OSNo_proj1 with Complex_i, λ x0 x1 . OSNo_proj1 (mul_OSNo Quaternion_k Quaternion_j) = x1 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply OSNo_p1_i with λ x0 x1 . OSNo_proj1 (mul_OSNo Quaternion_k Quaternion_j) = minus_HSNo x1.
Apply mul_OSNo_proj1 with Quaternion_k, Quaternion_j, λ x0 x1 . x1 = minus_HSNo 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L0.
Apply OSNo_p0_j with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj1 Quaternion_j) (OSNo_proj0 Quaternion_k)) (mul_HSNo (OSNo_proj1 Quaternion_k) (conj_HSNo x1)) = minus_HSNo 0.
Apply OSNo_p1_j with λ x0 x1 . add_HSNo (mul_HSNo x1 (OSNo_proj0 Quaternion_k)) (mul_HSNo (OSNo_proj1 Quaternion_k) (conj_HSNo Quaternion_j)) = minus_HSNo 0.
Apply OSNo_p0_k with λ x0 x1 . add_HSNo (mul_HSNo 0 x1) (mul_HSNo (OSNo_proj1 Quaternion_k) (conj_HSNo Quaternion_j)) = minus_HSNo 0.
Apply OSNo_p1_k with λ x0 x1 . add_HSNo (mul_HSNo 0 Quaternion_k) (mul_HSNo x1 (conj_HSNo Quaternion_j)) = minus_HSNo 0.
Apply mul_HSNo_0L with conj_HSNo Quaternion_j, λ x0 x1 . add_HSNo (mul_HSNo 0 Quaternion_k) x1 = minus_HSNo 0 leaving 2 subgoals.
Apply HSNo_conj_HSNo with Quaternion_j.
The subproof is completed by applying HSNo_Quaternion_j.
Apply mul_HSNo_0L with Quaternion_k, λ x0 x1 . add_HSNo x1 0 = minus_HSNo 0 leaving 2 subgoals.
The subproof is completed by applying HSNo_Quaternion_k.
Apply minus_HSNo_0 with λ x0 x1 . add_HSNo 0 0 = x1.
Apply add_HSNo_0L with 0.
The subproof is completed by applying HSNo_0.
■