Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: subfield x0 x1.

Assume H1: subfield x1 x2.

Apply subfield_E with x0, x1, subfield x0 x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H2: Field x0.

Assume H3: Field x1.

Assume H4: field0 x0 ⊆ field0 x1.

Assume H5: field3 x0 = field3 x1.

Assume H6: field4 x0 = field4 x1.

Assume H7: ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field1b x0 x3 x4 = field1b x1 x3 x4.

Assume H8: ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field2b x0 x3 x4 = field2b x1 x3 x4.

Apply subfield_E with x1, x2, subfield x0 x2 leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H9: Field x1.

Assume H10: Field x2.

Assume H11: field0 x1 ⊆ field0 x2.

Assume H12: field3 x1 = field3 x2.

Assume H13: field4 x1 = field4 x2.

Assume H14: ∀ x3 . x3 ∈ field0 x1 ⟶ ∀ x4 . x4 ∈ field0 x1 ⟶ field1b x1 x3 x4 = field1b x2 x3 x4.

Assume H15: ∀ x3 . x3 ∈ field0 x1 ⟶ ∀ x4 . x4 ∈ field0 x1 ⟶ field2b x1 x3 x4 = field2b x2 x3 x4.

Apply subfield_I with x0, x2 leaving 7 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H10.

Apply Subq_tra with field0 x0, field0 x1, field0 x2 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H11.

Apply H12 with λ x3 x4 . field3 x0 = x3.

The subproof is completed by applying H5.

Apply H13 with λ x3 x4 . field4 x0 = x3.

The subproof is completed by applying H6.

Let x3 of type ι be given.

Assume H16: x3 ∈ field0 x0.

Let x4 of type ι be given.

Assume H17: x4 ∈ field0 x0.

Claim L18: x3 ∈ field0 x1

Apply H4 with x3.

The subproof is completed by applying H16.

Claim L19: x4 ∈ field0 x1

Apply H4 with x4.

The subproof is completed by applying H17.

Apply H14 with x3, x4, λ x5 x6 . field1b x0 x3 x4 = x5 leaving 3 subgoals.

The subproof is completed by applying L18.

The subproof is completed by applying L19.

Apply H7 with x3, x4 leaving 2 subgoals.

The subproof is completed by applying H16.

The subproof is completed by applying H17.

Let x3 of type ι be given.

Assume H16: x3 ∈ field0 x0.

Let x4 of type ι be given.

Assume H17: x4 ∈ field0 x0.

Claim L18: x3 ∈ field0 x1

Apply H4 with x3.

The subproof is completed by applying H16.

Claim L19: x4 ∈ field0 x1

Apply H4 with x4.

The subproof is completed by applying H17.

Apply H15 with x3, x4, λ x5 x6 . field2b x0 x3 x4 = x5 leaving 3 subgoals.

The subproof is completed by applying L18.

The subproof is completed by applying L19.

Apply H8 with x3, x4 leaving 2 subgoals.

The subproof is completed by applying H16.

The subproof is completed by applying H17.

■

Proofgold Proof