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 ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
2 xmet0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑥 ) = 0 )
3 3anrot ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) )
4 xmettri2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
5 3 4 sylan2br ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
6 5 3anassrs ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
7 6 ralrimiva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
8 7 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
9 2 8 jca ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
10 9 ralrimiva ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
11 elfvex ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ V )
12 ispsmet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
13 11 12 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
14 1 10 13 mpbir2and ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )