This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( 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 𝑈 ) ) )