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 \in DivRing ⟼ \{s \in SubRing (w) \| w ↾_{𝑠} s \in DivRing\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csdrg	$class SubDRing$
1		vw	$setvar w$
2		cdr	$class DivRing$
3		vs	$setvar s$
4		csubrg	$class SubRing$
5	1	cv	$setvar w$
6	5 4	cfv	$class SubRing (w)$
7		cress	$class ↾_{𝑠}$
8	3	cv	$setvar s$
9	5 8 7	co	$class (w ↾_{𝑠} s)$
10	9 2	wcel	$wff w ↾_{𝑠} s \in DivRing$
11	10 3 6	crab	$class \{s \in SubRing (w) \| w ↾_{𝑠} s \in DivRing\}$
12	1 2 11	cmpt	$class (w \in DivRing ⟼ \{s \in SubRing (w) \| w ↾_{𝑠} s \in DivRing\})$
13	0 12	wceq	$wff SubDRing = (w \in DivRing ⟼ \{s \in SubRing (w) \| w ↾_{𝑠} s \in DivRing\})$

Metamath Proof Explorer

Definition df-sdrg

Detailed syntax breakdown