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={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
	fldgenval.3	$$⊢\phi \to S\subseteq B$$
Assertion	fldgenval	Could not format assertion : No typesetting found for |- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		fldgenval.3	$$⊢\phi \to S\subseteq B$$
4	2	elexd	$$⊢\phi \to F\in \mathrm{V}$$
5	1	fvexi	$$⊢B\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to B\in \mathrm{V}$$
7	6 3	ssexd	$$⊢\phi \to S\in \mathrm{V}$$
8	1	sdrgid	$$⊢F\in \mathrm{DivRing}\to B\in \mathrm{SubDRing}\left(F\right)$$
9	2 8	syl	$$⊢\phi \to B\in \mathrm{SubDRing}\left(F\right)$$
10		sseq2	$$⊢a=B\to \left(S\subseteq a\leftrightarrow S\subseteq B\right)$$
11	10	adantl	$$⊢\left(\phi \wedge a=B\right)\to \left(S\subseteq a\leftrightarrow S\subseteq B\right)$$
12	9 11 3	rspcedvd	$$⊢\phi \to \exists a\in \mathrm{SubDRing}\left(F\right)S\subseteq a$$
13		intexrab	$$⊢\exists a\in \mathrm{SubDRing}\left(F\right)S\subseteq a\leftrightarrow \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\in \mathrm{V}$$
14	12 13	sylib	$$⊢\phi \to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\in \mathrm{V}$$
15		simpl	$$⊢\left(f=F\wedge s=S\right)\to f=F$$
16	15	fveq2d	$$⊢\left(f=F\wedge s=S\right)\to \mathrm{SubDRing}\left(f\right)=\mathrm{SubDRing}\left(F\right)$$
17		simpr	$$⊢\left(f=F\wedge s=S\right)\to s=S$$
18	17	sseq1d	$$⊢\left(f=F\wedge s=S\right)\to \left(s\subseteq a\leftrightarrow S\subseteq a\right)$$
19	16 18	rabeqbidv	$$⊢\left(f=F\wedge s=S\right)\to \left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}=\left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
20	19	inteqd	$$⊢\left(f=F\wedge s=S\right)\to \bigcap \left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
21		df-fldgen	Could not format fldGen = ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } ) : No typesetting found for |- fldGen = ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } ) with typecode |-
22	20 21	ovmpoga	Could not format ( ( 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 } ) : No typesetting found for |- ( ( 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 } ) with typecode |-
23	4 7 14 22	syl3anc	Could not format ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) : No typesetting found for |- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) with typecode |-