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