Metamath Proof Explorer


Theorem metres

Description: A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion metres
|- ( D e. ( Met ` X ) -> ( D |` ( R X. R ) ) e. ( Met ` ( X i^i R ) ) )

Proof

Step Hyp Ref Expression
1 metf
 |-  ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
2 fdm
 |-  ( D : ( X X. X ) --> RR -> dom D = ( X X. X ) )
3 metreslem
 |-  ( dom D = ( X X. X ) -> ( D |` ( R X. R ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )
4 1 2 3 3syl
 |-  ( D e. ( Met ` X ) -> ( D |` ( R X. R ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )
5 inss1
 |-  ( X i^i R ) C_ X
6 metres2
 |-  ( ( D e. ( Met ` X ) /\ ( X i^i R ) C_ X ) -> ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) e. ( Met ` ( X i^i R ) ) )
7 5 6 mpan2
 |-  ( D e. ( Met ` X ) -> ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) e. ( Met ` ( X i^i R ) ) )
8 4 7 eqeltrd
 |-  ( D e. ( Met ` X ) -> ( D |` ( R X. R ) ) e. ( Met ` ( X i^i R ) ) )