Theorem 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	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	xmetdcn2.2	⊢ 𝐶 = ( dist ‘ ℝ*𝑠 )
	xmetdcn2.3	⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
	metdcn.d	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
	metdcn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	metdcn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
	metdcn.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
	metdcn.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	metdcn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
	metdcn.4	⊢ ( 𝜑 → ( 𝐴 𝐷 𝑌 ) < ( 𝑅 / 2 ) )
	metdcn.5	⊢ ( 𝜑 → ( 𝐵 𝐷 𝑍 ) < ( 𝑅 / 2 ) )
Assertion	metdcnlem	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) < 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		xmetdcn2.2	⊢ 𝐶 = ( dist ‘ ℝ*𝑠 )
3		xmetdcn2.3	⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
4		metdcn.d	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5		metdcn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
6		metdcn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
7		metdcn.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
8		metdcn.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
9		metdcn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
10		metdcn.4	⊢ ( 𝜑 → ( 𝐴 𝐷 𝑌 ) < ( 𝑅 / 2 ) )
11		metdcn.5	⊢ ( 𝜑 → ( 𝐵 𝐷 𝑍 ) < ( 𝑅 / 2 ) )
12	2	xrsxmet	⊢ 𝐶 ∈ ( ∞Met ‘ ℝ* )
13	12	a1i	⊢ ( 𝜑 → 𝐶 ∈ ( ∞Met ‘ ℝ* ) )
14		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
15	4 5 6 14	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
16		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝑌 𝐷 𝑍 ) ∈ ℝ* )
17	4 8 9 16	syl3anc	⊢ ( 𝜑 → ( 𝑌 𝐷 𝑍 ) ∈ ℝ* )
18		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑌 𝐷 𝐵 ) ∈ ℝ* )
19	4 8 6 18	syl3anc	⊢ ( 𝜑 → ( 𝑌 𝐷 𝐵 ) ∈ ℝ* )
20	7	rphalfcld	⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ+ )
21	20	rpred	⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ )
22		xmetcl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ℝ* ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝐵 ) ∈ ℝ* ) → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ∈ ℝ* )
23	13 15 19 22	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ∈ ℝ* )
24	20	rpxrd	⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ* )
25		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑌 ) ∈ ℝ* )
26	4 5 8 25	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐷 𝑌 ) ∈ ℝ* )
27	2	xmetrtri2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ≤ ( 𝐴 𝐷 𝑌 ) )
28	4 5 8 6 27	syl13anc	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ≤ ( 𝐴 𝐷 𝑌 ) )
29	23 26 24 28 10	xrlelttrd	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) < ( 𝑅 / 2 ) )
30	23 24 29	xrltled	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ≤ ( 𝑅 / 2 ) )
31		xmetlecl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ℝ* ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝐵 ) ∈ ℝ* ) ∧ ( ( 𝑅 / 2 ) ∈ ℝ ∧ ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ≤ ( 𝑅 / 2 ) ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ∈ ℝ )
32	13 15 19 21 30 31	syl122anc	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) ∈ ℝ )
33		xmetcl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ℝ* ) ∧ ( 𝑌 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝑍 ) ∈ ℝ* ) → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ∈ ℝ* )
34	13 19 17 33	syl3anc	⊢ ( 𝜑 → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ∈ ℝ* )
35		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐵 𝐷 𝑍 ) ∈ ℝ* )
36	4 6 9 35	syl3anc	⊢ ( 𝜑 → ( 𝐵 𝐷 𝑍 ) ∈ ℝ* )
37		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑌 𝐷 𝐵 ) = ( 𝐵 𝐷 𝑌 ) )
38	4 8 6 37	syl3anc	⊢ ( 𝜑 → ( 𝑌 𝐷 𝐵 ) = ( 𝐵 𝐷 𝑌 ) )
39		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝑌 𝐷 𝑍 ) = ( 𝑍 𝐷 𝑌 ) )
40	4 8 9 39	syl3anc	⊢ ( 𝜑 → ( 𝑌 𝐷 𝑍 ) = ( 𝑍 𝐷 𝑌 ) )
41	38 40	oveq12d	⊢ ( 𝜑 → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) = ( ( 𝐵 𝐷 𝑌 ) 𝐶 ( 𝑍 𝐷 𝑌 ) ) )
42	2	xmetrtri2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) ) → ( ( 𝐵 𝐷 𝑌 ) 𝐶 ( 𝑍 𝐷 𝑌 ) ) ≤ ( 𝐵 𝐷 𝑍 ) )
43	4 6 9 8 42	syl13anc	⊢ ( 𝜑 → ( ( 𝐵 𝐷 𝑌 ) 𝐶 ( 𝑍 𝐷 𝑌 ) ) ≤ ( 𝐵 𝐷 𝑍 ) )
44	41 43	eqbrtrd	⊢ ( 𝜑 → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( 𝐵 𝐷 𝑍 ) )
45	34 36 24 44 11	xrlelttrd	⊢ ( 𝜑 → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) < ( 𝑅 / 2 ) )
46	34 24 45	xrltled	⊢ ( 𝜑 → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( 𝑅 / 2 ) )
47		xmetlecl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ℝ* ) ∧ ( ( 𝑌 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝑍 ) ∈ ℝ* ) ∧ ( ( 𝑅 / 2 ) ∈ ℝ ∧ ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( 𝑅 / 2 ) ) ) → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ∈ ℝ )
48	13 19 17 21 46 47	syl122anc	⊢ ( 𝜑 → ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ∈ ℝ )
49	32 48	readdcld	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) + ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) ∈ ℝ )
50		xmettri	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ℝ* ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝑍 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝐵 ) ∈ ℝ* ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) +𝑒 ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) )
51	13 15 17 19 50	syl13anc	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) +𝑒 ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) )
52	32 48	rexaddd	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) +𝑒 ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) = ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) + ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) )
53	51 52	breqtrd	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) + ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) )
54		xmetlecl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ℝ* ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝑌 𝐷 𝑍 ) ∈ ℝ* ) ∧ ( ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) + ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) ∈ ℝ ∧ ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ≤ ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) + ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ∈ ℝ )
55	13 15 17 49 53 54	syl122anc	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ∈ ℝ )
56	7	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
57	32 48 56 29 45	lt2halvesd	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝐵 ) ) + ( ( 𝑌 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) ) < 𝑅 )
58	55 49 56 53 57	lelttrd	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐵 ) 𝐶 ( 𝑌 𝐷 𝑍 ) ) < 𝑅 )