isxmet2d

Description: It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypotheses	isxmetd.0	$⊢ φ \to X \in V$
	isxmetd.1	$⊢ φ \to D : X \times X ⟶ ℝ^{*}$
	isxmet2d.2	$⊢ (φ \land (x \in X \land y \in X)) \to 0 \leq x D y$
	isxmet2d.3	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y \leq 0 \leftrightarrow x = y)$
	isxmet2d.4	$⊢ (φ \land (x \in X \land y \in X \land z \in X) \land (z D x \in ℝ \land z D y \in ℝ)) \to x D y \leq (z D x) + (z D y)$
Assertion	isxmet2d	$⊢ φ \to D \in ∞Met (X)$

Proof

Step	Hyp	Ref	Expression
1		isxmetd.0	$⊢ φ \to X \in V$
2		isxmetd.1	$⊢ φ \to D : X \times X ⟶ ℝ^{*}$
3		isxmet2d.2	$⊢ (φ \land (x \in X \land y \in X)) \to 0 \leq x D y$
4		isxmet2d.3	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y \leq 0 \leftrightarrow x = y)$
5		isxmet2d.4	$⊢ (φ \land (x \in X \land y \in X \land z \in X) \land (z D x \in ℝ \land z D y \in ℝ)) \to x D y \leq (z D x) + (z D y)$
6	2	fovrnda	$⊢ (φ \land (x \in X \land y \in X)) \to x D y \in ℝ^{*}$
7		0xr	$⊢ 0 \in ℝ^{*}$
8		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))$
9	6 7 8	sylancl	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow (x D y \leq 0 \land 0 \leq x D y))$
10	3	biantrud	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y \leq 0 \leftrightarrow (x D y \leq 0 \land 0 \leq x D y))$
11	9 10 4	3bitr2d	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow x = y)$
12	5	3expa	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land (z D x \in ℝ \land z D y \in ℝ)) \to x D y \leq (z D x) + (z D y)$
13		rexadd	$⊢ (z D x \in ℝ \land z D y \in ℝ) \to (z D x) +_{𝑒} (z D y) = (z D x) + (z D y)$
14	13	adantl	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land (z D x \in ℝ \land z D y \in ℝ)) \to (z D x) +_{𝑒} (z D y) = (z D x) + (z D y)$
15	12 14	breqtrrd	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land (z D x \in ℝ \land z D y \in ℝ)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
16	15	anassrs	$⊢ (((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \land z D y \in ℝ) \to x D y \leq (z D x) +_{𝑒} (z D y)$
17	6	3adantr3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x D y \in ℝ^{*}$
18		pnfge	$⊢ x D y \in ℝ^{*} \to x D y \leq +∞$
19	17 18	syl	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x D y \leq +∞$
20	19	ad2antrr	$⊢ (((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \land z D y = +∞) \to x D y \leq +∞$
21		oveq2	$⊢ z D y = +∞ \to (z D x) +_{𝑒} (z D y) = (z D x) +_{𝑒} +∞$
22	2	ffnd	$⊢ φ \to D Fn (X \times X)$
23		elxrge0	$⊢ x D y \in [0, +∞] \leftrightarrow (x D y \in ℝ^{*} \land 0 \leq x D y)$
24	6 3 23	sylanbrc	$⊢ (φ \land (x \in X \land y \in X)) \to x D y \in [0, +∞]$
25	24	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X x D y \in [0, +∞]$
26		ffnov	$⊢ D : X \times X ⟶ [0, +∞] \leftrightarrow (D Fn (X \times X) \land \forall x \in X \forall y \in X x D y \in [0, +∞])$
27	22 25 26	sylanbrc	$⊢ φ \to D : X \times X ⟶ [0, +∞]$
28	27	adantr	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to D : X \times X ⟶ [0, +∞]$
29		simpr3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z \in X$
30		simpr1	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x \in X$
31	28 29 30	fovrnd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z D x \in [0, +∞]$
32		eliccxr	$⊢ z D x \in [0, +∞] \to z D x \in ℝ^{*}$
33	31 32	syl	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z D x \in ℝ^{*}$
34		renemnf	$⊢ z D x \in ℝ \to z D x \neq −∞$
35		xaddpnf1	$⊢ (z D x \in ℝ^{*} \land z D x \neq −∞) \to (z D x) +_{𝑒} +∞ = +∞$
36	33 34 35	syl2an	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \to (z D x) +_{𝑒} +∞ = +∞$
37	21 36	sylan9eqr	$⊢ (((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \land z D y = +∞) \to (z D x) +_{𝑒} (z D y) = +∞$
38	20 37	breqtrrd	$⊢ (((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \land z D y = +∞) \to x D y \leq (z D x) +_{𝑒} (z D y)$
39		simpr2	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y \in X$
40	28 29 39	fovrnd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z D y \in [0, +∞]$
41		eliccxr	$⊢ z D y \in [0, +∞] \to z D y \in ℝ^{*}$
42	40 41	syl	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z D y \in ℝ^{*}$
43		elxrge0	$⊢ z D y \in [0, +∞] \leftrightarrow (z D y \in ℝ^{*} \land 0 \leq z D y)$
44	43	simprbi	$⊢ z D y \in [0, +∞] \to 0 \leq z D y$
45	40 44	syl	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to 0 \leq z D y$
46		ge0nemnf	$⊢ (z D y \in ℝ^{*} \land 0 \leq z D y) \to z D y \neq −∞$
47	42 45 46	syl2anc	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z D y \neq −∞$
48	47	a1d	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (\neg x D y \leq (z D x) +_{𝑒} (z D y) \to z D y \neq −∞)$
49	48	necon4bd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (z D y = −∞ \to x D y \leq (z D x) +_{𝑒} (z D y))$
50	49	adantr	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \to (z D y = −∞ \to x D y \leq (z D x) +_{𝑒} (z D y))$
51	50	imp	$⊢ (((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \land z D y = −∞) \to x D y \leq (z D x) +_{𝑒} (z D y)$
52	42	adantr	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \to z D y \in ℝ^{*}$
53		elxr	$⊢ z D y \in ℝ^{*} \leftrightarrow (z D y \in ℝ \lor z D y = +∞ \lor z D y = −∞)$
54	52 53	sylib	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \to (z D y \in ℝ \lor z D y = +∞ \lor z D y = −∞)$
55	16 38 51 54	mpjao3dan	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x \in ℝ) \to x D y \leq (z D x) +_{𝑒} (z D y)$
56	19	adantr	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x = +∞) \to x D y \leq +∞$
57		oveq1	$⊢ z D x = +∞ \to (z D x) +_{𝑒} (z D y) = +∞ +_{𝑒} (z D y)$
58		xaddpnf2	$⊢ (z D y \in ℝ^{*} \land z D y \neq −∞) \to +∞ +_{𝑒} (z D y) = +∞$
59	42 47 58	syl2anc	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to +∞ +_{𝑒} (z D y) = +∞$
60	57 59	sylan9eqr	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x = +∞) \to (z D x) +_{𝑒} (z D y) = +∞$
61	56 60	breqtrrd	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x = +∞) \to x D y \leq (z D x) +_{𝑒} (z D y)$
62		elxrge0	$⊢ z D x \in [0, +∞] \leftrightarrow (z D x \in ℝ^{*} \land 0 \leq z D x)$
63	62	simprbi	$⊢ z D x \in [0, +∞] \to 0 \leq z D x$
64	31 63	syl	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to 0 \leq z D x$
65		ge0nemnf	$⊢ (z D x \in ℝ^{*} \land 0 \leq z D x) \to z D x \neq −∞$
66	33 64 65	syl2anc	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z D x \neq −∞$
67	66	a1d	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (\neg x D y \leq (z D x) +_{𝑒} (z D y) \to z D x \neq −∞)$
68	67	necon4bd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (z D x = −∞ \to x D y \leq (z D x) +_{𝑒} (z D y))$
69	68	imp	$⊢ ((φ \land (x \in X \land y \in X \land z \in X)) \land z D x = −∞) \to x D y \leq (z D x) +_{𝑒} (z D y)$
70		elxr	$⊢ z D x \in ℝ^{*} \leftrightarrow (z D x \in ℝ \lor z D x = +∞ \lor z D x = −∞)$
71	33 70	sylib	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (z D x \in ℝ \lor z D x = +∞ \lor z D x = −∞)$
72	55 61 69 71	mpjao3dan	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
73	1 2 11 72	isxmetd	$⊢ φ \to D \in ∞Met (X)$

Metamath Proof Explorer

Theorem isxmet2d

Proof