Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: subfield x0 x1.

Apply subfield_E with x0, x1, Group (Galois_Group x1 x0) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: Field x0.

Assume H2: Field x1.

Assume H3: ap x0 0 ⊆ ap x1 0.

Assume H4: field3 x0 = field3 x1.

Assume H5: field4 x0 = field4 x1.

Assume H6: ∀ x2 . x2 ∈ ap x0 0 ⟶ ∀ x3 . x3 ∈ ap x0 0 ⟶ field1b x0 x2 x3 = field1b x1 x2 x3.

Assume H7: ∀ x2 . x2 ∈ ap x0 0 ⟶ ∀ x3 . x3 ∈ ap x0 0 ⟶ field2b x0 x2 x3 = field2b x1 x2 x3.

Apply GroupI with {x2 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x2}, λ x2 x3 . lam (ap x1 0) (λ x4 . ap x2 (ap x3 x4)).

Claim L8: ...

...

Apply and3I with ∀ x2 . x2 ∈ {x3 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x3} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x4} ⟶ lam_comp (ap x1 0) x2 x3 ∈ {x4 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x4}, ∀ x2 . x2 ∈ {x3 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x3} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x4} ⟶ ∀ x4 . x4 ∈ {x5 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x5} ⟶ lam_comp (ap x1 0) x2 (lam_comp (ap x1 0) x3 x4) = lam_comp (ap x1 0) (lam_comp (ap x1 0) x2 x3) x4, ∃ x2 . and (x2 ∈ {x3 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x3}) (and (∀ x3 . x3 ∈ {x4 ∈ setexp (ap x1 0) (ap x1 0)|Field_automorphism_fixing x1 x0 x4} ⟶ and (lam_comp (ap x1 0) x2 x3 = x3) (lam_comp (ap x1 0) x3 x2 = x3)) (∀ x3 . ...)) leaving 3 subgoals.

...

■

Proofgold Proof