Definition df-sdrg 20634

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 20645), 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

Step	Hyp	Ref	Expression
1		csdrg 20633	. 2 class SubDRing
2		vw	. . 3 setvar 𝑤
3		cdr 20583	. . 3 class DivRing
4	2	cv 1539	. . . . . 6 class 𝑤
5		vs	. . . . . . 7 setvar 𝑠
6	5	cv 1539	. . . . . 6 class 𝑠
7		cress 17180	. . . . . 6 class ↾s
8	4, 6, 7	co 7412	. . . . 5 class (𝑤 ↾s 𝑠)
9	8, 3	wcel 2105	. . . 4 wff (𝑤 ↾s 𝑠) ∈ DivRing
10		csubrg 20465	. . . . 5 class SubRing
11	4, 10	cfv 6543	. . . 4 class (SubRing‘𝑤)
12	9, 5, 11	crab 3431	. . 3 class {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}
13	2, 3, 12	cmpt 5231	. 2 class (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing})
14	1, 13	wceq 1540	1 wff SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing})

This definition is referenced by:  issdrg  20635