Theorem fldgenssp

Description: The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3		fldgenidfld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝐹 ) )
4		fldgenssp.t	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
5		issdrg	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝐹 ) ↔ ( 𝐹 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝑆 ) ∈ DivRing ) )
6	3 5	sylib	⊢ ( 𝜑 → ( 𝐹 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝑆 ) ∈ DivRing ) )
7	6	simp2d	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝐹 ) )
8	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐹 ) → 𝑆 ⊆ 𝐵 )
9	7 8	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10	4 9	sstrd	⊢ ( 𝜑 → 𝑇 ⊆ 𝐵 )
11	1 2 10	fldgenval	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑇 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } )
12		sseq2	⊢ ( 𝑎 = 𝑆 → ( 𝑇 ⊆ 𝑎 ↔ 𝑇 ⊆ 𝑆 ) )
13	12 3 4	elrabd	⊢ ( 𝜑 → 𝑆 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } )
14		intss1	⊢ ( 𝑆 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } ⊆ 𝑆 )
15	13 14	syl	⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } ⊆ 𝑆 )
16	11 15	eqsstrd	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑇 ) ⊆ 𝑆 )