Metamath Proof Explorer


Theorem psmet0

Description: The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmet0
|- ( ( D e. ( PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 )

Proof

Step Hyp Ref Expression
1 elfvex
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
2 ispsmet
 |-  ( X e. _V -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) ) )
3 1 2 syl
 |-  ( D e. ( PsMet ` X ) -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) ) )
4 3 ibi
 |-  ( D e. ( PsMet ` X ) -> ( D : ( X X. X ) --> RR* /\ A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) )
5 4 simprd
 |-  ( D e. ( PsMet ` X ) -> A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) )
6 5 r19.21bi
 |-  ( ( D e. ( PsMet ` X ) /\ a e. X ) -> ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) )
7 6 simpld
 |-  ( ( D e. ( PsMet ` X ) /\ a e. X ) -> ( a D a ) = 0 )
8 7 ralrimiva
 |-  ( D e. ( PsMet ` X ) -> A. a e. X ( a D a ) = 0 )
9 id
 |-  ( a = A -> a = A )
10 9 9 oveq12d
 |-  ( a = A -> ( a D a ) = ( A D A ) )
11 10 eqeq1d
 |-  ( a = A -> ( ( a D a ) = 0 <-> ( A D A ) = 0 ) )
12 11 rspcv
 |-  ( A e. X -> ( A. a e. X ( a D a ) = 0 -> ( A D A ) = 0 ) )
13 8 12 mpan9
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 )