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

Metamath Proof Explorer

Theorem fldsdrgfldext

Description: A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses fldsdrgfldext.1 
|- G = ( F |`s A )
fldsdrgfldext.2 
|- ( ph -> F e. Field )
fldsdrgfldext.3 
|- ( ph -> A e. ( SubDRing ` F ) )
Assertion fldsdrgfldext 
|- ( ph -> F /FldExt G )

Proof

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