metdcnlem

Description: The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	xmetdcn2.1	$⊢ J = MetOpen (D)$
	xmetdcn2.2	$⊢ C = dist (ℝ_{𝑠}^{*})$
	xmetdcn2.3	$⊢ K = MetOpen (C)$
	metdcn.d	$⊢ φ \to D \in ∞Met (X)$
	metdcn.a	$⊢ φ \to A \in X$
	metdcn.b	$⊢ φ \to B \in X$
	metdcn.r	$⊢ φ \to R \in ℝ^{+}$
	metdcn.y	$⊢ φ \to Y \in X$
	metdcn.z	$⊢ φ \to Z \in X$
	metdcn.4	$⊢ φ \to A D Y < \frac{R}{2}$
	metdcn.5	$⊢ φ \to B D Z < \frac{R}{2}$
Assertion	metdcnlem	$⊢ φ \to (A D B) C (Y D Z) < R$

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	$⊢ J = MetOpen (D)$
2		xmetdcn2.2	$⊢ C = dist (ℝ_{𝑠}^{*})$
3		xmetdcn2.3	$⊢ K = MetOpen (C)$
4		metdcn.d	$⊢ φ \to D \in ∞Met (X)$
5		metdcn.a	$⊢ φ \to A \in X$
6		metdcn.b	$⊢ φ \to B \in X$
7		metdcn.r	$⊢ φ \to R \in ℝ^{+}$
8		metdcn.y	$⊢ φ \to Y \in X$
9		metdcn.z	$⊢ φ \to Z \in X$
10		metdcn.4	$⊢ φ \to A D Y < \frac{R}{2}$
11		metdcn.5	$⊢ φ \to B D Z < \frac{R}{2}$
12	2	xrsxmet	$⊢ C \in ∞Met (ℝ^{*})$
13	12	a1i	$⊢ φ \to C \in ∞Met (ℝ^{*})$
14		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B \in ℝ^{*}$
15	4 5 6 14	syl3anc	$⊢ φ \to A D B \in ℝ^{*}$
16		xmetcl	$⊢ (D \in ∞Met (X) \land Y \in X \land Z \in X) \to Y D Z \in ℝ^{*}$
17	4 8 9 16	syl3anc	$⊢ φ \to Y D Z \in ℝ^{*}$
18		xmetcl	$⊢ (D \in ∞Met (X) \land Y \in X \land B \in X) \to Y D B \in ℝ^{*}$
19	4 8 6 18	syl3anc	$⊢ φ \to Y D B \in ℝ^{*}$
20	7	rphalfcld	$⊢ φ \to \frac{R}{2} \in ℝ^{+}$
21	20	rpred	$⊢ φ \to \frac{R}{2} \in ℝ$
22		xmetcl	$⊢ (C \in ∞Met (ℝ^{}) \land A D B \in ℝ^{} \land Y D B \in ℝ^{}) \to (A D B) C (Y D B) \in ℝ^{}$
23	13 15 19 22	syl3anc	$⊢ φ \to (A D B) C (Y D B) \in ℝ^{*}$
24	20	rpxrd	$⊢ φ \to \frac{R}{2} \in ℝ^{*}$
25		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land Y \in X) \to A D Y \in ℝ^{*}$
26	4 5 8 25	syl3anc	$⊢ φ \to A D Y \in ℝ^{*}$
27	2	xmetrtri2	$⊢ (D \in ∞Met (X) \land (A \in X \land Y \in X \land B \in X)) \to (A D B) C (Y D B) \leq A D Y$
28	4 5 8 6 27	syl13anc	$⊢ φ \to (A D B) C (Y D B) \leq A D Y$
29	23 26 24 28 10	xrlelttrd	$⊢ φ \to (A D B) C (Y D B) < \frac{R}{2}$
30	23 24 29	xrltled	$⊢ φ \to (A D B) C (Y D B) \leq \frac{R}{2}$
31		xmetlecl	$⊢ (C \in ∞Met (ℝ^{}) \land (A D B \in ℝ^{} \land Y D B \in ℝ^{*}) \land (\frac{R}{2} \in ℝ \land (A D B) C (Y D B) \leq \frac{R}{2})) \to (A D B) C (Y D B) \in ℝ$
32	13 15 19 21 30 31	syl122anc	$⊢ φ \to (A D B) C (Y D B) \in ℝ$
33		xmetcl	$⊢ (C \in ∞Met (ℝ^{}) \land Y D B \in ℝ^{} \land Y D Z \in ℝ^{}) \to (Y D B) C (Y D Z) \in ℝ^{}$
34	13 19 17 33	syl3anc	$⊢ φ \to (Y D B) C (Y D Z) \in ℝ^{*}$
35		xmetcl	$⊢ (D \in ∞Met (X) \land B \in X \land Z \in X) \to B D Z \in ℝ^{*}$
36	4 6 9 35	syl3anc	$⊢ φ \to B D Z \in ℝ^{*}$
37		xmetsym	$⊢ (D \in ∞Met (X) \land Y \in X \land B \in X) \to Y D B = B D Y$
38	4 8 6 37	syl3anc	$⊢ φ \to Y D B = B D Y$
39		xmetsym	$⊢ (D \in ∞Met (X) \land Y \in X \land Z \in X) \to Y D Z = Z D Y$
40	4 8 9 39	syl3anc	$⊢ φ \to Y D Z = Z D Y$
41	38 40	oveq12d	$⊢ φ \to (Y D B) C (Y D Z) = (B D Y) C (Z D Y)$
42	2	xmetrtri2	$⊢ (D \in ∞Met (X) \land (B \in X \land Z \in X \land Y \in X)) \to (B D Y) C (Z D Y) \leq B D Z$
43	4 6 9 8 42	syl13anc	$⊢ φ \to (B D Y) C (Z D Y) \leq B D Z$
44	41 43	eqbrtrd	$⊢ φ \to (Y D B) C (Y D Z) \leq B D Z$
45	34 36 24 44 11	xrlelttrd	$⊢ φ \to (Y D B) C (Y D Z) < \frac{R}{2}$
46	34 24 45	xrltled	$⊢ φ \to (Y D B) C (Y D Z) \leq \frac{R}{2}$
47		xmetlecl	$⊢ (C \in ∞Met (ℝ^{}) \land (Y D B \in ℝ^{} \land Y D Z \in ℝ^{*}) \land (\frac{R}{2} \in ℝ \land (Y D B) C (Y D Z) \leq \frac{R}{2})) \to (Y D B) C (Y D Z) \in ℝ$
48	13 19 17 21 46 47	syl122anc	$⊢ φ \to (Y D B) C (Y D Z) \in ℝ$
49	32 48	readdcld	$⊢ φ \to ((A D B) C (Y D B)) + ((Y D B) C (Y D Z)) \in ℝ$
50		xmettri	$⊢ (C \in ∞Met (ℝ^{}) \land (A D B \in ℝ^{} \land Y D Z \in ℝ^{} \land Y D B \in ℝ^{})) \to (A D B) C (Y D Z) \leq ((A D B) C (Y D B)) +_{𝑒} ((Y D B) C (Y D Z))$
51	13 15 17 19 50	syl13anc	$⊢ φ \to (A D B) C (Y D Z) \leq ((A D B) C (Y D B)) +_{𝑒} ((Y D B) C (Y D Z))$
52	32 48	rexaddd	$⊢ φ \to ((A D B) C (Y D B)) +_{𝑒} ((Y D B) C (Y D Z)) = ((A D B) C (Y D B)) + ((Y D B) C (Y D Z))$
53	51 52	breqtrd	$⊢ φ \to (A D B) C (Y D Z) \leq ((A D B) C (Y D B)) + ((Y D B) C (Y D Z))$
54		xmetlecl	$⊢ (C \in ∞Met (ℝ^{}) \land (A D B \in ℝ^{} \land Y D Z \in ℝ^{*}) \land (((A D B) C (Y D B)) + ((Y D B) C (Y D Z)) \in ℝ \land (A D B) C (Y D Z) \leq ((A D B) C (Y D B)) + ((Y D B) C (Y D Z)))) \to (A D B) C (Y D Z) \in ℝ$
55	13 15 17 49 53 54	syl122anc	$⊢ φ \to (A D B) C (Y D Z) \in ℝ$
56	7	rpred	$⊢ φ \to R \in ℝ$
57	32 48 56 29 45	lt2halvesd	$⊢ φ \to ((A D B) C (Y D B)) + ((Y D B) C (Y D Z)) < R$
58	55 49 56 53 57	lelttrd	$⊢ φ \to (A D B) C (Y D Z) < R$

Metamath Proof Explorer

Theorem metdcnlem

Proof