Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fldgen Structured version   Visualization version   GIF version

Definition df-fldgen 33278
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 33281). If the base structure is a field, this is a subfield (see fldgenfld 33287 and fldsdrgfld 20821). 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.)
Assertion
Ref Expression
df-fldgen fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠𝑎})
Distinct variable group:   𝑓,𝑠,𝑎

Detailed syntax breakdown of Definition df-fldgen
StepHypRef Expression
1 cfldgen 33277 . 2 class fldGen
2 vf . . 3 setvar 𝑓
3 vs . . 3 setvar 𝑠
4 cvv 3488 . . 3 class V
53cv 1536 . . . . . 6 class 𝑠
6 va . . . . . . 7 setvar 𝑎
76cv 1536 . . . . . 6 class 𝑎
85, 7wss 3976 . . . . 5 wff 𝑠𝑎
92cv 1536 . . . . . 6 class 𝑓
10 csdrg 20809 . . . . . 6 class SubDRing
119, 10cfv 6573 . . . . 5 class (SubDRing‘𝑓)
128, 6, 11crab 3443 . . . 4 class {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠𝑎}
1312cint 4970 . . 3 class {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠𝑎}
142, 3, 4, 4, 13cmpo 7450 . 2 class (𝑓 ∈ V, 𝑠 ∈ V ↦ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠𝑎})
151, 14wceq 1537 1 wff fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠𝑎})
Colors of variables: wff setvar class
This definition is referenced by:  fldgenval  33279
  Copyright terms: Public domain W3C validator