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	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	Assertion	metds0	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) = 0$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
3	2	3adant3	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F : X ⟶ [0, +∞]$
4		ssel2	$⊢ (S \subseteq X \land A \in S) \to A \in X$
5	4	3adant1	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to A \in X$
6	3 5	ffvelcdmd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) \in [0, +∞]$
7		eliccxr	$⊢ F (A) \in [0, +∞] \to F (A) \in ℝ^{*}$
8	6 7	syl	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) \in ℝ^{*}$
9	8	xrleidd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) \leq F (A)$
10		simp1	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to D \in ∞Met (X)$
11		simp2	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to S \subseteq X$
12	1	metdsge	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) \in ℝ^{*}) \to (F (A) \leq F (A) \leftrightarrow S \cap (A ball (D) F (A)) = \emptyset)$
13	10 11 5 8 12	syl31anc	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to (F (A) \leq F (A) \leftrightarrow S \cap (A ball (D) F (A)) = \emptyset)$
14	9 13	mpbid	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to S \cap (A ball (D) F (A)) = \emptyset$
15		simpl3	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to A \in S$
16	10	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to D \in ∞Met (X)$
17	5	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to A \in X$
18	8	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to F (A) \in ℝ^{*}$
19		simpr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to 0 < F (A)$
20		xblcntr	$⊢ (D \in ∞Met (X) \land A \in X \land (F (A) \in ℝ^{*} \land 0 < F (A))) \to A \in (A ball (D) F (A))$
21	16 17 18 19 20	syl112anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to A \in (A ball (D) F (A))$
22		inelcm	$⊢ (A \in S \land A \in (A ball (D) F (A))) \to S \cap (A ball (D) F (A)) \neq \emptyset$
23	15 21 22	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in S) \land 0 < F (A)) \to S \cap (A ball (D) F (A)) \neq \emptyset$
24	23	ex	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to (0 < F (A) \to S \cap (A ball (D) F (A)) \neq \emptyset)$
25	24	necon2bd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to (S \cap (A ball (D) F (A)) = \emptyset \to \neg 0 < F (A))$
26	14 25	mpd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to \neg 0 < F (A)$
27		elxrge0	$⊢ F (A) \in [0, +∞] \leftrightarrow (F (A) \in ℝ^{*} \land 0 \leq F (A))$
28	27	simprbi	$⊢ F (A) \in [0, +∞] \to 0 \leq F (A)$
29	6 28	syl	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to 0 \leq F (A)$
30		0xr	$⊢ 0 \in ℝ^{*}$
31		xrleloe	$⊢ (0 \in ℝ^{} \land F (A) \in ℝ^{}) \to (0 \leq F (A) \leftrightarrow (0 < F (A) \lor 0 = F (A)))$
32	30 8 31	sylancr	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to (0 \leq F (A) \leftrightarrow (0 < F (A) \lor 0 = F (A)))$
33	29 32	mpbid	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to (0 < F (A) \lor 0 = F (A))$
34	33	ord	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to (\neg 0 < F (A) \to 0 = F (A))$
35	26 34	mpd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to 0 = F (A)$
36	35	eqcomd	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) = 0$

Metamath Proof Explorer

Theorem metds0

Proof