This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )