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 ⊢ SubDRing = w ∈ DivRing ⟼ s ∈ SubRing ⁡ w | w ↾ 𝑠 s ∈ DivRing

Detailed syntax breakdown

Step Hyp Ref Expression
0 csdrg class SubDRing
1 vw setvar w
2 cdr class DivRing
3 vs setvar s
4 csubrg class SubRing
5 1 cv setvar w
6 5 4 cfv class SubRing ⁡ w
7 cress class ↾ 𝑠
8 3 cv setvar s
9 5 8 7 co class w ↾ 𝑠 s
10 9 2 wcel wff w ↾ 𝑠 s ∈ DivRing
11 10 3 6 crab class s ∈ SubRing ⁡ w | w ↾ 𝑠 s ∈ DivRing
12 1 2 11 cmpt class w ∈ DivRing ⟼ s ∈ SubRing ⁡ w | w ↾ 𝑠 s ∈ DivRing
13 0 12 wceq wff SubDRing = w ∈ DivRing ⟼ s ∈ SubRing ⁡ w | w ↾ 𝑠 s ∈ DivRing