Metamath Proof Explorer

Theorem ressms

Description: The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ressms 
|- ( ( K e. MetSp /\ A e. V ) -> ( K |`s A ) e. MetSp )

Proof

Step Hyp Ref Expression
1 msxms 
 |-  ( K e. MetSp -> K e. *MetSp )
2 ressxms 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( K |`s A ) e. *MetSp )
3 1 2 sylan 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( K |`s A ) e. *MetSp )
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
6 4 5 msmet 
 |-  ( K e. MetSp -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) )
7 6 adantr 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) )
8 metres 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) e. ( Met ` ( ( Base ` K ) i^i A ) ) )
9 7 8 syl 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) e. ( Met ` ( ( Base ` K ) i^i A ) ) )
10 resres 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) )
11 inxp 
 |-  ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) = ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) )
12 11 reseq2i 
 |-  ( ( dist ` K ) |` ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
13 10 12 eqtri 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
14 eqid 
 |-  ( K |`s A ) = ( K |`s A )
15 eqid 
 |-  ( dist ` K ) = ( dist ` K )
16 14 15 ressds 
 |-  ( A e. V -> ( dist ` K ) = ( dist ` ( K |`s A ) ) )
17 16 adantl 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( dist ` K ) = ( dist ` ( K |`s A ) ) )
18 incom 
 |-  ( ( Base ` K ) i^i A ) = ( A i^i ( Base ` K ) )
19 14 4 ressbas 
 |-  ( A e. V -> ( A i^i ( Base ` K ) ) = ( Base ` ( K |`s A ) ) )
20 19 adantl 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( A i^i ( Base ` K ) ) = ( Base ` ( K |`s A ) ) )
21 18 20 syl5eq 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( Base ` K ) i^i A ) = ( Base ` ( K |`s A ) ) )
22 21 sqxpeqd 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) = ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
23 17 22 reseq12d 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) = ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
24 13 23 syl5eq 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
25 21 fveq2d 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( Met ` ( ( Base ` K ) i^i A ) ) = ( Met ` ( Base ` ( K |`s A ) ) ) )
26 9 24 25 3eltr3d 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) e. ( Met ` ( Base ` ( K |`s A ) ) ) )
27 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
28 14 27 resstopn 
 |-  ( ( TopOpen ` K ) |`t A ) = ( TopOpen ` ( K |`s A ) )
29 eqid 
 |-  ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
30 eqid 
 |-  ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
31 28 29 30 isms 
 |-  ( ( K |`s A ) e. MetSp <-> ( ( K |`s A ) e. *MetSp /\ ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) e. ( Met ` ( Base ` ( K |`s A ) ) ) ) )
32 3 26 31 sylanbrc 
 |-  ( ( K e. MetSp /\ A e. V ) -> ( K |`s A ) e. MetSp )