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/FldExtF→E∈Field

Proof

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