Let x0 of type ι be given.

Assume H0: x0 ∈ quaternion.

Let x1 of type ι be given.

Assume H1: x1 ∈ quaternion.

Claim L2: HSNo_proj0 x0 ∈ complex

Apply quaternion_p0_complex with x0.

The subproof is completed by applying H0.

Claim L3: HSNo_proj1 x0 ∈ complex

Apply quaternion_p1_complex with x0.

The subproof is completed by applying H0.

Claim L4: HSNo_proj0 x1 ∈ complex

Apply quaternion_p0_complex with x1.

The subproof is completed by applying H1.

Claim L5: HSNo_proj1 x1 ∈ complex

Apply quaternion_p1_complex with x1.

The subproof is completed by applying H1.

Apply complex_add_CSNo with mul_CSNo (HSNo_proj0 x0) (HSNo_proj0 x1), minus_CSNo (mul_CSNo (conj_CSNo (HSNo_proj1 x1)) (HSNo_proj1 x0)) leaving 2 subgoals.

Apply complex_mul_CSNo with HSNo_proj0 x0, HSNo_proj0 x1 leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L4.

Apply complex_minus_CSNo with mul_CSNo (conj_CSNo (HSNo_proj1 x1)) (HSNo_proj1 x0).

Apply complex_mul_CSNo with conj_CSNo (HSNo_proj1 x1), HSNo_proj1 x0 leaving 2 subgoals.

Apply complex_conj_CSNo with HSNo_proj1 x1.

The subproof is completed by applying L5.

The subproof is completed by applying L3.

Apply complex_add_CSNo with mul_CSNo (HSNo_proj1 x1) (HSNo_proj0 x0), mul_CSNo (HSNo_proj1 x0) (conj_CSNo (HSNo_proj0 x1)) leaving 2 subgoals.

Apply complex_mul_CSNo with HSNo_proj1 x1, HSNo_proj0 x0 leaving 2 subgoals.

The subproof is completed by applying L5.

The subproof is completed by applying L2.

Apply complex_mul_CSNo with HSNo_proj1 x0, conj_CSNo (HSNo_proj0 x1) leaving 2 subgoals.

The subproof is completed by applying L3.

Apply complex_conj_CSNo with HSNo_proj0 x1.

The subproof is completed by applying L4.

■

Proofgold Proof