metidval

Description: Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Assertion	metidval	$⊢ D \in PsMet (X) \to ~_{Met} (D) = \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\}$

Proof

Step	Hyp	Ref	Expression
1		df-metid	$⊢ ~_{Met} = (d \in ⋃ ran PsMet ⟼ \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\})$
2	1	a1i	$⊢ D \in PsMet (X) \to ~_{Met} = (d \in ⋃ ran PsMet ⟼ \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\})$
3		simpr	$⊢ (D \in PsMet (X) \land d = D) \to d = D$
4	3	dmeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom d = dom D$
5	4	dmeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = dom dom D$
6		psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$
7	6	adantr	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom D$
8	5 7	eqtr4d	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = X$
9	8	eleq2d	$⊢ (D \in PsMet (X) \land d = D) \to (x \in dom dom d \leftrightarrow x \in X)$
10	8	eleq2d	$⊢ (D \in PsMet (X) \land d = D) \to (y \in dom dom d \leftrightarrow y \in X)$
11	9 10	anbi12d	$⊢ (D \in PsMet (X) \land d = D) \to ((x \in dom dom d \land y \in dom dom d) \leftrightarrow (x \in X \land y \in X))$
12	3	oveqd	$⊢ (D \in PsMet (X) \land d = D) \to x d y = x D y$
13	12	eqeq1d	$⊢ (D \in PsMet (X) \land d = D) \to (x d y = 0 \leftrightarrow x D y = 0)$
14	11 13	anbi12d	$⊢ (D \in PsMet (X) \land d = D) \to (((x \in dom dom d \land y \in dom dom d) \land x d y = 0) \leftrightarrow ((x \in X \land y \in X) \land x D y = 0))$
15	14	opabbidv	$⊢ (D \in PsMet (X) \land d = D) \to \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\} = \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\}$
16		elfvdm	$⊢ D \in PsMet (X) \to X \in dom PsMet$
17		fveq2	$⊢ x = X \to PsMet (x) = PsMet (X)$
18	17	eleq2d	$⊢ x = X \to (D \in PsMet (x) \leftrightarrow D \in PsMet (X))$
19	18	rspcev	$⊢ (X \in dom PsMet \land D \in PsMet (X)) \to \exists x \in dom PsMet D \in PsMet (x)$
20	16 19	mpancom	$⊢ D \in PsMet (X) \to \exists x \in dom PsMet D \in PsMet (x)$
21		df-psmet	$⊢ PsMet = (x \in V ⟼ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\})$
22	21	funmpt2	$⊢ Fun PsMet$
23		elunirn	$⊢ Fun PsMet \to (D \in ⋃ ran PsMet \leftrightarrow \exists x \in dom PsMet D \in PsMet (x))$
24	22 23	ax-mp	$⊢ D \in ⋃ ran PsMet \leftrightarrow \exists x \in dom PsMet D \in PsMet (x)$
25	20 24	sylibr	$⊢ D \in PsMet (X) \to D \in ⋃ ran PsMet$
26		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \subseteq X \times X$
27		elfvex	$⊢ D \in PsMet (X) \to X \in V$
28	27 27	xpexd	$⊢ D \in PsMet (X) \to X \times X \in V$
29		ssexg	$⊢ (\{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \subseteq X \times X \land X \times X \in V) \to \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \in V$
30	26 28 29	sylancr	$⊢ D \in PsMet (X) \to \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \in V$
31	2 15 25 30	fvmptd	$⊢ D \in PsMet (X) \to ~_{Met} (D) = \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\}$

Metamath Proof Explorer

Theorem metidval

Proof