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⁡DB↔ADB=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→aDb=ADB
5 4 eqeq1d ⊢a=A∧b=B→aDb=0↔ADB=0
6 3 5 anbi12d ⊢a=A∧b=B→a∈X∧b∈X∧aDb=0↔A∈X∧B∈X∧ADB=0
7 eqid ⊢ab|a∈X∧b∈X∧aDb=0=ab|a∈X∧b∈X∧aDb=0
8 6 7 brabga ⊢A∈X∧B∈X→Aab|a∈X∧b∈X∧aDb=0B↔A∈X∧B∈X∧ADB=0
9 8 adantl ⊢D∈PsMet⁡X∧A∈X∧B∈X→Aab|a∈X∧b∈X∧aDb=0B↔A∈X∧B∈X∧ADB=0
10 metidval ⊢D∈PsMet⁡X→~Met⁡D=ab|a∈X∧b∈X∧aDb=0
11 10 adantr ⊢D∈PsMet⁡X∧A∈X∧B∈X→~Met⁡D=ab|a∈X∧b∈X∧aDb=0
12 11 breqd ⊢D∈PsMet⁡X∧A∈X∧B∈X→A~Met⁡DB↔Aab|a∈X∧b∈X∧aDb=0B
13 ibar ⊢A∈X∧B∈X→ADB=0↔A∈X∧B∈X∧ADB=0
14 13 adantl ⊢D∈PsMet⁡X∧A∈X∧B∈X→ADB=0↔A∈X∧B∈X∧ADB=0
15 9 12 14 3bitr4d ⊢D∈PsMet⁡X∧A∈X∧B∈X→A~Met⁡DB↔ADB=0