isxmet

Description: Express the predicate " D is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	isxmet	$⊢ X \in A \to (D \in ∞Met (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ X \in A \to X \in V$
2		xpeq12	$⊢ (t = X \land t = X) \to t \times t = X \times X$
3	2	anidms	$⊢ t = X \to t \times t = X \times X$
4	3	oveq2d	$⊢ t = X \to {ℝ^{}}^{(t \times t)} = {ℝ^{}}^{(X \times X)}$
5		raleq	$⊢ t = X \to (\forall z \in t x d y \leq (z d x) +_{𝑒} (z d y) \leftrightarrow \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))$
6	5	anbi2d	$⊢ t = X \to (((x d y = 0 \leftrightarrow x = y) \land \forall z \in t x d y \leq (z d x) +_{𝑒} (z d y)) \leftrightarrow ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y)))$
7	6	raleqbi1dv	$⊢ t = X \to (\forall y \in t ((x d y = 0 \leftrightarrow x = y) \land \forall z \in t x d y \leq (z d x) +_{𝑒} (z d y)) \leftrightarrow \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y)))$
8	7	raleqbi1dv	$⊢ t = X \to (\forall x \in t \forall y \in t ((x d y = 0 \leftrightarrow x = y) \land \forall z \in t x d y \leq (z d x) +_{𝑒} (z d y)) \leftrightarrow \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y)))$
9	4 8	rabeqbidv	$⊢ t = X \to \{d \in ({ℝ^{}}^{(t \times t)}) \| \forall x \in t \forall y \in t ((x d y = 0 \leftrightarrow x = y) \land \forall z \in t x d y \leq (z d x) +_{𝑒} (z d y))\} = \{d \in ({ℝ^{}}^{(X \times X)}) \| \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))\}$
10		df-xmet	$⊢ ∞Met = (t \in V ⟼ \{d \in ({ℝ^{*}}^{(t \times t)}) \| \forall x \in t \forall y \in t ((x d y = 0 \leftrightarrow x = y) \land \forall z \in t x d y \leq (z d x) +_{𝑒} (z d y))\})$
11		ovex	$⊢ {ℝ^{*}}^{(X \times X)} \in V$
12	11	rabex	$⊢ \{d \in ({ℝ^{*}}^{(X \times X)}) \| \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))\} \in V$
13	9 10 12	fvmpt	$⊢ X \in V \to ∞Met (X) = \{d \in ({ℝ^{*}}^{(X \times X)}) \| \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))\}$
14	1 13	syl	$⊢ X \in A \to ∞Met (X) = \{d \in ({ℝ^{*}}^{(X \times X)}) \| \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))\}$
15	14	eleq2d	$⊢ X \in A \to (D \in ∞Met (X) \leftrightarrow D \in \{d \in ({ℝ^{*}}^{(X \times X)}) \| \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))\})$
16		oveq	$⊢ d = D \to x d y = x D y$
17	16	eqeq1d	$⊢ d = D \to (x d y = 0 \leftrightarrow x D y = 0)$
18	17	bibi1d	$⊢ d = D \to ((x d y = 0 \leftrightarrow x = y) \leftrightarrow (x D y = 0 \leftrightarrow x = y))$
19		oveq	$⊢ d = D \to z d x = z D x$
20		oveq	$⊢ d = D \to z d y = z D y$
21	19 20	oveq12d	$⊢ d = D \to (z d x) +_{𝑒} (z d y) = (z D x) +_{𝑒} (z D y)$
22	16 21	breq12d	$⊢ d = D \to (x d y \leq (z d x) +_{𝑒} (z d y) \leftrightarrow x D y \leq (z D x) +_{𝑒} (z D y))$
23	22	ralbidv	$⊢ d = D \to (\forall z \in X x d y \leq (z d x) +_{𝑒} (z d y) \leftrightarrow \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))$
24	18 23	anbi12d	$⊢ d = D \to (((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y)) \leftrightarrow ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)))$
25	24	2ralbidv	$⊢ d = D \to (\forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y)) \leftrightarrow \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)))$
26	25	elrab	$⊢ D \in \{d \in ({ℝ^{}}^{(X \times X)}) \| \forall x \in X \forall y \in X ((x d y = 0 \leftrightarrow x = y) \land \forall z \in X x d y \leq (z d x) +_{𝑒} (z d y))\} \leftrightarrow (D \in ({ℝ^{}}^{(X \times X)}) \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)))$
27	15 26	syl6bb	$⊢ X \in A \to (D \in ∞Met (X) \leftrightarrow (D \in ({ℝ^{*}}^{(X \times X)}) \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
28		xrex	$⊢ ℝ^{*} \in V$
29		sqxpexg	$⊢ X \in A \to X \times X \in V$
30		elmapg	$⊢ (ℝ^{} \in V \land X \times X \in V) \to (D \in ({ℝ^{}}^{(X \times X)}) \leftrightarrow D : X \times X ⟶ ℝ^{*})$
31	28 29 30	sylancr	$⊢ X \in A \to (D \in ({ℝ^{}}^{(X \times X)}) \leftrightarrow D : X \times X ⟶ ℝ^{})$
32	31	anbi1d	$⊢ X \in A \to ((D \in ({ℝ^{}}^{(X \times X)}) \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))) \leftrightarrow (D : X \times X ⟶ ℝ^{} \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
33	27 32	bitrd	$⊢ X \in A \to (D \in ∞Met (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$

Metamath Proof Explorer

Theorem isxmet

Proof