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 ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐡 ) 𝐢 ( π‘Œ 𝐷 𝑍 ) ) < 𝑅 )