Definition df-sdrg

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

	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 } )