Metamath Proof Explorer

Theorem metidv

Description: A and B identify by the metric D if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion metidv ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A ~ Met ⁡ D B ↔ A D B = 0

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ a = A → a ∈ X ↔ A ∈ X
2 eleq1 ⊢ b = B → b ∈ X ↔ B ∈ X
3 1 2 bi2anan9 ⊢ a = A ∧ b = B → a ∈ X ∧ b ∈ X ↔ A ∈ X ∧ B ∈ X
4 oveq12 ⊢ a = A ∧ b = B → a D b = A D B
5 4 eqeq1d ⊢ a = A ∧ b = B → a D b = 0 ↔ A D B = 0
6 3 5 anbi12d ⊢ a = A ∧ b = B → a ∈ X ∧ b ∈ X ∧ a D b = 0 ↔ A ∈ X ∧ B ∈ X ∧ A D B = 0
7 eqid ⊢ a b | a ∈ X ∧ b ∈ X ∧ a D b = 0 = a b | a ∈ X ∧ b ∈ X ∧ a D b = 0
8 6 7 brabga ⊢ A ∈ X ∧ B ∈ X → A a b | a ∈ X ∧ b ∈ X ∧ a D b = 0 B ↔ A ∈ X ∧ B ∈ X ∧ A D B = 0
9 8 adantl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A a b | a ∈ X ∧ b ∈ X ∧ a D b = 0 B ↔ A ∈ X ∧ B ∈ X ∧ A D B = 0
10 metidval ⊢ D ∈ PsMet ⁡ X → ~ Met ⁡ D = a b | a ∈ X ∧ b ∈ X ∧ a D b = 0
11 10 adantr ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → ~ Met ⁡ D = a b | a ∈ X ∧ b ∈ X ∧ a D b = 0
12 11 breqd ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A ~ Met ⁡ D B ↔ A a b | a ∈ X ∧ b ∈ X ∧ a D b = 0 B
13 ibar ⊢ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A ∈ X ∧ B ∈ X ∧ A D B = 0
14 13 adantl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A ∈ X ∧ B ∈ X ∧ A D B = 0
15 9 12 14 3bitr4d ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A ~ Met ⁡ D B ↔ A D B = 0