xmeter

Description: The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Hypothesis	xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
	Assertion	xmeter	$⊢ D \in ∞Met (X) \to \underset{˙}{\sim} Er X$

Proof

Step	Hyp	Ref	Expression
1		xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
2		cnvimass	$⊢ D^{-1} [ℝ] \subseteq dom D$
3	1 2	eqsstri	$⊢ \underset{˙}{\sim} \subseteq dom D$
4		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
5	3 4	fssdm	$⊢ D \in ∞Met (X) \to \underset{˙}{\sim} \subseteq X \times X$
6		relxp	$⊢ Rel (X \times X)$
7		relss	$⊢ \underset{˙}{\sim} \subseteq X \times X \to (Rel (X \times X) \to Rel \underset{˙}{\sim})$
8	5 6 7	mpisyl	$⊢ D \in ∞Met (X) \to Rel \underset{˙}{\sim}$
9	1	xmeterval	$⊢ D \in ∞Met (X) \to (x \underset{˙}{\sim} y \leftrightarrow (x \in X \land y \in X \land x D y \in ℝ))$
10	9	biimpa	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to (x \in X \land y \in X \land x D y \in ℝ)$
11	10	simp2d	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to y \in X$
12	10	simp1d	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to x \in X$
13		simpl	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to D \in ∞Met (X)$
14		xmetsym	$⊢ (D \in ∞Met (X) \land x \in X \land y \in X) \to x D y = y D x$
15	13 12 11 14	syl3anc	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to x D y = y D x$
16	10	simp3d	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to x D y \in ℝ$
17	15 16	eqeltrrd	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to y D x \in ℝ$
18	1	xmeterval	$⊢ D \in ∞Met (X) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in X \land x \in X \land y D x \in ℝ))$
19	18	adantr	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in X \land x \in X \land y D x \in ℝ))$
20	11 12 17 19	mpbir3and	$⊢ (D \in ∞Met (X) \land x \underset{˙}{\sim} y) \to y \underset{˙}{\sim} x$
21	12	adantrr	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \in X$
22	1	xmeterval	$⊢ D \in ∞Met (X) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in X \land z \in X \land y D z \in ℝ))$
23	22	biimpa	$⊢ (D \in ∞Met (X) \land y \underset{˙}{\sim} z) \to (y \in X \land z \in X \land y D z \in ℝ)$
24	23	adantrl	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (y \in X \land z \in X \land y D z \in ℝ)$
25	24	simp2d	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to z \in X$
26		simpl	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to D \in ∞Met (X)$
27	16	adantrr	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x D y \in ℝ$
28	24	simp3d	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y D z \in ℝ$
29		rexadd	$⊢ (x D y \in ℝ \land y D z \in ℝ) \to (x D y) +_{𝑒} (y D z) = (x D y) + (y D z)$
30		readdcl	$⊢ (x D y \in ℝ \land y D z \in ℝ) \to (x D y) + (y D z) \in ℝ$
31	29 30	eqeltrd	$⊢ (x D y \in ℝ \land y D z \in ℝ) \to (x D y) +_{𝑒} (y D z) \in ℝ$
32	27 28 31	syl2anc	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (x D y) +_{𝑒} (y D z) \in ℝ$
33	11	adantrr	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y \in X$
34		xmettri	$⊢ (D \in ∞Met (X) \land (x \in X \land z \in X \land y \in X)) \to x D z \leq (x D y) +_{𝑒} (y D z)$
35	26 21 25 33 34	syl13anc	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x D z \leq (x D y) +_{𝑒} (y D z)$
36		xmetlecl	$⊢ (D \in ∞Met (X) \land (x \in X \land z \in X) \land ((x D y) +_{𝑒} (y D z) \in ℝ \land x D z \leq (x D y) +_{𝑒} (y D z))) \to x D z \in ℝ$
37	26 21 25 32 35 36	syl122anc	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x D z \in ℝ$
38	1	xmeterval	$⊢ D \in ∞Met (X) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in X \land z \in X \land x D z \in ℝ))$
39	38	adantr	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in X \land z \in X \land x D z \in ℝ))$
40	21 25 37 39	mpbir3and	$⊢ (D \in ∞Met (X) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \underset{˙}{\sim} z$
41		xmet0	$⊢ (D \in ∞Met (X) \land x \in X) \to x D x = 0$
42		0re	$⊢ 0 \in ℝ$
43	41 42	eqeltrdi	$⊢ (D \in ∞Met (X) \land x \in X) \to x D x \in ℝ$
44	43	ex	$⊢ D \in ∞Met (X) \to (x \in X \to x D x \in ℝ)$
45	44	pm4.71rd	$⊢ D \in ∞Met (X) \to (x \in X \leftrightarrow (x D x \in ℝ \land x \in X))$
46		df-3an	$⊢ (x \in X \land x \in X \land x D x \in ℝ) \leftrightarrow ((x \in X \land x \in X) \land x D x \in ℝ)$
47		anidm	$⊢ (x \in X \land x \in X) \leftrightarrow x \in X$
48	47	anbi2ci	$⊢ ((x \in X \land x \in X) \land x D x \in ℝ) \leftrightarrow (x D x \in ℝ \land x \in X)$
49	46 48	bitri	$⊢ (x \in X \land x \in X \land x D x \in ℝ) \leftrightarrow (x D x \in ℝ \land x \in X)$
50	45 49	bitr4di	$⊢ D \in ∞Met (X) \to (x \in X \leftrightarrow (x \in X \land x \in X \land x D x \in ℝ))$
51	1	xmeterval	$⊢ D \in ∞Met (X) \to (x \underset{˙}{\sim} x \leftrightarrow (x \in X \land x \in X \land x D x \in ℝ))$
52	50 51	bitr4d	$⊢ D \in ∞Met (X) \to (x \in X \leftrightarrow x \underset{˙}{\sim} x)$
53	8 20 40 52	iserd	$⊢ D \in ∞Met (X) \to \underset{˙}{\sim} Er X$

Metamath Proof Explorer

Theorem xmeter

Proof