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

Metamath Proof Explorer

Theorem psmetf

Description: The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetf 
|- ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )

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 simpld 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )