Let x0 of type ι be given.

Assume H0: x0 ∈ octonion.

Let x1 of type ι be given.

Assume H1: x1 ∈ octonion.

Apply octonion_p0_quaternion with x0.

The subproof is completed by applying H0.

Apply octonion_p1_quaternion with x0.

The subproof is completed by applying H0.

Apply octonion_p0_quaternion with x1.

The subproof is completed by applying H1.

Apply octonion_p1_quaternion with x1.

The subproof is completed by applying H1.

Apply quaternion_add_HSNo with mul_HSNo (OSNo_proj0 x0) (OSNo_proj0 x1), minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 x1)) (OSNo_proj1 x0)) leaving 2 subgoals.

Apply quaternion_mul_HSNo with OSNo_proj0 x0, OSNo_proj0 x1 leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L4.

Apply quaternion_minus_HSNo with mul_HSNo (conj_HSNo (OSNo_proj1 x1)) (OSNo_proj1 x0).

Apply quaternion_mul_HSNo with conj_HSNo (OSNo_proj1 x1), OSNo_proj1 x0 leaving 2 subgoals.

Apply quaternion_conj_HSNo with OSNo_proj1 x1.

The subproof is completed by applying L5.

The subproof is completed by applying L3.

Apply quaternion_add_HSNo with mul_HSNo (OSNo_proj1 x1) (OSNo_proj0 x0), mul_HSNo (OSNo_proj1 x0) (conj_HSNo (OSNo_proj0 x1)) leaving 2 subgoals.

Apply quaternion_mul_HSNo with OSNo_proj1 x1, OSNo_proj0 x0 leaving 2 subgoals.

The subproof is completed by applying L5.

The subproof is completed by applying L2.

Apply quaternion_mul_HSNo with OSNo_proj1 x0, conj_HSNo (OSNo_proj0 x1) leaving 2 subgoals.

The subproof is completed by applying L3.

Apply quaternion_conj_HSNo with OSNo_proj0 x1.

The subproof is completed by applying L4.

■

Proofgold Proof