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 F = x X sup ran y S x D y * <
metdscn.j J = MetOpen D
metdscn2.k K = TopOpen fld
Assertion metdscn2 D Met X S X S F J Cn K

Proof

Step Hyp Ref Expression
1 metdscn.f F = x X sup ran y S x D y * <
2 metdscn.j J = MetOpen D
3 metdscn2.k K = TopOpen fld
4 eqid dist 𝑠 * = dist 𝑠 *
5 4 xrsdsre dist 𝑠 * 2 = abs 2
6 4 xrsxmet dist 𝑠 * ∞Met *
7 ressxr *
8 eqid dist 𝑠 * 2 = dist 𝑠 * 2
9 eqid MetOpen dist 𝑠 * = MetOpen dist 𝑠 *
10 eqid MetOpen dist 𝑠 * 2 = MetOpen dist 𝑠 * 2
11 8 9 10 metrest dist 𝑠 * ∞Met * * MetOpen dist 𝑠 * 𝑡 = MetOpen dist 𝑠 * 2
12 6 7 11 mp2an MetOpen dist 𝑠 * 𝑡 = MetOpen dist 𝑠 * 2
13 5 12 tgioo topGen ran . = MetOpen dist 𝑠 * 𝑡
14 3 tgioo2 topGen ran . = K 𝑡
15 13 14 eqtr3i MetOpen dist 𝑠 * 𝑡 = K 𝑡
16 15 oveq2i J Cn MetOpen dist 𝑠 * 𝑡 = J Cn K 𝑡
17 3 cnfldtop K Top
18 cnrest2r K Top J Cn K 𝑡 J Cn K
19 17 18 ax-mp J Cn K 𝑡 J Cn K
20 16 19 eqsstri J Cn MetOpen dist 𝑠 * 𝑡 J Cn K
21 metxmet D Met X D ∞Met X
22 1 2 4 9 metdscn D ∞Met X S X F J Cn MetOpen dist 𝑠 *
23 21 22 sylan D Met X S X F J Cn MetOpen dist 𝑠 *
24 23 3adant3 D Met X S X S F J Cn MetOpen dist 𝑠 *
25 1 metdsre D Met X S X S F : X
26 frn F : X ran F
27 9 mopntopon dist 𝑠 * ∞Met * MetOpen dist 𝑠 * TopOn *
28 6 27 ax-mp MetOpen dist 𝑠 * TopOn *
29 cnrest2 MetOpen dist 𝑠 * TopOn * ran F * F J Cn MetOpen dist 𝑠 * F J Cn MetOpen dist 𝑠 * 𝑡
30 28 7 29 mp3an13 ran F F J Cn MetOpen dist 𝑠 * F J Cn MetOpen dist 𝑠 * 𝑡
31 25 26 30 3syl D Met X S X S F J Cn MetOpen dist 𝑠 * F J Cn MetOpen dist 𝑠 * 𝑡
32 24 31 mpbid D Met X S X S F J Cn MetOpen dist 𝑠 * 𝑡
33 20 32 sselid D Met X S X S F J Cn K