MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sdrg Structured version   Visualization version   GIF version

Definition df-sdrg 20167
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.
Assertion
Ref Expression
df-sdrg SubDRing = (𝑀 ∈ DivRing ↦ {𝑠 ∈ (SubRingβ€˜π‘€) ∣ (𝑀 β†Ύs 𝑠) ∈ DivRing})
Distinct variable group:   𝑀,𝑠

Detailed syntax breakdown of Definition df-sdrg
StepHypRef Expression
1 csdrg 20166 . 2 class SubDRing
2 vw . . 3 setvar 𝑀
3 cdr 20093 . . 3 class DivRing
42cv 1539 . . . . . 6 class 𝑀
5 vs . . . . . . 7 setvar 𝑠
65cv 1539 . . . . . 6 class 𝑠
7 cress 17038 . . . . . 6 class β†Ύs
84, 6, 7co 7337 . . . . 5 class (𝑀 β†Ύs 𝑠)
98, 3wcel 2105 . . . 4 wff (𝑀 β†Ύs 𝑠) ∈ DivRing
10 csubrg 20125 . . . . 5 class SubRing
114, 10cfv 6479 . . . 4 class (SubRingβ€˜π‘€)
129, 5, 11crab 3403 . . 3 class {𝑠 ∈ (SubRingβ€˜π‘€) ∣ (𝑀 β†Ύs 𝑠) ∈ DivRing}
132, 3, 12cmpt 5175 . 2 class (𝑀 ∈ DivRing ↦ {𝑠 ∈ (SubRingβ€˜π‘€) ∣ (𝑀 β†Ύs 𝑠) ∈ DivRing})
141, 13wceq 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