Metamath Proof Explorer


Theorem metdscnlem

Description: Lemma for metdscn . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f ⊒ 𝐹 = ( π‘₯ ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( π‘₯ 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
metdscn.c ⊒ 𝐢 = ( dist β€˜ ℝ*𝑠 )
metdscn.k ⊒ 𝐾 = ( MetOpen β€˜ 𝐢 )
metdscnlem.1 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
metdscnlem.2 ⊒ ( πœ‘ β†’ 𝑆 βŠ† 𝑋 )
metdscnlem.3 ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
metdscnlem.4 ⊒ ( πœ‘ β†’ 𝐡 ∈ 𝑋 )
metdscnlem.5 ⊒ ( πœ‘ β†’ 𝑅 ∈ ℝ+ )
metdscnlem.6 ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐡 ) < 𝑅 )
Assertion metdscnlem ( πœ‘ β†’ ( ( 𝐹 β€˜ 𝐴 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝐡 ) ) < 𝑅 )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊒ 𝐹 = ( π‘₯ ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( π‘₯ 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
3 metdscn.c ⊒ 𝐢 = ( dist β€˜ ℝ*𝑠 )
4 metdscn.k ⊒ 𝐾 = ( MetOpen β€˜ 𝐢 )
5 metdscnlem.1 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
6 metdscnlem.2 ⊒ ( πœ‘ β†’ 𝑆 βŠ† 𝑋 )
7 metdscnlem.3 ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
8 metdscnlem.4 ⊒ ( πœ‘ β†’ 𝐡 ∈ 𝑋 )
9 metdscnlem.5 ⊒ ( πœ‘ β†’ 𝑅 ∈ ℝ+ )
10 metdscnlem.6 ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐡 ) < 𝑅 )
11 1 metdsf ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ) β†’ 𝐹 : 𝑋 ⟢ ( 0 [,] +∞ ) )
12 5 6 11 syl2anc ⊒ ( πœ‘ β†’ 𝐹 : 𝑋 ⟢ ( 0 [,] +∞ ) )
13 12 7 ffvelcdmd ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) )
14 eliccxr ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* )
15 13 14 syl ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* )
16 12 8 ffvelcdmd ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐡 ) ∈ ( 0 [,] +∞ ) )
17 eliccxr ⊒ ( ( 𝐹 β€˜ 𝐡 ) ∈ ( 0 [,] +∞ ) β†’ ( 𝐹 β€˜ 𝐡 ) ∈ ℝ* )
18 16 17 syl ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐡 ) ∈ ℝ* )
19 18 xnegcld ⊒ ( πœ‘ β†’ -𝑒 ( 𝐹 β€˜ 𝐡 ) ∈ ℝ* )
20 15 19 xaddcld ⊒ ( πœ‘ β†’ ( ( 𝐹 β€˜ 𝐴 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝐡 ) ) ∈ ℝ* )
21 xmetcl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝐡 ) ∈ ℝ* )
22 5 7 8 21 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐡 ) ∈ ℝ* )
23 9 rpxrd ⊒ ( πœ‘ β†’ 𝑅 ∈ ℝ* )
24 1 metdstri ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) ) β†’ ( 𝐹 β€˜ 𝐴 ) ≀ ( ( 𝐴 𝐷 𝐡 ) +𝑒 ( 𝐹 β€˜ 𝐡 ) ) )
25 5 6 7 8 24 syl22anc ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐴 ) ≀ ( ( 𝐴 𝐷 𝐡 ) +𝑒 ( 𝐹 β€˜ 𝐡 ) ) )
26 elxrge0 ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* ∧ 0 ≀ ( 𝐹 β€˜ 𝐴 ) ) )
27 26 simprbi ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) β†’ 0 ≀ ( 𝐹 β€˜ 𝐴 ) )
28 13 27 syl ⊒ ( πœ‘ β†’ 0 ≀ ( 𝐹 β€˜ 𝐴 ) )
29 elxrge0 ⊒ ( ( 𝐹 β€˜ 𝐡 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 β€˜ 𝐡 ) ∈ ℝ* ∧ 0 ≀ ( 𝐹 β€˜ 𝐡 ) ) )
30 29 simprbi ⊒ ( ( 𝐹 β€˜ 𝐡 ) ∈ ( 0 [,] +∞ ) β†’ 0 ≀ ( 𝐹 β€˜ 𝐡 ) )
31 16 30 syl ⊒ ( πœ‘ β†’ 0 ≀ ( 𝐹 β€˜ 𝐡 ) )
32 ge0nemnf ⊒ ( ( ( 𝐹 β€˜ 𝐡 ) ∈ ℝ* ∧ 0 ≀ ( 𝐹 β€˜ 𝐡 ) ) β†’ ( 𝐹 β€˜ 𝐡 ) β‰  -∞ )
33 18 31 32 syl2anc ⊒ ( πœ‘ β†’ ( 𝐹 β€˜ 𝐡 ) β‰  -∞ )
34 xmetge0 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ 0 ≀ ( 𝐴 𝐷 𝐡 ) )
35 5 7 8 34 syl3anc ⊒ ( πœ‘ β†’ 0 ≀ ( 𝐴 𝐷 𝐡 ) )
36 xlesubadd ⊒ ( ( ( ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* ∧ ( 𝐹 β€˜ 𝐡 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐡 ) ∈ ℝ* ) ∧ ( 0 ≀ ( 𝐹 β€˜ 𝐴 ) ∧ ( 𝐹 β€˜ 𝐡 ) β‰  -∞ ∧ 0 ≀ ( 𝐴 𝐷 𝐡 ) ) ) β†’ ( ( ( 𝐹 β€˜ 𝐴 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝐡 ) ) ≀ ( 𝐴 𝐷 𝐡 ) ↔ ( 𝐹 β€˜ 𝐴 ) ≀ ( ( 𝐴 𝐷 𝐡 ) +𝑒 ( 𝐹 β€˜ 𝐡 ) ) ) )
37 15 18 22 28 33 35 36 syl33anc ⊒ ( πœ‘ β†’ ( ( ( 𝐹 β€˜ 𝐴 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝐡 ) ) ≀ ( 𝐴 𝐷 𝐡 ) ↔ ( 𝐹 β€˜ 𝐴 ) ≀ ( ( 𝐴 𝐷 𝐡 ) +𝑒 ( 𝐹 β€˜ 𝐡 ) ) ) )
38 25 37 mpbird ⊒ ( πœ‘ β†’ ( ( 𝐹 β€˜ 𝐴 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝐡 ) ) ≀ ( 𝐴 𝐷 𝐡 ) )
39 20 22 23 38 10 xrlelttrd ⊒ ( πœ‘ β†’ ( ( 𝐹 β€˜ 𝐴 ) +𝑒 -𝑒 ( 𝐹 β€˜ 𝐡 ) ) < 𝑅 )