Metamath Proof Explorer


Theorem rexmet

Description: The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis remet.1
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion rexmet
|- D e. ( *Met ` RR )

Proof

Step Hyp Ref Expression
1 remet.1
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
2 1 remet
 |-  D e. ( Met ` RR )
3 metxmet
 |-  ( D e. ( Met ` RR ) -> D e. ( *Met ` RR ) )
4 2 3 ax-mp
 |-  D e. ( *Met ` RR )