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 ) )