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 ffvelrnd ( 𝜑 → ( 𝐹𝐴 ) ∈ ( 0 [,] +∞ ) )
14 eliccxr ( ( 𝐹𝐴 ) ∈ ( 0 [,] +∞ ) → ( 𝐹𝐴 ) ∈ ℝ* )
15 13 14 syl ( 𝜑 → ( 𝐹𝐴 ) ∈ ℝ* )
16 12 8 ffvelrnd ( 𝜑 → ( 𝐹𝐵 ) ∈ ( 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 ( 𝜑 → ( ( 𝐹𝐴 ) +𝑒 -𝑒 ( 𝐹𝐵 ) ) < 𝑅 )