Metamath Proof Explorer

Theorem xmetpsmet

Description: An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion xmetpsmet 
|- ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )

Proof

Step Hyp Ref Expression
1 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
2 xmet0 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ( x D x ) = 0 )
3 3anrot 
 |-  ( ( z e. X /\ x e. X /\ y e. X ) <-> ( x e. X /\ y e. X /\ z e. X ) )
4 xmettri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( z e. X /\ x e. X /\ y e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
5 3 4 sylan2br 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
6 5 3anassrs 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ y e. X ) /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
7 6 ralrimiva 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ y e. X ) -> A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
8 7 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
9 2 8 jca 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
10 9 ralrimiva 
 |-  ( D e. ( *Met ` X ) -> A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
11 elfvex 
 |-  ( D e. ( *Met ` X ) -> X e. _V )
12 ispsmet 
 |-  ( X e. _V -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
13 11 12 syl 
 |-  ( D e. ( *Met ` X ) -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
14 1 10 13 mpbir2and 
 |-  ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )