df-tdrg

Description: Define a topological division ring (which differs from a topological field only in being potentially noncommutative), which is a division ring and topological ring such that the unit group of the division ring (which is the set of nonzero elements) is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Assertion	df-tdrg	$⊢ TopDRing = \{r \in (TopRing \cap DivRing) \| {mulGrp}_{r} ↾_{𝑠} Unit (r) \in TopGrp\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctdrg	$class TopDRing$
1		vr	$setvar r$
2		ctrg	$class TopRing$
3		cdr	$class DivRing$
4	2 3	cin	$class (TopRing \cap DivRing)$
5		cmgp	$class mulGrp$
6	1	cv	$setvar r$
7	6 5	cfv	$class {mulGrp}_{r}$
8		cress	$class ↾_{𝑠}$
9		cui	$class Unit$
10	6 9	cfv	$class Unit (r)$
11	7 10 8	co	$class ({mulGrp}_{r} ↾_{𝑠} Unit (r))$
12		ctgp	$class TopGrp$
13	11 12	wcel	$wff {mulGrp}_{r} ↾_{𝑠} Unit (r) \in TopGrp$
14	13 1 4	crab	$class \{r \in (TopRing \cap DivRing) \| {mulGrp}_{r} ↾_{𝑠} Unit (r) \in TopGrp\}$
15	0 14	wceq	$wff TopDRing = \{r \in (TopRing \cap DivRing) \| {mulGrp}_{r} ↾_{𝑠} Unit (r) \in TopGrp\}$

Metamath Proof Explorer

Definition df-tdrg

Detailed syntax breakdown