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 ) )