This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }