![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-sdrg | Structured version Visualization version GIF version |
Description: Define the function associating with a ring the set of its sub-division-rings. A sub-division-ring of a ring is a subset of its base set which is a division ring when equipped with the induced structure (sum, multiplication, zero, and unity). If a ring is commutative (resp., a field), then its sub-division-rings are commutative (resp., are fields) (fldsdrgfld 20645), so we do not make a specific definition for subfields. (Contributed by Stefan O'Rear, 3-Oct-2015.) TODO: extend this definition to a function with domain V or at least Ring and not only DivRing. |
Ref | Expression |
---|---|
df-sdrg | ⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csdrg 20633 | . 2 class SubDRing | |
2 | vw | . . 3 setvar 𝑤 | |
3 | cdr 20583 | . . 3 class DivRing | |
4 | 2 | cv 1539 | . . . . . 6 class 𝑤 |
5 | vs | . . . . . . 7 setvar 𝑠 | |
6 | 5 | cv 1539 | . . . . . 6 class 𝑠 |
7 | cress 17180 | . . . . . 6 class ↾s | |
8 | 4, 6, 7 | co 7412 | . . . . 5 class (𝑤 ↾s 𝑠) |
9 | 8, 3 | wcel 2105 | . . . 4 wff (𝑤 ↾s 𝑠) ∈ DivRing |
10 | csubrg 20465 | . . . . 5 class SubRing | |
11 | 4, 10 | cfv 6543 | . . . 4 class (SubRing‘𝑤) |
12 | 9, 5, 11 | crab 3431 | . . 3 class {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing} |
13 | 2, 3, 12 | cmpt 5231 | . 2 class (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) |
14 | 1, 13 | wceq 1540 | 1 wff SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) |
Colors of variables: wff setvar class |
This definition is referenced by: issdrg 20635 |
Copyright terms: Public domain | W3C validator |