This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )