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 = { 𝑟 ∈ ( TopRing ∩ DivRing ) ∣ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ∈ TopGrp }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctdrg TopDRing
1 vr 𝑟
2 ctrg TopRing
3 cdr DivRing
4 2 3 cin ( TopRing ∩ DivRing )
5 cmgp mulGrp
6 1 cv 𝑟
7 6 5 cfv ( mulGrp ‘ 𝑟 )
8 cress s
9 cui Unit
10 6 9 cfv ( Unit ‘ 𝑟 )
11 7 10 8 co ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) )
12 ctgp TopGrp
13 11 12 wcel ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ∈ TopGrp
14 13 1 4 crab { 𝑟 ∈ ( TopRing ∩ DivRing ) ∣ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ∈ TopGrp }
15 0 14 wceq TopDRing = { 𝑟 ∈ ( TopRing ∩ DivRing ) ∣ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ∈ TopGrp }