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 )

Metamath Proof Explorer

Theorem metds0

Proof