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 e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A ( ~Met ` D ) B <-> ( A D B ) = 0 ) )

Proof

Step Hyp Ref Expression
1 eleq1
 |-  ( a = A -> ( a e. X <-> A e. X ) )
2 eleq1
 |-  ( b = B -> ( b e. X <-> B e. X ) )
3 1 2 bi2anan9
 |-  ( ( a = A /\ b = B ) -> ( ( a e. X /\ b e. X ) <-> ( A e. X /\ B e. 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 e. X /\ b e. X ) /\ ( a D b ) = 0 ) <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) )
7 eqid
 |-  { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } = { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) }
8 6 7 brabga
 |-  ( ( A e. X /\ B e. X ) -> ( A { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } B <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) )
9 8 adantl
 |-  ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } B <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) )
10 metidval
 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } )
11 10 adantr
 |-  ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( ~Met ` D ) = { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } )
12 11 breqd
 |-  ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A ( ~Met ` D ) B <-> A { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } B ) )
13 ibar
 |-  ( ( A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) )
14 13 adantl
 |-  ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) = 0 <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) )
15 9 12 14 3bitr4d
 |-  ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A ( ~Met ` D ) B <-> ( A D B ) = 0 ) )