This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmetpsmet

Description: An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Assertion	xmetpsmet	$⊢ D \in ∞Met (X) \to D \in PsMet (X)$

Proof

Step	Hyp	Ref	Expression
1		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
2		xmet0	$⊢ (D \in ∞Met (X) \land x \in X) \to x D x = 0$
3		3anrot	$⊢ (z \in X \land x \in X \land y \in X) \leftrightarrow (x \in X \land y \in X \land z \in X)$
4		xmettri2	$⊢ (D \in ∞Met (X) \land (z \in X \land x \in X \land y \in X)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
5	3 4	sylan2br	$⊢ (D \in ∞Met (X) \land (x \in X \land y \in X \land z \in X)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
6	5	3anassrs	$⊢ (((D \in ∞Met (X) \land x \in X) \land y \in X) \land z \in X) \to x D y \leq (z D x) +_{𝑒} (z D y)$
7	6	ralrimiva	$⊢ ((D \in ∞Met (X) \land x \in X) \land y \in X) \to \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)$
8	7	ralrimiva	$⊢ (D \in ∞Met (X) \land x \in X) \to \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)$
9	2 8	jca	$⊢ (D \in ∞Met (X) \land x \in X) \to (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))$
10	9	ralrimiva	$⊢ D \in ∞Met (X) \to \forall x \in X (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))$
11		elfvex	$⊢ D \in ∞Met (X) \to X \in V$
12		ispsmet	$⊢ X \in V \to (D \in PsMet (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
13	11 12	syl	$⊢ D \in ∞Met (X) \to (D \in PsMet (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
14	1 10 13	mpbir2and	$⊢ D \in ∞Met (X) \to D \in PsMet (X)$