Metamath Proof Explorer


Theorem xmetdcn2

Description: The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn we use the metric topology instead of the order topology on RR* , which makes the theorem a bit stronger. Since +oo is an isolated point in the metric topology, this is saying that for any points A , B which are an infinite distance apart, there is a product neighborhood around <. A , B >. such that d ( a , b ) = +oo for any a near A and b near B , i.e., the distance function is locally constant +oo . (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xmetdcn2.1 J=MetOpenD
xmetdcn2.2 C=dist𝑠*
xmetdcn2.3 K=MetOpenC
Assertion xmetdcn2 D∞MetXDJ×tJCnK

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 J=MetOpenD
2 xmetdcn2.2 C=dist𝑠*
3 xmetdcn2.3 K=MetOpenC
4 xmetf D∞MetXD:X×X*
5 rphalfcl r+r2+
6 simp-4l D∞MetXxXyXr+zXwXxDz<r2yDw<r2D∞MetX
7 simplrl D∞MetXxXyXr+xX
8 7 ad2antrr D∞MetXxXyXr+zXwXxDz<r2yDw<r2xX
9 simplrr D∞MetXxXyXr+yX
10 9 ad2antrr D∞MetXxXyXr+zXwXxDz<r2yDw<r2yX
11 simpllr D∞MetXxXyXr+zXwXxDz<r2yDw<r2r+
12 simplrl D∞MetXxXyXr+zXwXxDz<r2yDw<r2zX
13 simplrr D∞MetXxXyXr+zXwXxDz<r2yDw<r2wX
14 simprl D∞MetXxXyXr+zXwXxDz<r2yDw<r2xDz<r2
15 simprr D∞MetXxXyXr+zXwXxDz<r2yDw<r2yDw<r2
16 1 2 3 6 8 10 11 12 13 14 15 metdcnlem D∞MetXxXyXr+zXwXxDz<r2yDw<r2xDyCzDw<r
17 16 ex D∞MetXxXyXr+zXwXxDz<r2yDw<r2xDyCzDw<r
18 17 ralrimivva D∞MetXxXyXr+zXwXxDz<r2yDw<r2xDyCzDw<r
19 breq2 s=r2xDz<sxDz<r2
20 breq2 s=r2yDw<syDw<r2
21 19 20 anbi12d s=r2xDz<syDw<sxDz<r2yDw<r2
22 21 imbi1d s=r2xDz<syDw<sxDyCzDw<rxDz<r2yDw<r2xDyCzDw<r
23 22 2ralbidv s=r2zXwXxDz<syDw<sxDyCzDw<rzXwXxDz<r2yDw<r2xDyCzDw<r
24 23 rspcev r2+zXwXxDz<r2yDw<r2xDyCzDw<rs+zXwXxDz<syDw<sxDyCzDw<r
25 5 18 24 syl2an2 D∞MetXxXyXr+s+zXwXxDz<syDw<sxDyCzDw<r
26 25 ralrimiva D∞MetXxXyXr+s+zXwXxDz<syDw<sxDyCzDw<r
27 26 ralrimivva D∞MetXxXyXr+s+zXwXxDz<syDw<sxDyCzDw<r
28 id D∞MetXD∞MetX
29 2 xrsxmet C∞Met*
30 29 a1i D∞MetXC∞Met*
31 1 1 3 txmetcn D∞MetXD∞MetXC∞Met*DJ×tJCnKD:X×X*xXyXr+s+zXwXxDz<syDw<sxDyCzDw<r
32 28 30 31 mpd3an23 D∞MetXDJ×tJCnKD:X×X*xXyXr+s+zXwXxDz<syDw<sxDyCzDw<r
33 4 27 32 mpbir2and D∞MetXDJ×tJCnK