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	$$⊢\phi \to F{\upharpoonright }_{𝑠}\left(F\mathrm{fldGen}S\right)\in \mathrm{Field}$$

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	$$⊢\phi \to F\mathrm{fldGen}S\in \mathrm{SubDRing}\left(F\right)$$
8		fldsdrgfld	$$⊢\left(F\in \mathrm{Field}\wedge F\mathrm{fldGen}S\in \mathrm{SubDRing}\left(F\right)\right)\to F{\upharpoonright }_{𝑠}\left(F\mathrm{fldGen}S\right)\in \mathrm{Field}$$
9	2 7 8	syl2anc	$$⊢\phi \to F{\upharpoonright }_{𝑠}\left(F\mathrm{fldGen}S\right)\in \mathrm{Field}$$