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 ∈ V , s ∈ V ⟼ ⋂ a ∈ SubDRing ⁡ f | s ⊆ a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfldgen class fldGen
1 vf setvar f
2 cvv class V
3 vs setvar s
4 va setvar a
5 csdrg class SubDRing
6 1 cv setvar f
7 6 5 cfv class SubDRing ⁡ f
8 3 cv setvar s
9 4 cv setvar a
10 8 9 wss wff s ⊆ a
11 10 4 7 crab class a ∈ SubDRing ⁡ f | s ⊆ a
12 11 cint class ⋂ a ∈ SubDRing ⁡ f | s ⊆ a
13 1 3 2 2 12 cmpo class f ∈ V , s ∈ V ⟼ ⋂ a ∈ SubDRing ⁡ f | s ⊆ a
14 0 13 wceq wff fldGen = f ∈ V , s ∈ V ⟼ ⋂ a ∈ SubDRing ⁡ f | s ⊆ a