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	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
	invrcn.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
	invrcn.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	invrcn2	⊢ ( 𝑅 ∈ TopDRing → 𝐼 ∈ ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
2		invrcn.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
3		invrcn.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
4		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5	4 3	tdrgunit	⊢ ( 𝑅 ∈ TopDRing → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ TopGrp )
6		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
7	4 1	mgptopn	⊢ 𝐽 = ( TopOpen ‘ ( mulGrp ‘ 𝑅 ) )
8	6 7	resstopn	⊢ ( 𝐽 ↾t 𝑈 ) = ( TopOpen ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
9	3 6 2	invrfval	⊢ 𝐼 = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
10	8 9	tgpinv	⊢ ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ TopGrp → 𝐼 ∈ ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) )
11	5 10	syl	⊢ ( 𝑅 ∈ TopDRing → 𝐼 ∈ ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) )