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 ⊢D∈PsMet⁡X∧A∈X→ADA=0

Proof

Step Hyp Ref Expression
1 elfvex ⊢D∈PsMet⁡X→X∈V
2 ispsmet ⊢X∈V→D∈PsMet⁡X↔D:X×X⟶ℝ*∧∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
3 1 2 syl ⊢D∈PsMet⁡X→D∈PsMet⁡X↔D:X×X⟶ℝ*∧∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
4 3 ibi ⊢D∈PsMet⁡X→D:X×X⟶ℝ*∧∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
5 4 simprd ⊢D∈PsMet⁡X→∀a∈XaDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
6 5 r19.21bi ⊢D∈PsMet⁡X∧a∈X→aDa=0∧∀b∈X∀c∈XaDb≤cDa+𝑒cDb
7 6 simpld ⊢D∈PsMet⁡X∧a∈X→aDa=0
8 7 ralrimiva ⊢D∈PsMet⁡X→∀a∈XaDa=0
9 id ⊢a=A→a=A
10 9 9 oveq12d ⊢a=A→aDa=ADA
11 10 eqeq1d ⊢a=A→aDa=0↔ADA=0
12 11 rspcv ⊢A∈X→∀a∈XaDa=0→ADA=0
13 8 12 mpan9 ⊢D∈PsMet⁡X∧A∈X→ADA=0