Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: OSNo ...
...
Claim L1: OSNo Octonion_i6
The subproof is completed by applying OSNo_Octonion_i6.
Claim L2: OSNo Complex_i
The subproof is completed by applying OSNo_Complex_i.
Claim L3: OSNo (mul_OSNo Octonion_i5 Octonion_i6)
Apply OSNo_mul_OSNo with Octonion_i5, Octonion_i6 leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply OSNo_proj0proj1_split with mul_OSNo Octonion_i5 Octonion_i6, Complex_i leaving 4 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L2.
Apply OSNo_p0_i with λ x0 x1 . OSNo_proj0 (mul_OSNo Octonion_i5 Octonion_i6) = x1.
Apply mul_OSNo_proj0 with Octonion_i5, Octonion_i6, λ x0 x1 . x1 = Complex_i leaving 3 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply OSNo_p0_i5 with λ x0 x1 . add_HSNo (mul_HSNo x1 (OSNo_proj0 Octonion_i6)) (minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 Octonion_i6)) (OSNo_proj1 Octonion_i5))) = Complex_i.
Apply OSNo_p1_i5 with λ x0 x1 . add_HSNo (mul_HSNo 0 (OSNo_proj0 Octonion_i6)) (minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 Octonion_i6)) x1)) = Complex_i.
Apply OSNo_p0_i6 with λ x0 x1 . add_HSNo (mul_HSNo 0 x1) (minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 Octonion_i6)) (minus_HSNo Quaternion_k))) = Complex_i.
Apply OSNo_p1_i6 with λ x0 x1 . add_HSNo (mul_HSNo 0 0) (minus_HSNo (mul_HSNo (conj_HSNo x1) (minus_HSNo Quaternion_k))) = Complex_i.
Apply mul_HSNo_0L with 0, λ x0 x1 . add_HSNo x1 (minus_HSNo (mul_HSNo (conj_HSNo (minus_HSNo Quaternion_j)) (minus_HSNo Quaternion_k))) = Complex_i leaving 2 subgoals.
The subproof is completed by applying HSNo_0.
Apply conj_minus_HSNo with Quaternion_j, λ x0 x1 . add_HSNo 0 (minus_HSNo (mul_HSNo x1 (minus_HSNo Quaternion_k))) = Complex_i leaving 2 subgoals.
The subproof is completed by applying HSNo_Quaternion_j.
Apply conj_HSNo_j with λ x0 x1 . add_HSNo 0 (minus_HSNo (mul_HSNo (minus_HSNo x1) (minus_HSNo Quaternion_k))) = Complex_i.
Apply minus_HSNo_invol with Quaternion_j, λ x0 x1 . add_HSNo 0 (minus_HSNo (mul_HSNo x1 (minus_HSNo Quaternion_k))) = Complex_i leaving 2 subgoals.
The subproof is completed by applying HSNo_Quaternion_j.
Apply minus_mul_HSNo_distrR with Quaternion_j, Quaternion_k, λ x0 x1 . add_HSNo 0 (minus_HSNo x1) = Complex_i leaving 3 subgoals.
The subproof is completed by applying HSNo_Quaternion_j.
The subproof is completed by applying HSNo_Quaternion_k.
Apply Quaternion_j_k with λ x0 x1 . add_HSNo 0 (minus_HSNo (minus_HSNo x1)) = Complex_i.
Apply minus_HSNo_invol with Complex_i, λ x0 x1 . add_HSNo 0 x1 = Complex_i leaving 2 subgoals.
The subproof is completed by applying HSNo_Complex_i.
Apply add_HSNo_0L with Complex_i.
The subproof is completed by applying HSNo_Complex_i.
Apply OSNo_p1_i with λ x0 x1 . OSNo_proj1 (mul_OSNo Octonion_i5 Octonion_i6) = x1.
Apply mul_OSNo_proj1 with Octonion_i5, Octonion_i6, λ x0 x1 . x1 = 0 leaving 3 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply OSNo_p0_i5 with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj1 Octonion_i6) x1) (mul_HSNo (OSNo_proj1 Octonion_i5) (conj_HSNo (OSNo_proj0 Octonion_i6))) = 0.
Apply OSNo_p1_i5 with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj1 Octonion_i6) 0) (mul_HSNo x1 (conj_HSNo (OSNo_proj0 Octonion_i6))) = 0.
Apply OSNo_p0_i6 with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj1 Octonion_i6) 0) (mul_HSNo (minus_HSNo Quaternion_k) (conj_HSNo x1)) = 0.
Apply OSNo_p1_i6 with λ x0 x1 . add_HSNo (mul_HSNo x1 0) (mul_HSNo (minus_HSNo Quaternion_k) (conj_HSNo 0)) = 0.
Apply conj_HSNo_id_SNo with 0, λ x0 x1 . add_HSNo (mul_HSNo (minus_HSNo Quaternion_j) 0) (mul_HSNo (minus_HSNo Quaternion_k) x1) = 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply mul_HSNo_0R with minus_HSNo Quaternion_k, λ x0 x1 . add_HSNo (mul_HSNo (minus_HSNo Quaternion_j) 0) x1 = 0 leaving 2 subgoals.
Apply HSNo_minus_HSNo with Quaternion_k.
The subproof is completed by applying HSNo_Quaternion_k.
Apply mul_HSNo_0R with minus_HSNo Quaternion_j, λ x0 x1 . add_HSNo x1 0 = 0 leaving 2 subgoals.
Apply HSNo_minus_HSNo with Quaternion_j.
The subproof is completed by applying HSNo_Quaternion_j.
Apply add_HSNo_0L with 0.
The subproof is completed by applying HSNo_0.
■