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

Metamath Proof Explorer

Theorem fldextsubrg

Description: Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Hypothesis fldextsubrg.1 
|- U = ( Base ` F )
Assertion fldextsubrg 
|- ( E /FldExt F -> U e. ( SubRing ` E ) )

Proof

Step Hyp Ref Expression
1 fldextsubrg.1 
 |-  U = ( Base ` F )
2 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
3 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
4 brfldext 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
5 2 3 4 syl2anc 
 |-  ( E /FldExt F -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
6 5 ibi 
 |-  ( E /FldExt F -> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) )
7 6 simprd 
 |-  ( E /FldExt F -> ( Base ` F ) e. ( SubRing ` E ) )
8 1 7 eqeltrid 
 |-  ( E /FldExt F -> U e. ( SubRing ` E ) )