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

Metamath Proof Explorer

Theorem metds0

Description: If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 1 metdsf ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 2 3adant3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
4 ssel2 ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
5 4 3adant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
6 3 5 ffvelcdmd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
7 eliccxr ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
8 6 7 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
9 8 xrleidd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) )
10 simp1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 simp2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 𝑆 ⊆ 𝑋 )
12 1 metdsge ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) )
13 10 11 5 8 12 syl31anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) )
14 9 13 mpbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ )
15 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ 𝑆 )
16 10 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 5 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ 𝑋 )
18 8 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
19 simpr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 0 < ( 𝐹 ‘ 𝐴 ) )
20 xblcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) ) → 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
21 16 17 18 19 20 syl112anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
22 inelcm ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ≠ ∅ )
23 15 21 22 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ≠ ∅ )
24 23 ex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 0 < ( 𝐹 ‘ 𝐴 ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ≠ ∅ ) )
25 24 necon2bd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ¬ 0 < ( 𝐹 ‘ 𝐴 ) ) )
26 14 25 mpd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ¬ 0 < ( 𝐹 ‘ 𝐴 ) )
27 elxrge0 ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝐴 ) ) )
28 27 simprbi ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
29 6 28 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
30 0xr ⊢ 0 ∈ ℝ*
31 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) ) )
32 30 8 31 sylancr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) ) )
33 29 32 mpbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) )
34 33 ord ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( ¬ 0 < ( 𝐹 ‘ 𝐴 ) → 0 = ( 𝐹 ‘ 𝐴 ) ) )
35 26 34 mpd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → 0 = ( 𝐹 ‘ 𝐴 ) )
36 35 eqcomd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 )