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

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 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝐵 ) ) < 𝑅 )