Definition df-tdrg 21964

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 = { r e. ( TopRing i^i DivRing ) | ( (mulGrp ` r ) ↾s (Unit ` r ) ) e. TopGrp }

Detailed syntax breakdown of Definition df-tdrg

Step	Hyp	Ref	Expression
1		ctdrg 21960	. 2 class TopDRing
2		vr	. . . . . . 7 setvar r
3	2	cv 1482	. . . . . 6 class r
4		cmgp 18489	. . . . . 6 class mulGrp
5	3, 4	cfv 5888	. . . . 5 class (mulGrp ` r )
6		cui 18639	. . . . . 6 class Unit
7	3, 6	cfv 5888	. . . . 5 class (Unit ` r )
8		cress 15858	. . . . 5 class ↾s
9	5, 7, 8	co 6650	. . . 4 class ( (mulGrp ` r ) ↾s (Unit ` r ) )
10		ctgp 21875	. . . 4 class TopGrp
11	9, 10	wcel 1990	. . 3 wff ( (mulGrp ` r ) ↾s (Unit ` r ) ) e. TopGrp
12		ctrg 21959	. . . 4 class TopRing
13		cdr 18747	. . . 4 class DivRing
14	12, 13	cin 3573	. . 3 class ( TopRing i^i DivRing )
15	11, 2, 14	crab 2916	. 2 class { r e. ( TopRing i^i DivRing ) | ( (mulGrp ` r ) ↾s (Unit ` r ) ) e. TopGrp }
16	1, 15	wceq 1483	1 wff TopDRing = { r e. ( TopRing i^i DivRing ) | ( (mulGrp ` r ) ↾s (Unit ` r ) ) e. TopGrp }

This definition is referenced by:  istdrg  21969