Metamath Proof Explorer

Theorem metdsle

Description: The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypothesis metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion metdsle ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
3 simpr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ 𝑋 )
4 3 sselda ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
5 4 adantrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
6 2 5 jca ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
7 1 metdstri ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) )
8 6 7 syldan ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) )
9 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
10 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
11 9 2 5 10 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
12 1 metds0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 )
13 12 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 )
14 13 adantrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) = 0 )
15 11 14 oveq12d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) )
16 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
17 9 5 2 16 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
18 17 xaddridd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐴 𝐷 𝐵 ) )
19 15 18 eqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 𝐷 𝐵 ) )
20 8 19 breqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) )