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 = ( 𝑤 ∈ 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 } )

Metamath Proof Explorer

Definition df-sdrg

Detailed syntax breakdown