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

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
2 isxmet 
 |-  ( X e. dom *Met -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
3 1 2 syl 
 |-  ( D e. ( *Met ` X ) -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
4 3 ibi 
 |-  ( D e. ( *Met ` X ) -> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
5 simpl 
 |-  ( ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) -> ( ( x D y ) = 0 <-> x = y ) )
6 5 2ralimi 
 |-  ( A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) -> A. x e. X A. y e. X ( ( x D y ) = 0 <-> x = y ) )
7 4 6 simpl2im 
 |-  ( D e. ( *Met ` X ) -> A. x e. X A. y e. X ( ( x D y ) = 0 <-> x = y ) )
8 oveq1 
 |-  ( x = A -> ( x D y ) = ( A D y ) )
9 8 eqeq1d 
 |-  ( x = A -> ( ( x D y ) = 0 <-> ( A D y ) = 0 ) )
10 eqeq1 
 |-  ( x = A -> ( x = y <-> A = y ) )
11 9 10 bibi12d 
 |-  ( x = A -> ( ( ( x D y ) = 0 <-> x = y ) <-> ( ( A D y ) = 0 <-> A = y ) ) )
12 oveq2 
 |-  ( y = B -> ( A D y ) = ( A D B ) )
13 12 eqeq1d 
 |-  ( y = B -> ( ( A D y ) = 0 <-> ( A D B ) = 0 ) )
14 eqeq2 
 |-  ( y = B -> ( A = y <-> A = B ) )
15 13 14 bibi12d 
 |-  ( y = B -> ( ( ( A D y ) = 0 <-> A = y ) <-> ( ( A D B ) = 0 <-> A = B ) ) )
16 11 15 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( ( x D y ) = 0 <-> x = y ) -> ( ( A D B ) = 0 <-> A = B ) ) )
17 7 16 syl5com 
 |-  ( D e. ( *Met ` X ) -> ( ( A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) ) )
18 17 3impib 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )