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	|- B = ( Base ` F )
	fldgenval.2	|- ( ph -> F e. DivRing )
	fldgenval.3	|- ( ph -> S C_ B )
Assertion	fldgenval	|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	|- B = ( Base ` F )
2		fldgenval.2	|- ( ph -> F e. DivRing )
3		fldgenval.3	|- ( ph -> S C_ B )
4	2	elexd	|- ( ph -> F e. _V )
5	1	fvexi	|- B e. _V
6	5	a1i	|- ( ph -> B e. _V )
7	6 3	ssexd	|- ( ph -> S e. _V )
8	1	sdrgid	|- ( F e. DivRing -> B e. ( SubDRing ` F ) )
9	2 8	syl	|- ( ph -> B e. ( SubDRing ` F ) )
10		sseq2	|- ( a = B -> ( S C_ a <-> S C_ B ) )
11	10	adantl	|- ( ( ph /\ a = B ) -> ( S C_ a <-> S C_ B ) )
12	9 11 3	rspcedvd	|- ( ph -> E. a e. ( SubDRing ` F ) S C_ a )
13		intexrab	|- ( E. a e. ( SubDRing ` F ) S C_ a <-> |^| { a e. ( SubDRing ` F ) | S C_ a } e. _V )
14	12 13	sylib	|- ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } e. _V )
15		simpl	|- ( ( f = F /\ s = S ) -> f = F )
16	15	fveq2d	|- ( ( f = F /\ s = S ) -> ( SubDRing ` f ) = ( SubDRing ` F ) )
17		simpr	|- ( ( f = F /\ s = S ) -> s = S )
18	17	sseq1d	|- ( ( f = F /\ s = S ) -> ( s C_ a <-> S C_ a ) )
19	16 18	rabeqbidv	|- ( ( f = F /\ s = S ) -> { a e. ( SubDRing ` f ) | s C_ a } = { a e. ( SubDRing ` F ) | S C_ a } )
20	19	inteqd	|- ( ( f = F /\ s = S ) -> |^| { a e. ( SubDRing ` f ) | s C_ a } = |^| { a e. ( SubDRing ` F ) | S C_ a } )
21		df-fldgen	|- fldGen = ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } )
22	20 21	ovmpoga	|- ( ( F e. _V /\ S e. _V /\ |^| { a e. ( SubDRing ` F ) | S C_ a } e. _V ) -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
23	4 7 14 22	syl3anc	|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )