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 ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ ∞MetSp )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
3 1 2 xmsxmet ⊢ ( 𝐾 ∈ ∞MetSp → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) )
4 3 adantr ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) )
5 xmetres ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
6 4 5 syl ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
7 resres ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
8 inxp ⊢ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) )
9 8 reseq2i ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
10 7 9 eqtri ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
11 eqid ⊢ ( 𝐾 ↾s 𝐴 ) = ( 𝐾 ↾s 𝐴 )
12 eqid ⊢ ( dist ‘ 𝐾 ) = ( dist ‘ 𝐾 )
13 11 12 ressds ⊢ ( 𝐴 ∈ 𝑉 → ( dist ‘ 𝐾 ) = ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) )
14 13 adantl ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( dist ‘ 𝐾 ) = ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) )
15 incom ⊢ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( Base ‘ 𝐾 ) )
16 11 1 ressbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
17 16 adantl ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
18 15 17 syl5eq ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
19 18 sqxpeqd ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
20 14 19 reseq12d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
21 10 20 syl5eq ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
22 18 fveq2d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ∞Met ‘ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ∞Met ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
23 6 21 22 3eltr3d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
24 eqid ⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
25 24 1 2 xmstopn ⊢ ( 𝐾 ∈ ∞MetSp → ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
26 25 adantr ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
27 26 oveq1d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
28 inss1 ⊢ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ⊆ ( Base ‘ 𝐾 )
29 xpss12 ⊢ ( ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ⊆ ( Base ‘ 𝐾 ) ∧ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ⊆ ( Base ‘ 𝐾 ) ) → ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ⊆ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
30 28 28 29 mp2an ⊢ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ⊆ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) )
31 resabs1 ⊢ ( ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ⊆ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ) )
32 30 31 ax-mp ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
33 10 32 eqtr4i ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
34 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
35 eqid ⊢ ( MetOpen ‘ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ) = ( MetOpen ‘ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) )
36 33 34 35 metrest ⊢ ( ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) ∧ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ⊆ ( Base ‘ 𝐾 ) ) → ( ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( MetOpen ‘ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ) )
37 4 28 36 sylancl ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( MetOpen ‘ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ) )
38 27 37 eqtrd ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( MetOpen ‘ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ) )
39 xmstps ⊢ ( 𝐾 ∈ ∞MetSp → 𝐾 ∈ TopSp )
40 1 24 tpsuni ⊢ ( 𝐾 ∈ TopSp → ( Base ‘ 𝐾 ) = ∪ ( TopOpen ‘ 𝐾 ) )
41 39 40 syl ⊢ ( 𝐾 ∈ ∞MetSp → ( Base ‘ 𝐾 ) = ∪ ( TopOpen ‘ 𝐾 ) )
42 41 adantr ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( Base ‘ 𝐾 ) = ∪ ( TopOpen ‘ 𝐾 ) )
43 42 ineq2d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( 𝐴 ∩ ∪ ( TopOpen ‘ 𝐾 ) ) )
44 15 43 syl5eq ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ∪ ( TopOpen ‘ 𝐾 ) ) )
45 44 oveq2d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( TopOpen ‘ 𝐾 ) ↾t ( 𝐴 ∩ ∪ ( TopOpen ‘ 𝐾 ) ) ) )
46 1 24 istps ⊢ ( 𝐾 ∈ TopSp ↔ ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
47 39 46 sylib ⊢ ( 𝐾 ∈ ∞MetSp → ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
48 eqid ⊢ ∪ ( TopOpen ‘ 𝐾 ) = ∪ ( TopOpen ‘ 𝐾 )
49 48 restin ⊢ ( ( ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( ( TopOpen ‘ 𝐾 ) ↾t ( 𝐴 ∩ ∪ ( TopOpen ‘ 𝐾 ) ) ) )
50 47 49 sylan ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( ( TopOpen ‘ 𝐾 ) ↾t ( 𝐴 ∩ ∪ ( TopOpen ‘ 𝐾 ) ) ) )
51 45 50 eqtr4d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) )
52 21 fveq2d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( MetOpen ‘ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ) = ( MetOpen ‘ ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ) )
53 38 51 52 3eqtr3d ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( MetOpen ‘ ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ) )
54 11 24 resstopn ⊢ ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( TopOpen ‘ ( 𝐾 ↾s 𝐴 ) )
55 eqid ⊢ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) )
56 eqid ⊢ ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) = ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
57 54 55 56 isxms2 ⊢ ( ( 𝐾 ↾s 𝐴 ) ∈ ∞MetSp ↔ ( ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ∧ ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( MetOpen ‘ ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ) ) )
58 23 53 57 sylanbrc ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ ∞MetSp )