Metamath Proof Explorer

Theorem fldextsdrg

Description: Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses fldextsdrg.1 
|- B = ( Base ` F )
fldextsdrg.2 
|- ( ph -> E /FldExt F )
Assertion fldextsdrg 
|- ( ph -> B e. ( SubDRing ` E ) )

Proof

Step Hyp Ref Expression
1 fldextsdrg.1 
 |-  B = ( Base ` F )
2 fldextsdrg.2 
 |-  ( ph -> E /FldExt F )
3 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
4 2 3 syl 
 |-  ( ph -> E e. Field )
5 4 flddrngd 
 |-  ( ph -> E e. DivRing )
6 1 fldextsubrg 
 |-  ( E /FldExt F -> B e. ( SubRing ` E ) )
7 2 6 syl 
 |-  ( ph -> B e. ( SubRing ` E ) )
8 fldextress 
 |-  ( E /FldExt F -> F = ( E |`s ( Base ` F ) ) )
9 2 8 syl 
 |-  ( ph -> F = ( E |`s ( Base ` F ) ) )
10 1 oveq2i 
 |-  ( E |`s B ) = ( E |`s ( Base ` F ) )
11 9 10 eqtr4di 
 |-  ( ph -> F = ( E |`s B ) )
12 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
13 2 12 syl 
 |-  ( ph -> F e. Field )
14 11 13 eqeltrrd 
 |-  ( ph -> ( E |`s B ) e. Field )
15 14 flddrngd 
 |-  ( ph -> ( E |`s B ) e. DivRing )
16 issdrg 
 |-  ( B e. ( SubDRing ` E ) <-> ( E e. DivRing /\ B e. ( SubRing ` E ) /\ ( E |`s B ) e. DivRing ) )
17 5 7 15 16 syl3anbrc 
 |-  ( ph -> B e. ( SubDRing ` E ) )