Metamath Proof Explorer

Theorem invrcn2

Description: The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to itself. (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	invrcn2	$⊢ R \in TopDRing \to I \in ((J ↾_{𝑡} U) Cn (J ↾_{𝑡} U))$

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		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4 3	tdrgunit	$⊢ R \in TopDRing \to {mulGrp}_{R} ↾_{𝑠} U \in TopGrp$
6		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} U = {mulGrp}_{R} ↾_{𝑠} U$
7	4 1	mgptopn	$⊢ J = TopOpen ({mulGrp}_{R})$
8	6 7	resstopn	$⊢ J ↾_{𝑡} U = TopOpen ({mulGrp}_{R} ↾_{𝑠} U)$
9	3 6 2	invrfval	$⊢ I = {inv}_{g} ({mulGrp}_{R} ↾_{𝑠} U)$
10	8 9	tgpinv	$⊢ {mulGrp}_{R} ↾_{𝑠} U \in TopGrp \to I \in ((J ↾_{𝑡} U) Cn (J ↾_{𝑡} U))$
11	5 10	syl	$⊢ R \in TopDRing \to I \in ((J ↾_{𝑡} U) Cn (J ↾_{𝑡} U))$