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

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
xmetdcn2.2 ⊢ 𝐶 = ( dist ‘ ℝ*𝑠 )
xmetdcn2.3 ⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
metdcn.d ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
metdcn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
metdcn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
metdcn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
metdcn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
metdcn.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
metdcn.4 ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑌 ) < ( 𝑅 / 2 ) )
metdcn.5 ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑍 ) < ( 𝑅 / 2 ) )
Assertion metdcnlem ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) < 𝑅 )

Proof

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