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

Metamath Proof Explorer

Theorem dvrcn

Description: The division function is continuous in a topological field. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses dvrcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
dvrcn.d ⊢ / = ( /r ‘ 𝑅 )
dvrcn.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion dvrcn ( 𝑅 ∈ TopDRing → / ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 dvrcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
2 dvrcn.d ⊢ / = ( /r ‘ 𝑅 )
3 dvrcn.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
7 4 5 3 6 2 dvrfval ⊢ / = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑦 ) ) )
8 tdrgtrg ⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopRing )
9 tdrgtps ⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopSp )
10 4 1 istps ⊢ ( 𝑅 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
11 9 10 sylib ⊢ ( 𝑅 ∈ TopDRing → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
12 4 3 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑅 )
13 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) ∧ 𝑈 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
14 11 12 13 sylancl ⊢ ( 𝑅 ∈ TopDRing → ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
15 11 14 cnmpt1st ⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ 𝑥 ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )
16 11 14 cnmpt2nd ⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ 𝑦 ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn ( 𝐽 ↾t 𝑈 ) ) )
17 1 6 3 invrcn ⊢ ( 𝑅 ∈ TopDRing → ( invr ‘ 𝑅 ) ∈ ( ( 𝐽 ↾t 𝑈 ) Cn 𝐽 ) )
18 11 14 16 17 cnmpt21f ⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ ( ( invr ‘ 𝑅 ) ‘ 𝑦 ) ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )
19 1 5 8 11 14 15 18 cnmpt2mulr ⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑦 ) ) ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )
20 7 19 eqeltrid ⊢ ( 𝑅 ∈ TopDRing → / ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )