Theorem isxmetd

Description: Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by AV, 9-Apr-2024)

	Ref	Expression
Hypotheses	isxmetd.0	|- ( ph -> X e. V )
	isxmetd.1	|- ( ph -> D : ( X X. X ) --> RR* )
	isxmetd.2	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )
	isxmetd.3	|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
Assertion	isxmetd	|- ( ph -> D e. ( *Met ` X ) )

Proof

Step	Hyp	Ref	Expression
1		isxmetd.0	|- ( ph -> X e. V )
2		isxmetd.1	|- ( ph -> D : ( X X. X ) --> RR* )
3		isxmetd.2	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )
4		isxmetd.3	|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
5	4	3exp2	|- ( ph -> ( x e. X -> ( y e. X -> ( z e. X -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
6	5	imp32	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( z e. X -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
7	6	ralrimiv	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
8	3 7	jca	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
9	8	ralrimivva	|- ( ph -> 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 ) ) ) )
10		isxmet	|- ( X e. V -> ( 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 ) ) ) ) ) )
11	1 10	syl	|- ( ph -> ( 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 ) ) ) ) ) )
12	2 9 11	mpbir2and	|- ( ph -> D e. ( *Met ` X ) )