Metamath Proof Explorer

Theorem fldextfld1

Description: A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion fldextfld1 ⊢ E /FldExt F → E ∈ Field

Proof

Step Hyp Ref Expression
1 opabssxp ⊢ e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e ⊆ Field × Field
2 df-br ⊢ E /FldExt F ↔ E F ∈ /FldExt
3 2 biimpi ⊢ E /FldExt F → E F ∈ /FldExt
4 df-fldext ⊢ /FldExt = e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e
5 3 4 eleqtrdi ⊢ E /FldExt F → E F ∈ e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e
6 1 5 sselid ⊢ E /FldExt F → E F ∈ Field × Field
7 opelxp1 ⊢ E F ∈ Field × Field → E ∈ Field
8 6 7 syl ⊢ E /FldExt F → E ∈ Field