Theorem tdrgunit

Description: The unit group of a topological division ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	istrg.1	$$⊢M={\mathrm{mulGrp}}_R$$
	istdrg.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	tdrgunit	$$⊢R\in \mathrm{TopDRing}\to M{\upharpoonright }_{𝑠}U\in \mathrm{TopGrp}$$

Proof

Step	Hyp	Ref	Expression
1		istrg.1	$$⊢M={\mathrm{mulGrp}}_R$$
2		istdrg.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
3	1 2	istdrg	$$⊢R\in \mathrm{TopDRing}\leftrightarrow \left(R\in \mathrm{TopRing}\wedge R\in \mathrm{DivRing}\wedge M{\upharpoonright }_{𝑠}U\in \mathrm{TopGrp}\right)$$
4	3	simp3bi	$$⊢R\in \mathrm{TopDRing}\to M{\upharpoonright }_{𝑠}U\in \mathrm{TopGrp}$$