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 ∈ MetSp ∧ A ∈ V → K ↾ 𝑠 A ∈ MetSp

Proof

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