metider

Description: The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Assertion	metider	$⊢ D \in PsMet (X) \to ~_{Met} (D) Er X$

Proof

Step	Hyp	Ref	Expression
1		metidss	$⊢ D \in PsMet (X) \to ~_{Met} (D) \subseteq X \times X$
2		xpss	$⊢ X \times X \subseteq V \times V$
3	1 2	sstrdi	$⊢ D \in PsMet (X) \to ~_{Met} (D) \subseteq V \times V$
4		df-rel	$⊢ Rel ~_{Met} (D) \leftrightarrow ~_{Met} (D) \subseteq V \times V$
5	3 4	sylibr	$⊢ D \in PsMet (X) \to Rel ~_{Met} (D)$
6	1	ssbrd	$⊢ D \in PsMet (X) \to (x ~_{Met} (D) y \to x (X \times X) y)$
7	6	imp	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) y) \to x (X \times X) y$
8		brxp	$⊢ x (X \times X) y \leftrightarrow (x \in X \land y \in X)$
9	7 8	sylib	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) y) \to (x \in X \land y \in X)$
10		psmetsym	$⊢ (D \in PsMet (X) \land x \in X \land y \in X) \to x D y = y D x$
11	10	3expb	$⊢ (D \in PsMet (X) \land (x \in X \land y \in X)) \to x D y = y D x$
12	11	eqeq1d	$⊢ (D \in PsMet (X) \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow y D x = 0)$
13		metidv	$⊢ (D \in PsMet (X) \land (x \in X \land y \in X)) \to (x ~_{Met} (D) y \leftrightarrow x D y = 0)$
14		metidv	$⊢ (D \in PsMet (X) \land (y \in X \land x \in X)) \to (y ~_{Met} (D) x \leftrightarrow y D x = 0)$
15	14	ancom2s	$⊢ (D \in PsMet (X) \land (x \in X \land y \in X)) \to (y ~_{Met} (D) x \leftrightarrow y D x = 0)$
16	12 13 15	3bitr4d	$⊢ (D \in PsMet (X) \land (x \in X \land y \in X)) \to (x ~_{Met} (D) y \leftrightarrow y ~_{Met} (D) x)$
17	16	biimpd	$⊢ (D \in PsMet (X) \land (x \in X \land y \in X)) \to (x ~_{Met} (D) y \to y ~_{Met} (D) x)$
18	17	impancom	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) y) \to ((x \in X \land y \in X) \to y ~_{Met} (D) x)$
19	9 18	mpd	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) y) \to y ~_{Met} (D) x$
20		simpl	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to D \in PsMet (X)$
21		simprr	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to y ~_{Met} (D) z$
22	1	ssbrd	$⊢ D \in PsMet (X) \to (y ~_{Met} (D) z \to y (X \times X) z)$
23	22	imp	$⊢ (D \in PsMet (X) \land y ~_{Met} (D) z) \to y (X \times X) z$
24		brxp	$⊢ y (X \times X) z \leftrightarrow (y \in X \land z \in X)$
25	23 24	sylib	$⊢ (D \in PsMet (X) \land y ~_{Met} (D) z) \to (y \in X \land z \in X)$
26	21 25	syldan	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (y \in X \land z \in X)$
27	26	simpld	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to y \in X$
28		simprl	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x ~_{Met} (D) y$
29	28 9	syldan	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (x \in X \land y \in X)$
30	29	simpld	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x \in X$
31	26	simprd	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to z \in X$
32		psmettri2	$⊢ (D \in PsMet (X) \land (y \in X \land x \in X \land z \in X)) \to x D z \leq (y D x) +_{𝑒} (y D z)$
33	20 27 30 31 32	syl13anc	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x D z \leq (y D x) +_{𝑒} (y D z)$
34	29 11	syldan	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x D y = y D x$
35	29 13	syldan	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (x ~_{Met} (D) y \leftrightarrow x D y = 0)$
36	28 35	mpbid	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x D y = 0$
37	34 36	eqtr3d	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to y D x = 0$
38		metidv	$⊢ (D \in PsMet (X) \land (y \in X \land z \in X)) \to (y ~_{Met} (D) z \leftrightarrow y D z = 0)$
39	26 38	syldan	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (y ~_{Met} (D) z \leftrightarrow y D z = 0)$
40	21 39	mpbid	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to y D z = 0$
41	37 40	oveq12d	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (y D x) +_{𝑒} (y D z) = 0 +_{𝑒} 0$
42		0xr	$⊢ 0 \in ℝ^{*}$
43		xaddrid	$⊢ 0 \in ℝ^{*} \to 0 +_{𝑒} 0 = 0$
44	42 43	ax-mp	$⊢ 0 +_{𝑒} 0 = 0$
45	41 44	eqtrdi	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (y D x) +_{𝑒} (y D z) = 0$
46	33 45	breqtrd	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x D z \leq 0$
47		psmetge0	$⊢ (D \in PsMet (X) \land x \in X \land z \in X) \to 0 \leq x D z$
48	20 30 31 47	syl3anc	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to 0 \leq x D z$
49		psmetcl	$⊢ (D \in PsMet (X) \land x \in X \land z \in X) \to x D z \in ℝ^{*}$
50	20 30 31 49	syl3anc	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x D z \in ℝ^{*}$
51		xrletri3	$⊢ (x D z \in ℝ^{} \land 0 \in ℝ^{}) \to (x D z = 0 \leftrightarrow (x D z \leq 0 \land 0 \leq x D z))$
52	50 42 51	sylancl	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (x D z = 0 \leftrightarrow (x D z \leq 0 \land 0 \leq x D z))$
53	46 48 52	mpbir2and	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x D z = 0$
54		metidv	$⊢ (D \in PsMet (X) \land (x \in X \land z \in X)) \to (x ~_{Met} (D) z \leftrightarrow x D z = 0)$
55	20 30 31 54	syl12anc	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to (x ~_{Met} (D) z \leftrightarrow x D z = 0)$
56	53 55	mpbird	$⊢ (D \in PsMet (X) \land (x ~_{Met} (D) y \land y ~_{Met} (D) z)) \to x ~_{Met} (D) z$
57		psmet0	$⊢ (D \in PsMet (X) \land x \in X) \to x D x = 0$
58		metidv	$⊢ (D \in PsMet (X) \land (x \in X \land x \in X)) \to (x ~_{Met} (D) x \leftrightarrow x D x = 0)$
59	58	anabsan2	$⊢ (D \in PsMet (X) \land x \in X) \to (x ~_{Met} (D) x \leftrightarrow x D x = 0)$
60	57 59	mpbird	$⊢ (D \in PsMet (X) \land x \in X) \to x ~_{Met} (D) x$
61	1	ssbrd	$⊢ D \in PsMet (X) \to (x ~_{Met} (D) x \to x (X \times X) x)$
62	61	imp	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) x) \to x (X \times X) x$
63		brxp	$⊢ x (X \times X) x \leftrightarrow (x \in X \land x \in X)$
64	62 63	sylib	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) x) \to (x \in X \land x \in X)$
65	64	simpld	$⊢ (D \in PsMet (X) \land x ~_{Met} (D) x) \to x \in X$
66	60 65	impbida	$⊢ D \in PsMet (X) \to (x \in X \leftrightarrow x ~_{Met} (D) x)$
67	5 19 56 66	iserd	$⊢ D \in PsMet (X) \to ~_{Met} (D) Er X$

Metamath Proof Explorer

Theorem metider

Proof