metdscn

Description: The function F which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	metdscn.j	$⊢ J = MetOpen (D)$
	metdscn.c	$⊢ C = dist (ℝ_{𝑠}^{*})$
	metdscn.k	$⊢ K = MetOpen (C)$
Assertion	metdscn	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		metdscn.j	$⊢ J = MetOpen (D)$
3		metdscn.c	$⊢ C = dist (ℝ_{𝑠}^{*})$
4		metdscn.k	$⊢ K = MetOpen (C)$
5	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
6		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
7		fss	$⊢ (F : X ⟶ [0, +∞] \land [0, +∞] \subseteq ℝ^{}) \to F : X ⟶ ℝ^{}$
8	5 6 7	sylancl	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ ℝ^{*}$
9		simprr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \to r \in ℝ^{+}$
10	8	ad2antrr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F : X ⟶ ℝ^{*}$
11		simplrl	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to z \in X$
12	10 11	ffvelrnd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F (z) \in ℝ^{*}$
13		simprl	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to w \in X$
14	10 13	ffvelrnd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F (w) \in ℝ^{*}$
15	3	xrsdsval	$⊢ (F (z) \in ℝ^{} \land F (w) \in ℝ^{}) \to F (z) C F (w) = if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w)))$
16	12 14 15	syl2anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F (z) C F (w) = if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w)))$
17		simplll	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to D \in ∞Met (X)$
18		simpllr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to S \subseteq X$
19		simplrr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to r \in ℝ^{+}$
20		xmetsym	$⊢ (D \in ∞Met (X) \land w \in X \land z \in X) \to w D z = z D w$
21	17 13 11 20	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to w D z = z D w$
22		simprr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to z D w < r$
23	21 22	eqbrtrd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to w D z < r$
24	1 2 3 4 17 18 13 11 19 23	metdscnlem	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F (w) +_{𝑒} (- F (z)) < r$
25	1 2 3 4 17 18 11 13 19 22	metdscnlem	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F (z) +_{𝑒} (- F (w)) < r$
26		breq1	$⊢ F (w) +_{𝑒} (- F (z)) = if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w))) \to (F (w) +_{𝑒} (- F (z)) < r \leftrightarrow if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w))) < r)$
27		breq1	$⊢ F (z) +_{𝑒} (- F (w)) = if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w))) \to (F (z) +_{𝑒} (- F (w)) < r \leftrightarrow if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w))) < r)$
28	26 27	ifboth	$⊢ (F (w) +_{𝑒} (- F (z)) < r \land F (z) +_{𝑒} (- F (w)) < r) \to if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w))) < r$
29	24 25 28	syl2anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to if (F (z) \leq F (w), F (w) +_{𝑒} (- F (z)), F (z) +_{𝑒} (- F (w))) < r$
30	16 29	eqbrtrd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land (w \in X \land z D w < r)) \to F (z) C F (w) < r$
31	30	expr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \land w \in X) \to (z D w < r \to F (z) C F (w) < r)$
32	31	ralrimiva	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \to \forall w \in X (z D w < r \to F (z) C F (w) < r)$
33		breq2	$⊢ s = r \to (z D w < s \leftrightarrow z D w < r)$
34	33	rspceaimv	$⊢ (r \in ℝ^{+} \land \forall w \in X (z D w < r \to F (z) C F (w) < r)) \to \exists s \in ℝ^{+} \forall w \in X (z D w < s \to F (z) C F (w) < r)$
35	9 32 34	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (z \in X \land r \in ℝ^{+})) \to \exists s \in ℝ^{+} \forall w \in X (z D w < s \to F (z) C F (w) < r)$
36	35	ralrimivva	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to \forall z \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall w \in X (z D w < s \to F (z) C F (w) < r)$
37		simpl	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to D \in ∞Met (X)$
38	3	xrsxmet	$⊢ C \in ∞Met (ℝ^{*})$
39	2 4	metcn	$⊢ (D \in ∞Met (X) \land C \in ∞Met (ℝ^{})) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ ℝ^{} \land \forall z \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall w \in X (z D w < s \to F (z) C F (w) < r)))$
40	37 38 39	sylancl	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ ℝ^{*} \land \forall z \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall w \in X (z D w < s \to F (z) C F (w) < r)))$
41	8 36 40	mpbir2and	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F \in (J Cn K)$

Metamath Proof Explorer

Theorem metdscn

Proof