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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csdrg	|- SubDRing
1		vw	|- w
2		cdr	|- DivRing
3		vs	|- s
4		csubrg	|- SubRing
5	1	cv	|- w
6	5 4	cfv	|- ( SubRing ` w )
7		cress	|- |`s
8	3	cv	|- s
9	5 8 7	co	|- ( w |`s s )
10	9 2	wcel	|- ( w |`s s ) e. DivRing
11	10 3 6	crab	|- { s e. ( SubRing ` w ) | ( w |`s s ) e. DivRing }
12	1 2 11	cmpt	|- ( w e. DivRing |-> { s e. ( SubRing ` w ) | ( w |`s s ) e. DivRing } )
13	0 12	wceq	|- SubDRing = ( w e. DivRing |-> { s e. ( SubRing ` w ) | ( w |`s s ) e. DivRing } )