Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply CSNo_ReIm_split with
mul_CSNo x0 (mul_CSNo x1 x2),
mul_CSNo (mul_CSNo x0 x1) x2 leaving 4 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
set y3 to be ...
set y4 to be ...
Claim L13: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Apply mul_CSNo_CRe with
x2,
mul_CSNo y3 y4,
λ x6 . x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y6 to be ...
set y7 to be ...
set y8 to be ...
Apply L14 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H15: y8 y7 y7.
The subproof is completed by applying H15.
Apply add_SNo_rotate_4_0312 with
mul_SNo (CSNo_Re x5) (mul_SNo (CSNo_Re y6) (CSNo_Re y7)),
minus_SNo (mul_SNo (CSNo_Re x5) (mul_SNo (CSNo_Im y7) (CSNo_Im y6))),
minus_SNo (mul_SNo (CSNo_Im y7) (mul_SNo (CSNo_Re y6) (CSNo_Im x5))),
minus_SNo (mul_SNo (CSNo_Im y6) (mul_SNo (CSNo_Re y7) (CSNo_Im x5))),
λ x9 . y8 leaving 5 subgoals.
Apply SNo_mul_SNo_3 with
CSNo_Re x5,
CSNo_Re y6,
CSNo_Re y7 leaving 3 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Re x5) (mul_SNo (CSNo_Im y7) (CSNo_Im y6)).
Apply SNo_mul_SNo_3 with
CSNo_Re x5,
CSNo_Im y7,
CSNo_Im y6 leaving 3 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H13.
The subproof is completed by applying L12.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Im y7) (mul_SNo (CSNo_Re y6) (CSNo_Im x5)).
Apply SNo_mul_SNo_3 with
CSNo_Im y7,
CSNo_Re y6,
CSNo_Im x5 leaving 3 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying L9.
The subproof is completed by applying L11.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Im y6) (mul_SNo (CSNo_Re y7) (CSNo_Im x5)).
Apply SNo_mul_SNo_3 with
CSNo_Im y6,
CSNo_Re y7,
CSNo_Im x5 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
set y9 to be ...
set y10 to be ...
Claim L15: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
set y12 to be ...
set y13 to be ...
set y14 to be ...
set y15 to be ...
Apply L16 with
λ x16 . y15 x16 y14 ⟶ y15 y14 x16 leaving 2 subgoals.
Assume H17: y15 y14 y14.
The subproof is completed by applying H17.
set y16 to be ...
set y17 to be ...
set y18 to be ...
Claim L17: ∀ x19 : ι → ο . x19 y18 ⟶ x19 y17
Let x19 of type ι → ο be given.
Apply L17 with
λ x20 . y19 x20 y18 ⟶ y19 y18 x20 leaving 2 subgoals.
Assume H18: y19 y18 y18.
The subproof is completed by applying H18.
The subproof is completed by applying L17.
set y11 to be λ x11 . y10
Apply L15 with
λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Assume H16: y11 y10 y10.
The subproof is completed by applying H16.
set y12 to be λ x12 . y11
Apply mul_CSNo_CRe with
mul_CSNo y8 y9,
y10,
λ x13 x14 . y12 x14 x13 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L4.
The subproof is completed by applying L15.
Let x5 of type ι → ι → ο be given.
Apply L13 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H14: x5 y4 y4.
The subproof is completed by applying H14.