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 )