![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-fldgen | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-fldgen | ⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfldgen 33277 | . 2 class fldGen | |
2 | vf | . . 3 setvar 𝑓 | |
3 | vs | . . 3 setvar 𝑠 | |
4 | cvv 3488 | . . 3 class V | |
5 | 3 | cv 1536 | . . . . . 6 class 𝑠 |
6 | va | . . . . . . 7 setvar 𝑎 | |
7 | 6 | cv 1536 | . . . . . 6 class 𝑎 |
8 | 5, 7 | wss 3976 | . . . . 5 wff 𝑠 ⊆ 𝑎 |
9 | 2 | cv 1536 | . . . . . 6 class 𝑓 |
10 | csdrg 20809 | . . . . . 6 class SubDRing | |
11 | 9, 10 | cfv 6573 | . . . . 5 class (SubDRing‘𝑓) |
12 | 8, 6, 11 | crab 3443 | . . . 4 class {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎} |
13 | 12 | cint 4970 | . . 3 class ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎} |
14 | 2, 3, 4, 4, 13 | cmpo 7450 | . 2 class (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}) |
15 | 1, 14 | wceq 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 |