Proof of Theorem ressms
Step | Hyp | Ref
| Expression |
1 | | msxms 22069 |
. . 3
⊢ (𝐾 ∈ MetSp → 𝐾 ∈
∞MetSp) |
2 | | ressxms 22140 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp) |
3 | 1, 2 | sylan 487 |
. 2
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp) |
4 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
5 | | eqid 2610 |
. . . . . 6
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) |
6 | 4, 5 | msmet 22072 |
. . . . 5
⊢ (𝐾 ∈ MetSp →
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(Met‘(Base‘𝐾))) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈ (Met‘(Base‘𝐾))) |
8 | | metres 21980 |
. . . 4
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
∈ (Met‘(Base‘𝐾)) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)) ∈ (Met‘((Base‘𝐾) ∩ 𝐴))) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)) ∈ (Met‘((Base‘𝐾) ∩ 𝐴))) |
10 | | resres 5329 |
. . . . 5
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
↾ (𝐴 × 𝐴)) = ((dist‘𝐾) ↾ (((Base‘𝐾) × (Base‘𝐾)) ∩ (𝐴 × 𝐴))) |
11 | | inxp 5176 |
. . . . . 6
⊢
(((Base‘𝐾)
× (Base‘𝐾))
∩ (𝐴 × 𝐴)) = (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴)) |
12 | 11 | reseq2i 5314 |
. . . . 5
⊢
((dist‘𝐾)
↾ (((Base‘𝐾)
× (Base‘𝐾))
∩ (𝐴 × 𝐴))) = ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) |
13 | 10, 12 | eqtri 2632 |
. . . 4
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
↾ (𝐴 × 𝐴)) = ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) |
14 | | eqid 2610 |
. . . . . . 7
⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴) |
15 | | eqid 2610 |
. . . . . . 7
⊢
(dist‘𝐾) =
(dist‘𝐾) |
16 | 14, 15 | ressds 15896 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (dist‘𝐾) = (dist‘(𝐾 ↾s 𝐴))) |
17 | 16 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (dist‘𝐾) = (dist‘(𝐾 ↾s 𝐴))) |
18 | | incom 3767 |
. . . . . . 7
⊢
((Base‘𝐾)
∩ 𝐴) = (𝐴 ∩ (Base‘𝐾)) |
19 | 14, 4 | ressbas 15757 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ (Base‘𝐾)) = (Base‘(𝐾 ↾s 𝐴))) |
20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ (Base‘𝐾)) = (Base‘(𝐾 ↾s 𝐴))) |
21 | 18, 20 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → ((Base‘𝐾) ∩ 𝐴) = (Base‘(𝐾 ↾s 𝐴))) |
22 | 21 | sqxpeqd 5065 |
. . . . 5
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴)) = ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) |
23 | 17, 22 | reseq12d 5318 |
. . . 4
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) = ((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
24 | 13, 23 | syl5eq 2656 |
. . 3
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)) = ((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
25 | 21 | fveq2d 6107 |
. . 3
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (Met‘((Base‘𝐾) ∩ 𝐴)) = (Met‘(Base‘(𝐾 ↾s 𝐴)))) |
26 | 9, 24, 25 | 3eltr3d 2702 |
. 2
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → ((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) ∈ (Met‘(Base‘(𝐾 ↾s 𝐴)))) |
27 | | eqid 2610 |
. . . 4
⊢
(TopOpen‘𝐾) =
(TopOpen‘𝐾) |
28 | 14, 27 | resstopn 20800 |
. . 3
⊢
((TopOpen‘𝐾)
↾t 𝐴) =
(TopOpen‘(𝐾
↾s 𝐴)) |
29 | | eqid 2610 |
. . 3
⊢
(Base‘(𝐾
↾s 𝐴)) =
(Base‘(𝐾
↾s 𝐴)) |
30 | | eqid 2610 |
. . 3
⊢
((dist‘(𝐾
↾s 𝐴))
↾ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) =
((dist‘(𝐾
↾s 𝐴))
↾ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) |
31 | 28, 29, 30 | isms 22064 |
. 2
⊢ ((𝐾 ↾s 𝐴) ∈ MetSp ↔ ((𝐾 ↾s 𝐴) ∈ ∞MetSp ∧
((dist‘(𝐾
↾s 𝐴))
↾ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴))))
∈ (Met‘(Base‘(𝐾 ↾s 𝐴))))) |
32 | 3, 26, 31 | sylanbrc 695 |
1
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ MetSp) |