Metamath Proof Explorer

Theorem xmeteq0

Description: The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmeteq0 ⊢D∈∞Met⁡X∧A∈X∧B∈X→ADB=0↔A=B

Proof

Step Hyp Ref Expression
1 elfvdm ⊢D∈∞Met⁡X→X∈dom⁡∞Met
2 isxmet ⊢X∈dom⁡∞Met→D∈∞Met⁡X↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
3 1 2 syl ⊢D∈∞Met⁡X→D∈∞Met⁡X↔D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
4 3 ibi ⊢D∈∞Met⁡X→D:X×X⟶ℝ*∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy
5 simpl ⊢xDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy→xDy=0↔x=y
6 5 2ralimi ⊢∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+𝑒zDy→∀x∈X∀y∈XxDy=0↔x=y
7 4 6 simpl2im ⊢D∈∞Met⁡X→∀x∈X∀y∈XxDy=0↔x=y
8 oveq1 ⊢x=A→xDy=ADy
9 8 eqeq1d ⊢x=A→xDy=0↔ADy=0
10 eqeq1 ⊢x=A→x=y↔A=y
11 9 10 bibi12d ⊢x=A→xDy=0↔x=y↔ADy=0↔A=y
12 oveq2 ⊢y=B→ADy=ADB
13 12 eqeq1d ⊢y=B→ADy=0↔ADB=0
14 eqeq2 ⊢y=B→A=y↔A=B
15 13 14 bibi12d ⊢y=B→ADy=0↔A=y↔ADB=0↔A=B
16 11 15 rspc2v ⊢A∈X∧B∈X→∀x∈X∀y∈XxDy=0↔x=y→ADB=0↔A=B
17 7 16 syl5com ⊢D∈∞Met⁡X→A∈X∧B∈X→ADB=0↔A=B
18 17 3impib ⊢D∈∞Met⁡X∧A∈X∧B∈X→ADB=0↔A=B