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 ⊢BaseK=BaseK
5 eqid ⊢dist⁡K↾BaseK×BaseK=dist⁡K↾BaseK×BaseK
6 4 5 msmet ⊢K∈MetSp→dist⁡K↾BaseK×BaseK∈Met⁡BaseK
7 6 adantr ⊢K∈MetSp∧A∈V→dist⁡K↾BaseK×BaseK∈Met⁡BaseK
8 metres ⊢dist⁡K↾BaseK×BaseK∈Met⁡BaseK→dist⁡K↾BaseK×BaseK↾A×A∈Met⁡BaseK∩A
9 7 8 syl ⊢K∈MetSp∧A∈V→dist⁡K↾BaseK×BaseK↾A×A∈Met⁡BaseK∩A
10 resres ⊢dist⁡K↾BaseK×BaseK↾A×A=dist⁡K↾BaseK×BaseK∩A×A
11 inxp ⊢BaseK×BaseK∩A×A=BaseK∩A×BaseK∩A
12 11 reseq2i ⊢dist⁡K↾BaseK×BaseK∩A×A=dist⁡K↾BaseK∩A×BaseK∩A
13 10 12 eqtri ⊢dist⁡K↾BaseK×BaseK↾A×A=dist⁡K↾BaseK∩A×BaseK∩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 ⊢BaseK∩A=A∩BaseK
19 14 4 ressbas ⊢A∈V→A∩BaseK=BaseK↾𝑠A
20 19 adantl ⊢K∈MetSp∧A∈V→A∩BaseK=BaseK↾𝑠A
21 18 20 eqtrid ⊢K∈MetSp∧A∈V→BaseK∩A=BaseK↾𝑠A
22 21 sqxpeqd ⊢K∈MetSp∧A∈V→BaseK∩A×BaseK∩A=BaseK↾𝑠A×BaseK↾𝑠A
23 17 22 reseq12d ⊢K∈MetSp∧A∈V→dist⁡K↾BaseK∩A×BaseK∩A=dist⁡K↾𝑠A↾BaseK↾𝑠A×BaseK↾𝑠A
24 13 23 eqtrid ⊢K∈MetSp∧A∈V→dist⁡K↾BaseK×BaseK↾A×A=dist⁡K↾𝑠A↾BaseK↾𝑠A×BaseK↾𝑠A
25 21 fveq2d ⊢K∈MetSp∧A∈V→Met⁡BaseK∩A=Met⁡BaseK↾𝑠A
26 9 24 25 3eltr3d ⊢K∈MetSp∧A∈V→dist⁡K↾𝑠A↾BaseK↾𝑠A×BaseK↾𝑠A∈Met⁡BaseK↾𝑠A
27 eqid ⊢TopOpen⁡K=TopOpen⁡K
28 14 27 resstopn ⊢TopOpen⁡K↾𝑡A=TopOpen⁡K↾𝑠A
29 eqid ⊢BaseK↾𝑠A=BaseK↾𝑠A
30 eqid ⊢dist⁡K↾𝑠A↾BaseK↾𝑠A×BaseK↾𝑠A=dist⁡K↾𝑠A↾BaseK↾𝑠A×BaseK↾𝑠A
31 28 29 30 isms ⊢K↾𝑠A∈MetSp↔K↾𝑠A∈∞MetSp∧dist⁡K↾𝑠A↾BaseK↾𝑠A×BaseK↾𝑠A∈Met⁡BaseK↾𝑠A
32 3 26 31 sylanbrc ⊢K∈MetSp∧A∈V→K↾𝑠A∈MetSp