Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sdrg Structured version   Visualization version   GIF version

Definition df-sdrg 38264
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.)
Assertion
Ref Expression
df-sdrg SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤s 𝑠) ∈ DivRing})
Distinct variable group:   𝑤,𝑠

Detailed syntax breakdown of Definition df-sdrg
StepHypRef Expression
1 csdrg 38263 . 2 class SubDRing
2 vw . . 3 setvar 𝑤
3 cdr 18945 . . 3 class DivRing
42cv 1627 . . . . . 6 class 𝑤
5 vs . . . . . . 7 setvar 𝑠
65cv 1627 . . . . . 6 class 𝑠
7 cress 16056 . . . . . 6 class s
84, 6, 7co 6809 . . . . 5 class (𝑤s 𝑠)
98, 3wcel 2135 . . . 4 wff (𝑤s 𝑠) ∈ DivRing
10 csubrg 18974 . . . . 5 class SubRing
114, 10cfv 6045 . . . 4 class (SubRing‘𝑤)
129, 5, 11crab 3050 . . 3 class {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤s 𝑠) ∈ DivRing}
132, 3, 12cmpt 4877 . 2 class (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤s 𝑠) ∈ DivRing})
141, 13wceq 1628 1 wff SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤s 𝑠) ∈ DivRing})
Colors of variables: wff setvar class
This definition is referenced by:  issdrg  38265
  Copyright terms: Public domain W3C validator