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

Proof

Step Hyp Ref Expression
1 msxms ⊢ ( 𝐾 ∈ MetSp → 𝐾 ∈ ∞MetSp )
2 ressxms ⊢ ( ( 𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ ∞MetSp )
3 1 2 sylan ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ ∞MetSp )
4 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
6 4 5 msmet ⊢ ( 𝐾 ∈ MetSp → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) )
7 6 adantr ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) )
8 metres ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( Met ‘ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
9 7 8 syl ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( Met ‘ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
10 resres ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
11 inxp ⊢ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) )
12 11 reseq2i ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
13 10 12 eqtri ⊢ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
14 eqid ⊢ ( 𝐾 ↾s 𝐴 ) = ( 𝐾 ↾s 𝐴 )
15 eqid ⊢ ( dist ‘ 𝐾 ) = ( dist ‘ 𝐾 )
16 14 15 ressds ⊢ ( 𝐴 ∈ 𝑉 → ( dist ‘ 𝐾 ) = ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) )
17 16 adantl ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( dist ‘ 𝐾 ) = ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) )
18 incom ⊢ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( Base ‘ 𝐾 ) )
19 14 4 ressbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
20 19 adantl ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
21 18 20 syl5eq ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
22 21 sqxpeqd ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
23 17 22 reseq12d ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( dist ‘ 𝐾 ) ↾ ( ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) × ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) ) = ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
24 13 23 syl5eq ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
25 21 fveq2d ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( Met ‘ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( Met ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
26 9 24 25 3eltr3d ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
27 eqid ⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
28 14 27 resstopn ⊢ ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( TopOpen ‘ ( 𝐾 ↾s 𝐴 ) )
29 eqid ⊢ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) )
30 eqid ⊢ ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) = ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
31 28 29 30 isms ⊢ ( ( 𝐾 ↾s 𝐴 ) ∈ MetSp ↔ ( ( 𝐾 ↾s 𝐴 ) ∈ ∞MetSp ∧ ( ( dist ‘ ( 𝐾 ↾s 𝐴 ) ) ↾ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
32 3 26 31 sylanbrc ⊢ ( ( 𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ MetSp )