This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressxms

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

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` K ) = ( Base ` K )
2 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
3 1 2 xmsxmet 
 |-  ( K e. *MetSp -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) )
4 3 adantr 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) )
5 xmetres 
 |-  ( ( ( 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 ) ) )
6 4 5 syl 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) e. ( *Met ` ( ( Base ` K ) i^i A ) ) )
7 resres 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) )
8 inxp 
 |-  ( ( ( Base ` K ) X. ( Base ` K ) ) i^i ( A X. A ) ) = ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) )
9 8 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 ) ) )
10 7 9 eqtri 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
11 eqid 
 |-  ( K |`s A ) = ( K |`s A )
12 eqid 
 |-  ( dist ` K ) = ( dist ` K )
13 11 12 ressds 
 |-  ( A e. V -> ( dist ` K ) = ( dist ` ( K |`s A ) ) )
14 13 adantl 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( dist ` K ) = ( dist ` ( K |`s A ) ) )
15 incom 
 |-  ( ( Base ` K ) i^i A ) = ( A i^i ( Base ` K ) )
16 11 1 ressbas 
 |-  ( A e. V -> ( A i^i ( Base ` K ) ) = ( Base ` ( K |`s A ) ) )
17 16 adantl 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( A i^i ( Base ` K ) ) = ( Base ` ( K |`s A ) ) )
18 15 17 eqtrid 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( Base ` K ) i^i A ) = ( Base ` ( K |`s A ) ) )
19 18 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 ) ) ) )
20 14 19 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 ) ) ) ) )
21 10 20 eqtrid 
 |-  ( ( 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 ) ) ) ) )
22 18 fveq2d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( *Met ` ( ( Base ` K ) i^i A ) ) = ( *Met ` ( Base ` ( K |`s A ) ) ) )
23 6 21 22 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 ) ) ) )
24 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
25 24 1 2 xmstopn 
 |-  ( K e. *MetSp -> ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
26 25 adantr 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
27 26 oveq1d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) |`t ( ( Base ` K ) i^i A ) ) )
28 inss1 
 |-  ( ( Base ` K ) i^i A ) C_ ( Base ` K )
29 xpss12 
 |-  ( ( ( ( Base ` K ) i^i A ) C_ ( Base ` K ) /\ ( ( Base ` K ) i^i A ) C_ ( Base ` K ) ) -> ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) C_ ( ( Base ` K ) X. ( Base ` K ) ) )
30 28 28 29 mp2an 
 |-  ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) C_ ( ( Base ` K ) X. ( Base ` K ) )
31 resabs1 
 |-  ( ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) C_ ( ( Base ` K ) X. ( Base ` K ) ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) )
32 30 31 ax-mp 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) ) = ( ( dist ` K ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
33 10 32 eqtr4i 
 |-  ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) = ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( ( ( Base ` K ) i^i A ) X. ( ( Base ` K ) i^i A ) ) )
34 eqid 
 |-  ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
35 eqid 
 |-  ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) )
36 33 34 35 metrest 
 |-  ( ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) /\ ( ( Base ` K ) i^i A ) C_ ( Base ` K ) ) -> ( ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) |`t ( ( Base ` K ) i^i A ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) )
37 4 28 36 sylancl 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) |`t ( ( Base ` K ) i^i A ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) )
38 27 37 eqtrd 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) )
39 xmstps 
 |-  ( K e. *MetSp -> K e. TopSp )
40 1 24 tpsuni 
 |-  ( K e. TopSp -> ( Base ` K ) = U. ( TopOpen ` K ) )
41 39 40 syl 
 |-  ( K e. *MetSp -> ( Base ` K ) = U. ( TopOpen ` K ) )
42 41 adantr 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( Base ` K ) = U. ( TopOpen ` K ) )
43 42 ineq2d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( A i^i ( Base ` K ) ) = ( A i^i U. ( TopOpen ` K ) ) )
44 15 43 eqtrid 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( Base ` K ) i^i A ) = ( A i^i U. ( TopOpen ` K ) ) )
45 44 oveq2d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( TopOpen ` K ) |`t ( A i^i U. ( TopOpen ` K ) ) ) )
46 1 24 istps 
 |-  ( K e. TopSp <-> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
47 39 46 sylib 
 |-  ( K e. *MetSp -> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
48 eqid 
 |-  U. ( TopOpen ` K ) = U. ( TopOpen ` K )
49 48 restin 
 |-  ( ( ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) /\ A e. V ) -> ( ( TopOpen ` K ) |`t A ) = ( ( TopOpen ` K ) |`t ( A i^i U. ( TopOpen ` K ) ) ) )
50 47 49 sylan 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t A ) = ( ( TopOpen ` K ) |`t ( A i^i U. ( TopOpen ` K ) ) ) )
51 45 50 eqtr4d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( TopOpen ` K ) |`t A ) )
52 21 fveq2d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( MetOpen ` ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
53 38 51 52 3eqtr3d 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( ( TopOpen ` K ) |`t A ) = ( MetOpen ` ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) )
54 11 24 resstopn 
 |-  ( ( TopOpen ` K ) |`t A ) = ( TopOpen ` ( K |`s A ) )
55 eqid 
 |-  ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
56 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 ) ) ) )
57 54 55 56 isxms2 
 |-  ( ( K |`s A ) e. *MetSp <-> ( ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) e. ( *Met ` ( Base ` ( K |`s A ) ) ) /\ ( ( TopOpen ` K ) |`t A ) = ( MetOpen ` ( ( dist ` ( K |`s A ) ) |` ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) ) ) )
58 23 53 57 sylanbrc 
 |-  ( ( K e. *MetSp /\ A e. V ) -> ( K |`s A ) e. *MetSp )