Definition df-sdrg 37766

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 = ( w e. DivRing |-> { s e. (SubRing ` w ) | ( w ↾s s ) e. DivRing } )

Distinct variable group:   w, s

Detailed syntax breakdown of Definition df-sdrg

Step	Hyp	Ref	Expression
1		csdrg 37765	. 2 class SubDRing
2		vw	. . 3 setvar w
3		cdr 18747	. . 3 class DivRing
4	2	cv 1482	. . . . . 6 class w
5		vs	. . . . . . 7 setvar s
6	5	cv 1482	. . . . . 6 class s
7		cress 15858	. . . . . 6 class ↾s
8	4, 6, 7	co 6650	. . . . 5 class ( w ↾s s )
9	8, 3	wcel 1990	. . . 4 wff ( w ↾s s ) e. DivRing
10		csubrg 18776	. . . . 5 class SubRing
11	4, 10	cfv 5888	. . . 4 class (SubRing ` w )
12	9, 5, 11	crab 2916	. . 3 class { s e. (SubRing ` w ) | ( w ↾s s ) e. DivRing }
13	2, 3, 12	cmpt 4729	. 2 class ( w e. DivRing |-> { s e. (SubRing ` w ) | ( w ↾s s ) e. DivRing } )
14	1, 13	wceq 1483	1 wff SubDRing = ( w e. DivRing |-> { s e. (SubRing ` w ) | ( w ↾s s ) e. DivRing } )

This definition is referenced by:  issdrg  37767