Theorem fldgenidfld

Description: The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
	fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
	fldgenidfld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝐹 ) )
Assertion	fldgenidfld	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3		fldgenidfld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝐹 ) )
4	1	sdrgss	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝐹 ) → 𝑆 ⊆ 𝐵 )
5	3 4	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6	1 2 5	fldgenval	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
7		intmin	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝐹 ) → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } = 𝑆 )
8	3 7	syl	⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } = 𝑆 )
9	6 8	eqtrd	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = 𝑆 )