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 33046
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 33049). If the base structure is a field, this is a subfield (see fldgenfld 33055 and fldsdrgfld 20690). 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 33045 . 2 class fldGen
2 vf . . 3 setvar 𝑓
3 vs . . 3 setvar 𝑠
4 cvv 3463 . . 3 class V
53cv 1532 . . . . . 6 class 𝑠
6 va . . . . . . 7 setvar π‘Ž
76cv 1532 . . . . . 6 class π‘Ž
85, 7wss 3939 . . . . 5 wff 𝑠 βŠ† π‘Ž
92cv 1532 . . . . . 6 class 𝑓
10 csdrg 20678 . . . . . 6 class SubDRing
119, 10cfv 6543 . . . . 5 class (SubDRingβ€˜π‘“)
128, 6, 11crab 3419 . . . 4 class {π‘Ž ∈ (SubDRingβ€˜π‘“) ∣ 𝑠 βŠ† π‘Ž}
1312cint 4944 . . 3 class ∩ {π‘Ž ∈ (SubDRingβ€˜π‘“) ∣ 𝑠 βŠ† π‘Ž}
142, 3, 4, 4, 13cmpo 7418 . 2 class (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {π‘Ž ∈ (SubDRingβ€˜π‘“) ∣ 𝑠 βŠ† π‘Ž})
151, 14wceq 1533 1 wff fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {π‘Ž ∈ (SubDRingβ€˜π‘“) ∣ 𝑠 βŠ† π‘Ž})
Colors of variables: wff setvar class
This definition is referenced by:  fldgenval  33047
  Copyright terms: Public domain W3C validator