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 ∈ TopRing ∩ DivRing | mulGrp r ↾ 𝑠 Unit ⁡ r ∈ TopGrp

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctdrg class TopDRing
1 vr setvar r
2 ctrg class TopRing
3 cdr class DivRing
4 2 3 cin class TopRing ∩ DivRing
5 cmgp class mulGrp
6 1 cv setvar r
7 6 5 cfv class mulGrp r
8 cress class ↾ 𝑠
9 cui class Unit
10 6 9 cfv class Unit ⁡ r
11 7 10 8 co class mulGrp r ↾ 𝑠 Unit ⁡ r
12 ctgp class TopGrp
13 11 12 wcel wff mulGrp r ↾ 𝑠 Unit ⁡ r ∈ TopGrp
14 13 1 4 crab class r ∈ TopRing ∩ DivRing | mulGrp r ↾ 𝑠 Unit ⁡ r ∈ TopGrp
15 0 14 wceq wff TopDRing = r ∈ TopRing ∩ DivRing | mulGrp r ↾ 𝑠 Unit ⁡ r ∈ TopGrp