Definition df-tdrg 24169

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

Assertion

Ref	Expression
df-tdrg	⊢ TopDRing = {𝑟 ∈ (TopRing ∩ DivRing) ∣ ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) ∈ TopGrp}

Detailed syntax breakdown of Definition df-tdrg

Step	Hyp	Ref	Expression
1		ctdrg 24165	. 2 class TopDRing
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1539	. . . . . 6 class 𝑟
4		cmgp 20137	. . . . . 6 class mulGrp
5	3, 4	cfv 6561	. . . . 5 class (mulGrp‘𝑟)
6		cui 20355	. . . . . 6 class Unit
7	3, 6	cfv 6561	. . . . 5 class (Unit‘𝑟)
8		cress 17274	. . . . 5 class ↾s
9	5, 7, 8	co 7431	. . . 4 class ((mulGrp‘𝑟) ↾s (Unit‘𝑟))
10		ctgp 24079	. . . 4 class TopGrp
11	9, 10	wcel 2108	. . 3 wff ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) ∈ TopGrp
12		ctrg 24164	. . . 4 class TopRing
13		cdr 20729	. . . 4 class DivRing
14	12, 13	cin 3950	. . 3 class (TopRing ∩ DivRing)
15	11, 2, 14	crab 3436	. 2 class {𝑟 ∈ (TopRing ∩ DivRing) ∣ ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) ∈ TopGrp}
16	1, 15	wceq 1540	1 wff TopDRing = {𝑟 ∈ (TopRing ∩ DivRing) ∣ ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) ∈ TopGrp}

This definition is referenced by:  istdrg  24174