Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply setminusE with
field0 x0,
Sing (field3 x0),
x2,
and (Field_div x0 x1 x2 ∈ field0 x0) (x1 = field2b x0 x2 (Field_div x0 x1 x2)) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply Field_mult_inv_L with
x0,
x2,
∃ x3 . and (x3 ∈ field0 x0) (x1 = field2b x0 x2 x3) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Let x3 of type ι be given.
Apply H7 with
∃ x4 . and (x4 ∈ field0 x0) (x1 = field2b x0 x2 x4).
Let x4 of type ο be given.
Apply H10 with
field2b x0 x3 x1.
Apply andI with
field2b x0 x3 x1 ∈ field0 x0,
x1 = field2b x0 x2 (field2b x0 x3 x1) leaving 2 subgoals.
Apply Field_mult_clos with
x0,
x3,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H8.
The subproof is completed by applying H1.
Let x5 of type ι → ι → ο be given.
set y6 to be ...
set y7 to be ...
Claim L11: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
Assume H11: x8 x3.
Apply Field_mult_assoc with
x2,
x4,
x5,
x3,
λ x9 . x8 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H8.
The subproof is completed by applying H1.
set y9 to be ...
set y10 to be ...
Claim L12: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
set y11 to be λ x11 . y10
Apply L12 with
λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Assume H13: y11 y10 y10.
The subproof is completed by applying H13.
Apply Field_one_L with
x5,
y6,
λ x12 . y11 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying L12.
set y8 to be λ x8 x9 . y7 x9 x8
Apply L11 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9.
Assume H12: y8 y7 y7.
The subproof is completed by applying H12.