Metamath Proof Explorer

Theorem xmetres

Description: A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 xmetf 
 |-  ( 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 xmetres2 
 |-  ( ( 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 ) ) )