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 20172), 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 20166 | . 2 class SubDRing | |
2 | vw | . . 3 setvar π€ | |
3 | cdr 20093 | . . 3 class DivRing | |
4 | 2 | cv 1539 | . . . . . 6 class π€ |
5 | vs | . . . . . . 7 setvar π | |
6 | 5 | cv 1539 | . . . . . 6 class π |
7 | cress 17038 | . . . . . 6 class βΎs | |
8 | 4, 6, 7 | co 7337 | . . . . 5 class (π€ βΎs π ) |
9 | 8, 3 | wcel 2105 | . . . 4 wff (π€ βΎs π ) β DivRing |
10 | csubrg 20125 | . . . . 5 class SubRing | |
11 | 4, 10 | cfv 6479 | . . . 4 class (SubRingβπ€) |
12 | 9, 5, 11 | crab 3403 | . . 3 class {π β (SubRingβπ€) β£ (π€ βΎs π ) β DivRing} |
13 | 2, 3, 12 | cmpt 5175 | . 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 20168 |
Copyright terms: Public domain | W3C validator |