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

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
2		invrcn.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
3		invrcn.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
4		tdrgtps	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopSp )
5	1	tpstop	⊢ ( 𝑅 ∈ TopSp → 𝐽 ∈ Top )
6		cnrest2r	⊢ ( 𝐽 ∈ Top → ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) ⊆ ( ( 𝐽 ↾t 𝑈 ) Cn 𝐽 ) )
7	4 5 6	3syl	⊢ ( 𝑅 ∈ TopDRing → ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) ⊆ ( ( 𝐽 ↾t 𝑈 ) Cn 𝐽 ) )
8	1 2 3	invrcn2	⊢ ( 𝑅 ∈ TopDRing → 𝐼 ∈ ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) )
9	7 8	sseldd	⊢ ( 𝑅 ∈ TopDRing → 𝐼 ∈ ( ( 𝐽 ↾t 𝑈 ) Cn 𝐽 ) )