Metamath Proof Explorer

Theorem metdcnlem

Description: The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xmetdcn2.1 ⊢ J = MetOpen ⁡ D
xmetdcn2.2 ⊢ C = dist ⁡ ℝ 𝑠 *
xmetdcn2.3 ⊢ K = MetOpen ⁡ C
metdcn.d ⊢ φ → D ∈ ∞Met ⁡ X
metdcn.a ⊢ φ → A ∈ X
metdcn.b ⊢ φ → B ∈ X
metdcn.r ⊢ φ → R ∈ ℝ +
metdcn.y ⊢ φ → Y ∈ X
metdcn.z ⊢ φ → Z ∈ X
metdcn.4 ⊢ φ → A D Y < R 2
metdcn.5 ⊢ φ → B D Z < R 2
Assertion metdcnlem ⊢ φ → A D B C Y D Z < R

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 ⊢ J = MetOpen ⁡ D
2 xmetdcn2.2 ⊢ C = dist ⁡ ℝ 𝑠 *
3 xmetdcn2.3 ⊢ K = MetOpen ⁡ C
4 metdcn.d ⊢ φ → D ∈ ∞Met ⁡ X
5 metdcn.a ⊢ φ → A ∈ X
6 metdcn.b ⊢ φ → B ∈ X
7 metdcn.r ⊢ φ → R ∈ ℝ +
8 metdcn.y ⊢ φ → Y ∈ X
9 metdcn.z ⊢ φ → Z ∈ X
10 metdcn.4 ⊢ φ → A D Y < R 2
11 metdcn.5 ⊢ φ → B D Z < R 2
12 2 xrsxmet ⊢ C ∈ ∞Met ⁡ ℝ *
13 12 a1i ⊢ φ → C ∈ ∞Met ⁡ ℝ *
14 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
15 4 5 6 14 syl3anc ⊢ φ → A D B ∈ ℝ *
16 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ Y ∈ X ∧ Z ∈ X → Y D Z ∈ ℝ *
17 4 8 9 16 syl3anc ⊢ φ → Y D Z ∈ ℝ *
18 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ Y ∈ X ∧ B ∈ X → Y D B ∈ ℝ *
19 4 8 6 18 syl3anc ⊢ φ → Y D B ∈ ℝ *
20 7 rphalfcld ⊢ φ → R 2 ∈ ℝ +
21 20 rpred ⊢ φ → R 2 ∈ ℝ
22 xmetcl ⊢ C ∈ ∞Met ⁡ ℝ * ∧ A D B ∈ ℝ * ∧ Y D B ∈ ℝ * → A D B C Y D B ∈ ℝ *
23 13 15 19 22 syl3anc ⊢ φ → A D B C Y D B ∈ ℝ *
24 20 rpxrd ⊢ φ → R 2 ∈ ℝ *
25 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ Y ∈ X → A D Y ∈ ℝ *
26 4 5 8 25 syl3anc ⊢ φ → A D Y ∈ ℝ *
27 2 xmetrtri2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ Y ∈ X ∧ B ∈ X → A D B C Y D B ≤ A D Y
28 4 5 8 6 27 syl13anc ⊢ φ → A D B C Y D B ≤ A D Y
29 23 26 24 28 10 xrlelttrd ⊢ φ → A D B C Y D B < R 2
30 23 24 29 xrltled ⊢ φ → A D B C Y D B ≤ R 2
31 xmetlecl ⊢ C ∈ ∞Met ⁡ ℝ * ∧ A D B ∈ ℝ * ∧ Y D B ∈ ℝ * ∧ R 2 ∈ ℝ ∧ A D B C Y D B ≤ R 2 → A D B C Y D B ∈ ℝ
32 13 15 19 21 30 31 syl122anc ⊢ φ → A D B C Y D B ∈ ℝ
33 xmetcl ⊢ C ∈ ∞Met ⁡ ℝ * ∧ Y D B ∈ ℝ * ∧ Y D Z ∈ ℝ * → Y D B C Y D Z ∈ ℝ *
34 13 19 17 33 syl3anc ⊢ φ → Y D B C Y D Z ∈ ℝ *
35 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ X ∧ Z ∈ X → B D Z ∈ ℝ *
36 4 6 9 35 syl3anc ⊢ φ → B D Z ∈ ℝ *
37 xmetsym ⊢ D ∈ ∞Met ⁡ X ∧ Y ∈ X ∧ B ∈ X → Y D B = B D Y
38 4 8 6 37 syl3anc ⊢ φ → Y D B = B D Y
39 xmetsym ⊢ D ∈ ∞Met ⁡ X ∧ Y ∈ X ∧ Z ∈ X → Y D Z = Z D Y
40 4 8 9 39 syl3anc ⊢ φ → Y D Z = Z D Y
41 38 40 oveq12d ⊢ φ → Y D B C Y D Z = B D Y C Z D Y
42 2 xmetrtri2 ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ X ∧ Z ∈ X ∧ Y ∈ X → B D Y C Z D Y ≤ B D Z
43 4 6 9 8 42 syl13anc ⊢ φ → B D Y C Z D Y ≤ B D Z
44 41 43 eqbrtrd ⊢ φ → Y D B C Y D Z ≤ B D Z
45 34 36 24 44 11 xrlelttrd ⊢ φ → Y D B C Y D Z < R 2
46 34 24 45 xrltled ⊢ φ → Y D B C Y D Z ≤ R 2
47 xmetlecl ⊢ C ∈ ∞Met ⁡ ℝ * ∧ Y D B ∈ ℝ * ∧ Y D Z ∈ ℝ * ∧ R 2 ∈ ℝ ∧ Y D B C Y D Z ≤ R 2 → Y D B C Y D Z ∈ ℝ
48 13 19 17 21 46 47 syl122anc ⊢ φ → Y D B C Y D Z ∈ ℝ
49 32 48 readdcld ⊢ φ → A D B C Y D B + Y D B C Y D Z ∈ ℝ
50 xmettri ⊢ C ∈ ∞Met ⁡ ℝ * ∧ A D B ∈ ℝ * ∧ Y D Z ∈ ℝ * ∧ Y D B ∈ ℝ * → A D B C Y D Z ≤ A D B C Y D B + 𝑒 Y D B C Y D Z
51 13 15 17 19 50 syl13anc ⊢ φ → A D B C Y D Z ≤ A D B C Y D B + 𝑒 Y D B C Y D Z
52 32 48 rexaddd ⊢ φ → A D B C Y D B + 𝑒 Y D B C Y D Z = A D B C Y D B + Y D B C Y D Z
53 51 52 breqtrd ⊢ φ → A D B C Y D Z ≤ A D B C Y D B + Y D B C Y D Z
54 xmetlecl ⊢ C ∈ ∞Met ⁡ ℝ * ∧ A D B ∈ ℝ * ∧ Y D Z ∈ ℝ * ∧ A D B C Y D B + Y D B C Y D Z ∈ ℝ ∧ A D B C Y D Z ≤ A D B C Y D B + Y D B C Y D Z → A D B C Y D Z ∈ ℝ
55 13 15 17 49 53 54 syl122anc ⊢ φ → A D B C Y D Z ∈ ℝ
56 7 rpred ⊢ φ → R ∈ ℝ
57 32 48 56 29 45 lt2halvesd ⊢ φ → A D B C Y D B + Y D B C Y D Z < R
58 55 49 56 53 57 lelttrd ⊢ φ → A D B C Y D Z < R