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

Metamath Proof Explorer

Theorem sdrgfldext

Description: A field E and any sub-division-ring F of E form a field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses sdrgfldext.b 
|- B = ( Base ` E )
sdrgfldext.e 
|- ( ph -> E e. Field )
sdrgfldext.f 
|- ( ph -> F e. ( SubDRing ` E ) )
Assertion sdrgfldext 
|- ( ph -> E /FldExt ( E |`s F ) )

Proof

Step Hyp Ref Expression
1 sdrgfldext.b 
 |-  B = ( Base ` E )
2 sdrgfldext.e 
 |-  ( ph -> E e. Field )
3 sdrgfldext.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
4 fldsdrgfld 
 |-  ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
5 2 3 4 syl2anc 
 |-  ( ph -> ( E |`s F ) e. Field )
6 1 sdrgss 
 |-  ( F e. ( SubDRing ` E ) -> F C_ B )
7 3 6 syl 
 |-  ( ph -> F C_ B )
8 eqid 
 |-  ( E |`s F ) = ( E |`s F )
9 8 1 ressbas2 
 |-  ( F C_ B -> F = ( Base ` ( E |`s F ) ) )
10 7 9 syl 
 |-  ( ph -> F = ( Base ` ( E |`s F ) ) )
11 10 oveq2d 
 |-  ( ph -> ( E |`s F ) = ( E |`s ( Base ` ( E |`s F ) ) ) )
12 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
13 3 12 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
14 10 13 eqeltrrd 
 |-  ( ph -> ( Base ` ( E |`s F ) ) e. ( SubRing ` E ) )
15 brfldext 
 |-  ( ( E e. Field /\ ( E |`s F ) e. Field ) -> ( E /FldExt ( E |`s F ) <-> ( ( E |`s F ) = ( E |`s ( Base ` ( E |`s F ) ) ) /\ ( Base ` ( E |`s F ) ) e. ( SubRing ` E ) ) ) )
16 15 biimpar 
 |-  ( ( ( E e. Field /\ ( E |`s F ) e. Field ) /\ ( ( E |`s F ) = ( E |`s ( Base ` ( E |`s F ) ) ) /\ ( Base ` ( E |`s F ) ) e. ( SubRing ` E ) ) ) -> E /FldExt ( E |`s F ) )
17 2 5 11 14 16 syl22anc 
 |-  ( ph -> E /FldExt ( E |`s F ) )