# Metamath Proof Explorer

## Definition df-sdrg

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
Assertion df-sdrg ${⊢}\mathrm{SubDRing}=\left({w}\in \mathrm{DivRing}⟼\left\{{s}\in \mathrm{SubRing}\left({w}\right)|{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 csdrg ${class}\mathrm{SubDRing}$
1 vw ${setvar}{w}$
2 cdr ${class}\mathrm{DivRing}$
3 vs ${setvar}{s}$
4 csubrg ${class}\mathrm{SubRing}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}\mathrm{SubRing}\left({w}\right)$
7 cress ${class}{↾}_{𝑠}$
8 3 cv ${setvar}{s}$
9 5 8 7 co ${class}\left({w}{↾}_{𝑠}{s}\right)$
10 9 2 wcel ${wff}{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}$
11 10 3 6 crab ${class}\left\{{s}\in \mathrm{SubRing}\left({w}\right)|{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}$
12 1 2 11 cmpt ${class}\left({w}\in \mathrm{DivRing}⟼\left\{{s}\in \mathrm{SubRing}\left({w}\right)|{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}\right)$
13 0 12 wceq ${wff}\mathrm{SubDRing}=\left({w}\in \mathrm{DivRing}⟼\left\{{s}\in \mathrm{SubRing}\left({w}\right)|{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}\right)$