Definition df-fldgen

Description: Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg ). If the base structure is a field, this is a subfield (see fldgenfld and fldsdrgfld ). In general this will be used in the context of fields, hence the name fldGen . (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025)

	Ref	Expression
Assertion	df-fldgen	|- fldGen = ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfldgen	|- fldGen
1		vf	|- f
2		cvv	|- _V
3		vs	|- s
4		va	|- a
5		csdrg	|- SubDRing
6	1	cv	|- f
7	6 5	cfv	|- ( SubDRing ` f )
8	3	cv	|- s
9	4	cv	|- a
10	8 9	wss	|- s C_ a
11	10 4 7	crab	|- { a e. ( SubDRing ` f ) | s C_ a }
12	11	cint	|- |^| { a e. ( SubDRing ` f ) | s C_ a }
13	1 3 2 2 12	cmpo	|- ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } )
14	0 13	wceq	|- fldGen = ( f e. _V , s e. _V |-> |^| { a e. ( SubDRing ` f ) | s C_ a } )