Theorem fldgenval

Description: Value of the field generating function: ( F fldGen S ) is the smallest sub-division-ring of F containing S . (Contributed by Thierry Arnoux, 11-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
	fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
	fldgenval.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	fldgenval	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3		fldgenval.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4	2	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
5	1	fvexi	⊢ 𝐵 ∈ V
6	5	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
7	6 3	ssexd	⊢ ( 𝜑 → 𝑆 ∈ V )
8	1	sdrgid	⊢ ( 𝐹 ∈ DivRing → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
9	2 8	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
10		sseq2	⊢ ( 𝑎 = 𝐵 → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐵 ) → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
12	9 11 3	rspcedvd	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) 𝑆 ⊆ 𝑎 )
13		intexrab	⊢ ( ∃ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) 𝑆 ⊆ 𝑎 ↔ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ V )
14	12 13	sylib	⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ V )
15		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → 𝑓 = 𝐹 )
16	15	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → ( SubDRing ‘ 𝑓 ) = ( SubDRing ‘ 𝐹 ) )
17		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
18	17	sseq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → ( 𝑠 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝑎 ) )
19	16 18	rabeqbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } = { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
20	19	inteqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
21		df-fldgen	⊢ fldGen = ( 𝑓 ∈ V , 𝑠 ∈ V ↦ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } )
22	20 21	ovmpoga	⊢ ( ( 𝐹 ∈ V ∧ 𝑆 ∈ V ∧ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ V ) → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
23	4 7 14 22	syl3anc	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )