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

Metamath Proof Explorer

Theorem fldgenfld

Description: A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Hypotheses fldgenfld.1 
|- B = ( Base ` F )
fldgenfld.2 
|- ( ph -> F e. Field )
fldgenfld.3 
|- ( ph -> S C_ B )
Assertion fldgenfld 
|- ( ph -> ( F |`s ( F fldGen S ) ) e. Field )

Proof

Step Hyp Ref Expression
1 fldgenfld.1 
 |-  B = ( Base ` F )
2 fldgenfld.2 
 |-  ( ph -> F e. Field )
3 fldgenfld.3 
 |-  ( ph -> S C_ B )
4 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
5 2 4 sylib 
 |-  ( ph -> ( F e. DivRing /\ F e. CRing ) )
6 5 simpld 
 |-  ( ph -> F e. DivRing )
7 1 6 3 fldgensdrg 
 |-  ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) )
8 fldsdrgfld 
 |-  ( ( F e. Field /\ ( F fldGen S ) e. ( SubDRing ` F ) ) -> ( F |`s ( F fldGen S ) ) e. Field )
9 2 7 8 syl2anc 
 |-  ( ph -> ( F |`s ( F fldGen S ) ) e. Field )