Metamath Proof Explorer

Theorem invrcn

Description: The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to the field. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Hypotheses	mulrcn.j	$⊢ J = TopOpen (R)$
		invrcn.i	$⊢ I = {inv}_{r} (R)$
		invrcn.u	$⊢ U = Unit (R)$
	Assertion	invrcn	$⊢ R \in TopDRing \to I \in ((J ↾_{𝑡} U) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	$⊢ J = TopOpen (R)$
2		invrcn.i	$⊢ I = {inv}_{r} (R)$
3		invrcn.u	$⊢ U = Unit (R)$
4		tdrgtps	$⊢ R \in TopDRing \to R \in TopSp$
5	1	tpstop	$⊢ R \in TopSp \to J \in Top$
6		cnrest2r	$⊢ J \in Top \to (J ↾_{𝑡} U) Cn (J ↾_{𝑡} U) \subseteq (J ↾_{𝑡} U) Cn J$
7	4 5 6	3syl	$⊢ R \in TopDRing \to (J ↾_{𝑡} U) Cn (J ↾_{𝑡} U) \subseteq (J ↾_{𝑡} U) Cn J$
8	1 2 3	invrcn2	$⊢ R \in TopDRing \to I \in ((J ↾_{𝑡} U) Cn (J ↾_{𝑡} U))$
9	7 8	sseldd	$⊢ R \in TopDRing \to I \in ((J ↾_{𝑡} U) Cn J)$