This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )