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