xrsxmet

Description: The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015)

		Ref	Expression
	Hypothesis	xrsxmet.1	$⊢ D = dist (ℝ_{𝑠}^{*})$
	Assertion	xrsxmet	$⊢ D \in ∞Met (ℝ^{*})$

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	$⊢ D = dist (ℝ_{𝑠}^{*})$
2		xrex	$⊢ ℝ^{*} \in V$
3	2	a1i	$⊢ ⊤ \to ℝ^{*} \in V$
4		id	$⊢ y \in ℝ^{} \to y \in ℝ^{}$
5		xnegcl	$⊢ x \in ℝ^{} \to - x \in ℝ^{}$
6		xaddcl	$⊢ (y \in ℝ^{} \land - x \in ℝ^{}) \to y +_{𝑒} (- x) \in ℝ^{*}$
7	4 5 6	syl2anr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to y +_{𝑒} (- x) \in ℝ^{*}$
8		xnegcl	$⊢ y \in ℝ^{} \to - y \in ℝ^{}$
9		xaddcl	$⊢ (x \in ℝ^{} \land - y \in ℝ^{}) \to x +_{𝑒} (- y) \in ℝ^{*}$
10	8 9	sylan2	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x +_{𝑒} (- y) \in ℝ^{*}$
11	7 10	ifcld	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \in ℝ^{*}$
12	11	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \in ℝ^{*}$
13	1	xrsds	$⊢ D = (x \in ℝ^{}, y \in ℝ^{} ⟼ if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)))$
14	13	fmpo	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \in ℝ^{} \leftrightarrow D : ℝ^{} \times ℝ^{} ⟶ ℝ^{}$
15	12 14	mpbi	$⊢ D : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$
16	15	a1i	$⊢ ⊤ \to D : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$
17		breq2	$⊢ y +_{𝑒} (- x) = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \to (0 \leq y +_{𝑒} (- x) \leftrightarrow 0 \leq if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)))$
18		breq2	$⊢ x +_{𝑒} (- y) = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \to (0 \leq x +_{𝑒} (- y) \leftrightarrow 0 \leq if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)))$
19		xsubge0	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to (0 \leq y +_{𝑒} (- x) \leftrightarrow x \leq y)$
20	19	ancoms	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (0 \leq y +_{𝑒} (- x) \leftrightarrow x \leq y)$
21	20	biimpar	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \leq y) \to 0 \leq y +_{𝑒} (- x)$
22		xrletri	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \lor y \leq x)$
23	22	orcanai	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land \neg x \leq y) \to y \leq x$
24		xsubge0	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (0 \leq x +_{𝑒} (- y) \leftrightarrow y \leq x)$
25	24	biimpar	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land y \leq x) \to 0 \leq x +_{𝑒} (- y)$
26	23 25	syldan	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land \neg x \leq y) \to 0 \leq x +_{𝑒} (- y)$
27	17 18 21 26	ifbothda	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to 0 \leq if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y))$
28	1	xrsdsval	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x D y = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y))$
29	27 28	breqtrrd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to 0 \leq x D y$
30	29	adantl	$⊢ (⊤ \land (x \in ℝ^{} \land y \in ℝ^{})) \to 0 \leq x D y$
31	29	biantrud	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x D y \leq 0 \leftrightarrow (x D y \leq 0 \land 0 \leq x D y))$
32	28 11	eqeltrd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x D y \in ℝ^{*}$
33		0xr	$⊢ 0 \in ℝ^{*}$
34		xrletri3	$⊢ (x D y \in ℝ^{} \land 0 \in ℝ^{}) \to (x D y = 0 \leftrightarrow (x D y \leq 0 \land 0 \leq x D y))$
35	32 33 34	sylancl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x D y = 0 \leftrightarrow (x D y \leq 0 \land 0 \leq x D y))$
36		simpr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x = y) \to x = y$
37		simplr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x D y = 0$
38		0re	$⊢ 0 \in ℝ$
39	37 38	eqeltrdi	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x D y \in ℝ$
40	1	xrsdsreclb	$⊢ (x \in ℝ^{} \land y \in ℝ^{} \land x \neq y) \to (x D y \in ℝ \leftrightarrow (x \in ℝ \land y \in ℝ))$
41	40	ad4ant124	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to (x D y \in ℝ \leftrightarrow (x \in ℝ \land y \in ℝ))$
42	39 41	mpbid	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to (x \in ℝ \land y \in ℝ)$
43	42	simpld	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x \in ℝ$
44	43	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x \in ℂ$
45	42	simprd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to y \in ℝ$
46	45	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to y \in ℂ$
47		rexsub	$⊢ (x \in ℝ \land y \in ℝ) \to x +_{𝑒} (- y) = x - y$
48	42 47	syl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x +_{𝑒} (- y) = x - y$
49	28	eqeq1d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x D y = 0 \leftrightarrow if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0)$
50	49	biimpa	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \to if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0$
51	50	adantr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0$
52		xneg11	$⊢ (y +_{𝑒} (- x) \in ℝ^{} \land 0 \in ℝ^{}) \to (- (y +_{𝑒} (- x)) = - 0 \leftrightarrow y +_{𝑒} (- x) = 0)$
53	7 33 52	sylancl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (- (y +_{𝑒} (- x)) = - 0 \leftrightarrow y +_{𝑒} (- x) = 0)$
54		simpr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to y \in ℝ^{*}$
55	5	adantr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to - x \in ℝ^{*}$
56		xnegdi	$⊢ (y \in ℝ^{} \land - x \in ℝ^{}) \to - (y +_{𝑒} (- x)) = (- y) +_{𝑒} (- (- x))$
57	54 55 56	syl2anc	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to - (y +_{𝑒} (- x)) = (- y) +_{𝑒} (- (- x))$
58		xnegneg	$⊢ x \in ℝ^{*} \to - (- x) = x$
59	58	adantr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to - (- x) = x$
60	59	oveq2d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (- y) +_{𝑒} (- (- x)) = (- y) +_{𝑒} x$
61	8	adantl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to - y \in ℝ^{*}$
62		simpl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x \in ℝ^{*}$
63		xaddcom	$⊢ (- y \in ℝ^{} \land x \in ℝ^{}) \to (- y) +_{𝑒} x = x +_{𝑒} (- y)$
64	61 62 63	syl2anc	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (- y) +_{𝑒} x = x +_{𝑒} (- y)$
65	57 60 64	3eqtrd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to - (y +_{𝑒} (- x)) = x +_{𝑒} (- y)$
66		xneg0	$⊢ - 0 = 0$
67	66	a1i	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to - 0 = 0$
68	65 67	eqeq12d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (- (y +_{𝑒} (- x)) = - 0 \leftrightarrow x +_{𝑒} (- y) = 0)$
69	53 68	bitr3d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y +_{𝑒} (- x) = 0 \leftrightarrow x +_{𝑒} (- y) = 0)$
70	69	ad2antrr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to (y +_{𝑒} (- x) = 0 \leftrightarrow x +_{𝑒} (- y) = 0)$
71		biidd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to (x +_{𝑒} (- y) = 0 \leftrightarrow x +_{𝑒} (- y) = 0)$
72		eqeq1	$⊢ y +_{𝑒} (- x) = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \to (y +_{𝑒} (- x) = 0 \leftrightarrow if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0)$
73	72	bibi1d	$⊢ y +_{𝑒} (- x) = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \to ((y +_{𝑒} (- x) = 0 \leftrightarrow x +_{𝑒} (- y) = 0) \leftrightarrow (if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0 \leftrightarrow x +_{𝑒} (- y) = 0))$
74		eqeq1	$⊢ x +_{𝑒} (- y) = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \to (x +_{𝑒} (- y) = 0 \leftrightarrow if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0)$
75	74	bibi1d	$⊢ x +_{𝑒} (- y) = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) \to ((x +_{𝑒} (- y) = 0 \leftrightarrow x +_{𝑒} (- y) = 0) \leftrightarrow (if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0 \leftrightarrow x +_{𝑒} (- y) = 0))$
76	73 75	ifboth	$⊢ ((y +_{𝑒} (- x) = 0 \leftrightarrow x +_{𝑒} (- y) = 0) \land (x +_{𝑒} (- y) = 0 \leftrightarrow x +_{𝑒} (- y) = 0)) \to (if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0 \leftrightarrow x +_{𝑒} (- y) = 0)$
77	70 71 76	syl2anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to (if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = 0 \leftrightarrow x +_{𝑒} (- y) = 0)$
78	51 77	mpbid	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x +_{𝑒} (- y) = 0$
79	48 78	eqtr3d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x - y = 0$
80	44 46 79	subeq0d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \land x \neq y) \to x = y$
81	36 80	pm2.61dane	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x D y = 0) \to x = y$
82	81	ex	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x D y = 0 \to x = y)$
83	1	xrsdsval	$⊢ (y \in ℝ^{} \land y \in ℝ^{}) \to y D y = if (y \leq y, y +_{𝑒} (- y), y +_{𝑒} (- y))$
84	83	anidms	$⊢ y \in ℝ^{*} \to y D y = if (y \leq y, y +_{𝑒} (- y), y +_{𝑒} (- y))$
85		xrleid	$⊢ y \in ℝ^{*} \to y \leq y$
86	85	iftrued	$⊢ y \in ℝ^{*} \to if (y \leq y, y +_{𝑒} (- y), y +_{𝑒} (- y)) = y +_{𝑒} (- y)$
87		xnegid	$⊢ y \in ℝ^{*} \to y +_{𝑒} (- y) = 0$
88	84 86 87	3eqtrd	$⊢ y \in ℝ^{*} \to y D y = 0$
89	88	adantl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to y D y = 0$
90		oveq1	$⊢ x = y \to x D y = y D y$
91	90	eqeq1d	$⊢ x = y \to (x D y = 0 \leftrightarrow y D y = 0)$
92	89 91	syl5ibrcom	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x = y \to x D y = 0)$
93	82 92	impbid	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x D y = 0 \leftrightarrow x = y)$
94	31 35 93	3bitr2d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x D y \leq 0 \leftrightarrow x = y)$
95	94	adantl	$⊢ (⊤ \land (x \in ℝ^{} \land y \in ℝ^{})) \to (x D y \leq 0 \leftrightarrow x = y)$
96		simplrr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D y \in ℝ$
97	96	leidd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D y \leq z D y$
98		simpr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z = x$
99	98	oveq1d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D y = x D y$
100	98	oveq1d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D x = x D x$
101		simpll1	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to x \in ℝ^{}$
102		oveq12	$⊢ (y = x \land y = x) \to y D y = x D x$
103	102	anidms	$⊢ y = x \to y D y = x D x$
104	103	eqeq1d	$⊢ y = x \to (y D y = 0 \leftrightarrow x D x = 0)$
105	104 88	vtoclga	$⊢ x \in ℝ^{*} \to x D x = 0$
106	101 105	syl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to x D x = 0$
107	100 106	eqtrd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D x = 0$
108	107	oveq1d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to (z D x) + (z D y) = 0 + (z D y)$
109	96	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D y \in ℂ$
110	109	addlidd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to 0 + (z D y) = z D y$
111	108 110	eqtr2d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to z D y = (z D x) + (z D y)$
112	97 99 111	3brtr3d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = x) \to x D y \leq (z D x) + (z D y)$
113		simpr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to z = y$
114	113	oveq1d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to z D x = y D x$
115		simplrl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to z D x \in ℝ$
116	114 115	eqeltrrd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to y D x \in ℝ$
117	116	leidd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to y D x \leq y D x$
118		simpll1	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to x \in ℝ^{}$
119		simpll2	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to y \in ℝ^{}$
120		oveq2	$⊢ x = y \to y D x = y D y$
121	90 120	eqtr4d	$⊢ x = y \to x D y = y D x$
122	121	adantl	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x = y) \to x D y = y D x$
123		eqeq2	$⊢ x +_{𝑒} (- y) = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x)) \to (if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = x +_{𝑒} (- y) \leftrightarrow if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x)))$
124		eqeq2	$⊢ y +_{𝑒} (- x) = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x)) \to (if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = y +_{𝑒} (- x) \leftrightarrow if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x)))$
125		xrleloe	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \leftrightarrow (x < y \lor x = y))$
126	125	adantr	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to (x \leq y \leftrightarrow (x < y \lor x = y))$
127		simpr	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to x \neq y$
128	127	neneqd	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to \neg x = y$
129		biorf	$⊢ \neg x = y \to (x < y \leftrightarrow (x = y \lor x < y))$
130		orcom	$⊢ (x = y \lor x < y) \leftrightarrow (x < y \lor x = y)$
131	129 130	bitrdi	$⊢ \neg x = y \to (x < y \leftrightarrow (x < y \lor x = y))$
132	128 131	syl	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to (x < y \leftrightarrow (x < y \lor x = y))$
133		xrltnle	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x < y \leftrightarrow \neg y \leq x)$
134	133	adantr	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to (x < y \leftrightarrow \neg y \leq x)$
135	126 132 134	3bitr2d	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to (x \leq y \leftrightarrow \neg y \leq x)$
136	135	con2bid	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to (y \leq x \leftrightarrow \neg x \leq y)$
137	136	biimpa	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \land y \leq x) \to \neg x \leq y$
138	137	iffalsed	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \land y \leq x) \to if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = x +_{𝑒} (- y)$
139	135	biimpar	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \land \neg y \leq x) \to x \leq y$
140	139	iftrued	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \land \neg y \leq x) \to if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = y +_{𝑒} (- x)$
141	123 124 138 140	ifbothda	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y)) = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x))$
142	28	adantr	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to x D y = if (x \leq y, y +_{𝑒} (- x), x +_{𝑒} (- y))$
143	1	xrsdsval	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to y D x = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x))$
144	143	ancoms	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to y D x = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x))$
145	144	adantr	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to y D x = if (y \leq x, x +_{𝑒} (- y), y +_{𝑒} (- x))$
146	141 142 145	3eqtr4d	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x \neq y) \to x D y = y D x$
147	122 146	pm2.61dane	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x D y = y D x$
148	118 119 147	syl2anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to x D y = y D x$
149	113	oveq1d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to z D y = y D y$
150	119 88	syl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to y D y = 0$
151	149 150	eqtrd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to z D y = 0$
152	114 151	oveq12d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to (z D x) + (z D y) = (y D x) + 0$
153	116	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to y D x \in ℂ$
154	153	addridd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to (y D x) + 0 = y D x$
155	152 154	eqtrd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to (z D x) + (z D y) = y D x$
156	117 148 155	3brtr4d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land z = y) \to x D y \leq (z D x) + (z D y)$
157		simplrl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z D x \in ℝ$
158		simpll3	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z \in ℝ^{}$
159		simpll1	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to x \in ℝ^{}$
160		simprl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z \neq x$
161	1	xrsdsreclb	$⊢ (z \in ℝ^{} \land x \in ℝ^{} \land z \neq x) \to (z D x \in ℝ \leftrightarrow (z \in ℝ \land x \in ℝ))$
162	158 159 160 161	syl3anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to (z D x \in ℝ \leftrightarrow (z \in ℝ \land x \in ℝ))$
163	157 162	mpbid	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to (z \in ℝ \land x \in ℝ)$
164	163	simprd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to x \in ℝ$
165	164	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to x \in ℂ$
166		simplrr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z D y \in ℝ$
167		simpll2	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to y \in ℝ^{}$
168		simprr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z \neq y$
169	1	xrsdsreclb	$⊢ (z \in ℝ^{} \land y \in ℝ^{} \land z \neq y) \to (z D y \in ℝ \leftrightarrow (z \in ℝ \land y \in ℝ))$
170	158 167 168 169	syl3anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to (z D y \in ℝ \leftrightarrow (z \in ℝ \land y \in ℝ))$
171	166 170	mpbid	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to (z \in ℝ \land y \in ℝ)$
172	171	simprd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to y \in ℝ$
173	172	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to y \in ℂ$
174	163	simpld	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z \in ℝ$
175	174	recnd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z \in ℂ$
176	165 173 175	abs3difd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to \|x - y\| \leq \|x - z\| + \|z - y\|$
177	1	xrsdsreval	$⊢ (x \in ℝ \land y \in ℝ) \to x D y = \|x - y\|$
178	164 172 177	syl2anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to x D y = \|x - y\|$
179	1	xrsdsreval	$⊢ (z \in ℝ \land x \in ℝ) \to z D x = \|z - x\|$
180	163 179	syl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z D x = \|z - x\|$
181	175 165	abssubd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to \|z - x\| = \|x - z\|$
182	180 181	eqtrd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z D x = \|x - z\|$
183	1	xrsdsreval	$⊢ (z \in ℝ \land y \in ℝ) \to z D y = \|z - y\|$
184	171 183	syl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to z D y = \|z - y\|$
185	182 184	oveq12d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to (z D x) + (z D y) = \|x - z\| + \|z - y\|$
186	176 178 185	3brtr4d	$⊢ (((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \land (z \neq x \land z \neq y)) \to x D y \leq (z D x) + (z D y)$
187	112 156 186	pm2.61da2ne	$⊢ ((x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \to x D y \leq (z D x) + (z D y)$
188	187	3adant1	$⊢ (⊤ \land (x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \land (z D x \in ℝ \land z D y \in ℝ)) \to x D y \leq (z D x) + (z D y)$
189	3 16 30 95 188	isxmet2d	$⊢ ⊤ \to D \in ∞Met (ℝ^{*})$
190	189	mptru	$⊢ D \in ∞Met (ℝ^{*})$

Metamath Proof Explorer

Theorem xrsxmet

Proof