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 = ( 𝑤 ∈ DivRing ↦ { 𝑠 ∈ ( SubRing ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ DivRing } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csdrg	⊢ SubDRing
1		vw	⊢ 𝑤
2		cdr	⊢ DivRing
3		vs	⊢ 𝑠
4		csubrg	⊢ SubRing
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( SubRing ‘ 𝑤 )
7		cress	⊢ ↾s
8	3	cv	⊢ 𝑠
9	5 8 7	co	⊢ ( 𝑤 ↾s 𝑠 )
10	9 2	wcel	⊢ ( 𝑤 ↾s 𝑠 ) ∈ DivRing
11	10 3 6	crab	⊢ { 𝑠 ∈ ( SubRing ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ DivRing }
12	1 2 11	cmpt	⊢ ( 𝑤 ∈ DivRing ↦ { 𝑠 ∈ ( SubRing ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ DivRing } )
13	0 12	wceq	⊢ SubDRing = ( 𝑤 ∈ DivRing ↦ { 𝑠 ∈ ( SubRing ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ DivRing } )