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

Metamath Proof Explorer

Theorem psmet0

Description: The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmet0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
2 ispsmet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ) ) )
3 1 2 syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ) ) )
4 3 ibi ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ) )
5 4 simprd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) )
6 5 r19.21bi ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) )
7 6 simpld ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 𝐷 𝑎 ) = 0 )
8 7 ralrimiva ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑎 ∈ 𝑋 ( 𝑎 𝐷 𝑎 ) = 0 )
9 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
10 9 9 oveq12d ⊢ ( 𝑎 = 𝐴 → ( 𝑎 𝐷 𝑎 ) = ( 𝐴 𝐷 𝐴 ) )
11 10 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 𝐷 𝑎 ) = 0 ↔ ( 𝐴 𝐷 𝐴 ) = 0 ) )
12 11 rspcv ⊢ ( 𝐴 ∈ 𝑋 → ( ∀ 𝑎 ∈ 𝑋 ( 𝑎 𝐷 𝑎 ) = 0 → ( 𝐴 𝐷 𝐴 ) = 0 ) )
13 8 12 mpan9 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )