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 e. Field )

Proof

Step Hyp Ref Expression
1 opabssxp
 |-  { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } C_ ( Field X. Field )
2 df-br
 |-  ( E /FldExt F <-> <. E , F >. e. /FldExt )
3 2 biimpi
 |-  ( E /FldExt F -> <. E , F >. e. /FldExt )
4 df-fldext
 |-  /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }
5 3 4 eleqtrdi
 |-  ( E /FldExt F -> <. E , F >. e. { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } )
6 1 5 sselid
 |-  ( E /FldExt F -> <. E , F >. e. ( Field X. Field ) )
7 opelxp1
 |-  ( <. E , F >. e. ( Field X. Field ) -> E e. Field )
8 6 7 syl
 |-  ( E /FldExt F -> E e. Field )