Theorem fldgenfld

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

	Ref	Expression
Hypotheses	fldgenfld.1	$$⊢B={\mathrm{Base}}_F$$
	fldgenfld.2	$$⊢\phi \to F\in \mathrm{Field}$$
	fldgenfld.3	$$⊢\phi \to S\subseteq B$$
Assertion	fldgenfld	Could not format assertion : No typesetting found for |- ( ph -> ( F |`s ( F fldGen S ) ) e. Field ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fldgenfld.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenfld.2	$$⊢\phi \to F\in \mathrm{Field}$$
3		fldgenfld.3	$$⊢\phi \to S\subseteq B$$
4		isfld	$$⊢F\in \mathrm{Field}\leftrightarrow \left(F\in \mathrm{DivRing}\wedge F\in \mathrm{CRing}\right)$$
5	2 4	sylib	$$⊢\phi \to \left(F\in \mathrm{DivRing}\wedge F\in \mathrm{CRing}\right)$$
6	5	simpld	$$⊢\phi \to F\in \mathrm{DivRing}$$
7	1 6 3	fldgensdrg	Could not format ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) ) : No typesetting found for |- ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) ) with typecode |-
8		fldsdrgfld	Could not format ( ( F e. Field /\ ( F fldGen S ) e. ( SubDRing ` F ) ) -> ( F |`s ( F fldGen S ) ) e. Field ) : No typesetting found for |- ( ( F e. Field /\ ( F fldGen S ) e. ( SubDRing ` F ) ) -> ( F |`s ( F fldGen S ) ) e. Field ) with typecode |-
9	2 7 8	syl2anc	Could not format ( ph -> ( F |`s ( F fldGen S ) ) e. Field ) : No typesetting found for |- ( ph -> ( F |`s ( F fldGen S ) ) e. Field ) with typecode |-