Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctdrg 
 |-  TopDRing
1 vr 
 |-  r
2 ctrg 
 |-  TopRing
3 cdr 
 |-  DivRing
4 2 3 cin 
 |-  ( TopRing i^i DivRing )
5 cmgp 
 |-  mulGrp
6 1 cv 
 |-  r
7 6 5 cfv 
 |-  ( mulGrp ` r )
8 cress 
 |-  |`s
9 cui 
 |-  Unit
10 6 9 cfv 
 |-  ( Unit ` r )
11 7 10 8 co 
 |-  ( ( mulGrp ` r ) |`s ( Unit ` r ) )
12 ctgp 
 |-  TopGrp
13 11 12 wcel 
 |-  ( ( mulGrp ` r ) |`s ( Unit ` r ) ) e. TopGrp
14 13 1 4 crab 
 |-  { r e. ( TopRing i^i DivRing ) | ( ( mulGrp ` r ) |`s ( Unit ` r ) ) e. TopGrp }
15 0 14 wceq 
 |-  TopDRing = { r e. ( TopRing i^i DivRing ) | ( ( mulGrp ` r ) |`s ( Unit ` r ) ) e. TopGrp }