metustsym

Description: Elements of the filter base generated by the metric D are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metustsym	$⊢ (D \in PsMet (X) \land A \in F) \to A^{-1} = A$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	metustss	$⊢ (D \in PsMet (X) \land A \in F) \to A \subseteq X \times X$
3		cnvss	$⊢ A \subseteq X \times X \to A^{-1} \subseteq {(X \times X)}^{-1}$
4		cnvxp	$⊢ {(X \times X)}^{-1} = X \times X$
5	3 4	sseqtrdi	$⊢ A \subseteq X \times X \to A^{-1} \subseteq X \times X$
6	2 5	syl	$⊢ (D \in PsMet (X) \land A \in F) \to A^{-1} \subseteq X \times X$
7		simp-4l	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D \in PsMet (X)$
8		simpr1r	$⊢ ((D \in PsMet (X) \land A \in F) \land ((p \in X \land q \in X) \land a \in ℝ^{+} \land A = D^{-1} [[0, a)])) \to q \in X$
9	8	3anassrs	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to q \in X$
10		simpr1l	$⊢ ((D \in PsMet (X) \land A \in F) \land ((p \in X \land q \in X) \land a \in ℝ^{+} \land A = D^{-1} [[0, a)])) \to p \in X$
11	10	3anassrs	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to p \in X$
12		psmetsym	$⊢ (D \in PsMet (X) \land q \in X \land p \in X) \to q D p = p D q$
13	7 9 11 12	syl3anc	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to q D p = p D q$
14		df-ov	$⊢ q D p = D (⟨q, p⟩)$
15		df-ov	$⊢ p D q = D (⟨p, q⟩)$
16	13 14 15	3eqtr3g	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D (⟨q, p⟩) = D (⟨p, q⟩)$
17	16	eleq1d	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (D (⟨q, p⟩) \in [0, a) \leftrightarrow D (⟨p, q⟩) \in [0, a))$
18		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
19		ffun	$⊢ D : X \times X ⟶ ℝ^{*} \to Fun D$
20	7 18 19	3syl	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to Fun D$
21		simpllr	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (p \in X \land q \in X)$
22	21	ancomd	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (q \in X \land p \in X)$
23		opelxpi	$⊢ (q \in X \land p \in X) \to ⟨q, p⟩ \in (X \times X)$
24	22 23	syl	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to ⟨q, p⟩ \in (X \times X)$
25		fdm	$⊢ D : X \times X ⟶ ℝ^{*} \to dom D = X \times X$
26	7 18 25	3syl	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to dom D = X \times X$
27	24 26	eleqtrrd	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to ⟨q, p⟩ \in dom D$
28		fvimacnv	$⊢ (Fun D \land ⟨q, p⟩ \in dom D) \to (D (⟨q, p⟩) \in [0, a) \leftrightarrow ⟨q, p⟩ \in D^{-1} [[0, a)])$
29	20 27 28	syl2anc	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (D (⟨q, p⟩) \in [0, a) \leftrightarrow ⟨q, p⟩ \in D^{-1} [[0, a)])$
30		opelxpi	$⊢ (p \in X \land q \in X) \to ⟨p, q⟩ \in (X \times X)$
31	21 30	syl	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to ⟨p, q⟩ \in (X \times X)$
32	31 26	eleqtrrd	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to ⟨p, q⟩ \in dom D$
33		fvimacnv	$⊢ (Fun D \land ⟨p, q⟩ \in dom D) \to (D (⟨p, q⟩) \in [0, a) \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
34	20 32 33	syl2anc	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (D (⟨p, q⟩) \in [0, a) \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
35	17 29 34	3bitr3d	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (⟨q, p⟩ \in D^{-1} [[0, a)] \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
36		simpr	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to A = D^{-1} [[0, a)]$
37	36	eleq2d	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (⟨q, p⟩ \in A \leftrightarrow ⟨q, p⟩ \in D^{-1} [[0, a)])$
38	36	eleq2d	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (⟨p, q⟩ \in A \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
39	35 37 38	3bitr4d	$⊢ ((((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (⟨q, p⟩ \in A \leftrightarrow ⟨p, q⟩ \in A)$
40		eqid	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
41	40	elrnmpt	$⊢ A \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \to (A \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} A = D^{-1} [[0, a)])$
42	41	ibi	$⊢ A \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
43	42 1	eleq2s	$⊢ A \in F \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
44	43	ad2antlr	$⊢ ((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
45	39 44	r19.29a	$⊢ ((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \to (⟨q, p⟩ \in A \leftrightarrow ⟨p, q⟩ \in A)$
46		df-br	$⊢ p A^{-1} q \leftrightarrow ⟨p, q⟩ \in A^{-1}$
47		vex	$⊢ p \in V$
48		vex	$⊢ q \in V$
49	47 48	opelcnv	$⊢ ⟨p, q⟩ \in A^{-1} \leftrightarrow ⟨q, p⟩ \in A$
50	46 49	bitri	$⊢ p A^{-1} q \leftrightarrow ⟨q, p⟩ \in A$
51		df-br	$⊢ p A q \leftrightarrow ⟨p, q⟩ \in A$
52	45 50 51	3bitr4g	$⊢ ((D \in PsMet (X) \land A \in F) \land (p \in X \land q \in X)) \to (p A^{-1} q \leftrightarrow p A q)$
53	52	3impb	$⊢ ((D \in PsMet (X) \land A \in F) \land p \in X \land q \in X) \to (p A^{-1} q \leftrightarrow p A q)$
54	6 2 53	eqbrrdva	$⊢ (D \in PsMet (X) \land A \in F) \to A^{-1} = A$

Metamath Proof Explorer

Theorem metustsym

Proof