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

Metamath Proof Explorer

Theorem metdscn2

Description: The function F which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
metdscn2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion metdscn2 ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 metdscn2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
4 eqid ⊢ ( dist ‘ ℝ*𝑠 ) = ( dist ‘ ℝ*𝑠 )
5 4 xrsdsre ⊢ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
6 4 xrsxmet ⊢ ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* )
7 ressxr ⊢ ℝ ⊆ ℝ*
8 eqid ⊢ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) )
9 eqid ⊢ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) = ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) )
10 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) )
11 8 9 10 metrest ⊢ ( ( ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* ) ∧ ℝ ⊆ ℝ* ) → ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) = ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) ) )
12 6 7 11 mp2an ⊢ ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) = ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) )
13 5 12 tgioo ⊢ ( topGen ‘ ran (,) ) = ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ )
14 3 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ )
15 13 14 eqtr3i ⊢ ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) = ( 𝐾 ↾t ℝ )
16 15 oveq2i ⊢ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) = ( 𝐽 Cn ( 𝐾 ↾t ℝ ) )
17 3 cnfldtop ⊢ 𝐾 ∈ Top
18 cnrest2r ⊢ ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 ) )
19 17 18 ax-mp ⊢ ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 )
20 16 19 eqsstri ⊢ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 )
21 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
22 1 2 4 9 metdscn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
23 21 22 sylan ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
24 23 3adant3 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
25 1 metdsre ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 : 𝑋 ⟶ ℝ )
26 frn ⊢ ( 𝐹 : 𝑋 ⟶ ℝ → ran 𝐹 ⊆ ℝ )
27 9 mopntopon ⊢ ( ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* ) → ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ∈ ( TopOn ‘ ℝ* ) )
28 6 27 ax-mp ⊢ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ∈ ( TopOn ‘ ℝ* )
29 cnrest2 ⊢ ( ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ∈ ( TopOn ‘ ℝ* ) ∧ ran 𝐹 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → ( 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ) )
30 28 7 29 mp3an13 ⊢ ( ran 𝐹 ⊆ ℝ → ( 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ) )
31 25 26 30 3syl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ) )
32 24 31 mpbid ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) )
33 20 32 sselid ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )