![]() |
Mathbox for Stefan O'Rear |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-sdrg | Structured version Visualization version GIF version |
Description: A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
Ref | Expression |
---|---|
df-sdrg | ⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csdrg 38724 | . 2 class SubDRing | |
2 | vw | . . 3 setvar 𝑤 | |
3 | cdr 19139 | . . 3 class DivRing | |
4 | 2 | cv 1600 | . . . . . 6 class 𝑤 |
5 | vs | . . . . . . 7 setvar 𝑠 | |
6 | 5 | cv 1600 | . . . . . 6 class 𝑠 |
7 | cress 16256 | . . . . . 6 class ↾s | |
8 | 4, 6, 7 | co 6922 | . . . . 5 class (𝑤 ↾s 𝑠) |
9 | 8, 3 | wcel 2107 | . . . 4 wff (𝑤 ↾s 𝑠) ∈ DivRing |
10 | csubrg 19168 | . . . . 5 class SubRing | |
11 | 4, 10 | cfv 6135 | . . . 4 class (SubRing‘𝑤) |
12 | 9, 5, 11 | crab 3094 | . . 3 class {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing} |
13 | 2, 3, 12 | cmpt 4965 | . 2 class (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) |
14 | 1, 13 | wceq 1601 | 1 wff SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) |
Colors of variables: wff setvar class |
This definition is referenced by: issdrg 38726 |
Copyright terms: Public domain | W3C validator |