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 }