ismet2

Description: An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	ismet2	$⊢ D \in Met (X) \leftrightarrow (D \in ∞Met (X) \land D : X \times X ⟶ ℝ)$

Proof

Step	Hyp	Ref	Expression
1		elfvex	$⊢ D \in Met (X) \to X \in V$
2		elfvex	$⊢ D \in ∞Met (X) \to X \in V$
3	2	adantr	$⊢ (D \in ∞Met (X) \land D : X \times X ⟶ ℝ) \to X \in V$
4		simpllr	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to D : X \times X ⟶ ℝ$
5		simpr	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to z \in X$
6		simplrl	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to x \in X$
7	4 5 6	fovrnd	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to z D x \in ℝ$
8		simplrr	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to y \in X$
9	4 5 8	fovrnd	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to z D y \in ℝ$
10	7 9	rexaddd	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to (z D x) +_{𝑒} (z D y) = (z D x) + (z D y)$
11	10	breq2d	$⊢ (((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \land z \in X) \to (x D y \leq (z D x) +_{𝑒} (z D y) \leftrightarrow x D y \leq (z D x) + (z D y))$
12	11	ralbidva	$⊢ ((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \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))$
13	12	anbi2d	$⊢ ((X \in V \land D : X \times X ⟶ ℝ) \land (x \in X \land y \in X)) \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)))$
14	13	2ralbidva	$⊢ (X \in V \land D : X \times X ⟶ ℝ) \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)))$
15		simpr	$⊢ (X \in V \land D : X \times X ⟶ ℝ) \to D : X \times X ⟶ ℝ$
16		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
17		fss	$⊢ (D : X \times X ⟶ ℝ \land ℝ \subseteq ℝ^{}) \to D : X \times X ⟶ ℝ^{}$
18	15 16 17	sylancl	$⊢ (X \in V \land D : X \times X ⟶ ℝ) \to D : X \times X ⟶ ℝ^{*}$
19	18	biantrurd	$⊢ (X \in V \land D : X \times X ⟶ ℝ) \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 (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))))$
20	14 19	bitr3d	$⊢ (X \in V \land D : X \times X ⟶ ℝ) \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 (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))))$
21	20	pm5.32da	$⊢ X \in V \to ((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))) \leftrightarrow (D : X \times X ⟶ ℝ \land (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)))))$
22	21	biancomd	$⊢ X \in V \to ((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))) \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))) \land D : X \times X ⟶ ℝ))$
23		ismet	$⊢ X \in V \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))))$
24		isxmet	$⊢ X \in V \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))))$
25	24	anbi1d	$⊢ X \in V \to ((D \in ∞Met (X) \land D : X \times 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))) \land D : X \times X ⟶ ℝ))$
26	22 23 25	3bitr4d	$⊢ X \in V \to (D \in Met (X) \leftrightarrow (D \in ∞Met (X) \land D : X \times X ⟶ ℝ))$
27	1 3 26	pm5.21nii	$⊢ D \in Met (X) \leftrightarrow (D \in ∞Met (X) \land D : X \times X ⟶ ℝ)$

Metamath Proof Explorer

Theorem ismet2

Proof