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 𝐾 ) )