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

Metamath Proof Explorer

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