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

Proof

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