Theorem fldgenfld

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

	Ref	Expression
Hypotheses	fldgenfld.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
	fldgenfld.2	⊢ ( 𝜑 → 𝐹 ∈ Field )
	fldgenfld.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	fldgenfld	⊢ ( 𝜑 → ( 𝐹 ↾s ( 𝐹 fldGen 𝑆 ) ) ∈ Field )

Proof

Step	Hyp	Ref	Expression
1		fldgenfld.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenfld.2	⊢ ( 𝜑 → 𝐹 ∈ Field )
3		fldgenfld.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4		isfld	⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
5	2 4	sylib	⊢ ( 𝜑 → ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
6	5	simpld	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
7	1 6 3	fldgensdrg	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) ∈ ( SubDRing ‘ 𝐹 ) )
8		fldsdrgfld	⊢ ( ( 𝐹 ∈ Field ∧ ( 𝐹 fldGen 𝑆 ) ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s ( 𝐹 fldGen 𝑆 ) ) ∈ Field )
9	2 7 8	syl2anc	⊢ ( 𝜑 → ( 𝐹 ↾s ( 𝐹 fldGen 𝑆 ) ) ∈ Field )