Proof of Theorem ressxms
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | eqid 2738 |
. . . . . 6
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) |
3 | 1, 2 | xmsxmet 23202 |
. . . . 5
⊢ (𝐾 ∈ ∞MetSp →
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(∞Met‘(Base‘𝐾))) |
4 | 3 | adantr 484 |
. . . 4
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈
(∞Met‘(Base‘𝐾))) |
5 | | xmetres 23110 |
. . . 4
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
∈ (∞Met‘(Base‘𝐾)) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)) ∈
(∞Met‘((Base‘𝐾) ∩ 𝐴))) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)) ∈
(∞Met‘((Base‘𝐾) ∩ 𝐴))) |
7 | | resres 5832 |
. . . . 5
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
↾ (𝐴 × 𝐴)) = ((dist‘𝐾) ↾ (((Base‘𝐾) × (Base‘𝐾)) ∩ (𝐴 × 𝐴))) |
8 | | inxp 5669 |
. . . . . 6
⊢
(((Base‘𝐾)
× (Base‘𝐾))
∩ (𝐴 × 𝐴)) = (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴)) |
9 | 8 | reseq2i 5816 |
. . . . 5
⊢
((dist‘𝐾)
↾ (((Base‘𝐾)
× (Base‘𝐾))
∩ (𝐴 × 𝐴))) = ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) |
10 | 7, 9 | eqtri 2761 |
. . . 4
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
↾ (𝐴 × 𝐴)) = ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) |
11 | | eqid 2738 |
. . . . . . 7
⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴) |
12 | | eqid 2738 |
. . . . . . 7
⊢
(dist‘𝐾) =
(dist‘𝐾) |
13 | 11, 12 | ressds 16782 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (dist‘𝐾) = (dist‘(𝐾 ↾s 𝐴))) |
14 | 13 | adantl 485 |
. . . . 5
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (dist‘𝐾) = (dist‘(𝐾 ↾s 𝐴))) |
15 | | incom 4089 |
. . . . . . 7
⊢
((Base‘𝐾)
∩ 𝐴) = (𝐴 ∩ (Base‘𝐾)) |
16 | 11, 1 | ressbas 16650 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ (Base‘𝐾)) = (Base‘(𝐾 ↾s 𝐴))) |
17 | 16 | adantl 485 |
. . . . . . 7
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ (Base‘𝐾)) = (Base‘(𝐾 ↾s 𝐴))) |
18 | 15, 17 | syl5eq 2785 |
. . . . . 6
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((Base‘𝐾) ∩ 𝐴) = (Base‘(𝐾 ↾s 𝐴))) |
19 | 18 | sqxpeqd 5551 |
. . . . 5
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴)) = ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) |
20 | 14, 19 | reseq12d 5820 |
. . . 4
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) = ((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
21 | 10, 20 | syl5eq 2785 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)) = ((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
22 | 18 | fveq2d 6672 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) →
(∞Met‘((Base‘𝐾) ∩ 𝐴)) = (∞Met‘(Base‘(𝐾 ↾s 𝐴)))) |
23 | 6, 21, 22 | 3eltr3d 2847 |
. 2
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) ∈
(∞Met‘(Base‘(𝐾 ↾s 𝐴)))) |
24 | | eqid 2738 |
. . . . . . 7
⊢
(TopOpen‘𝐾) =
(TopOpen‘𝐾) |
25 | 24, 1, 2 | xmstopn 23197 |
. . . . . 6
⊢ (𝐾 ∈ ∞MetSp →
(TopOpen‘𝐾) =
(MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))))) |
26 | 25 | adantr 484 |
. . . . 5
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (TopOpen‘𝐾) = (MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))))) |
27 | 26 | oveq1d 7179 |
. . . 4
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t ((Base‘𝐾) ∩ 𝐴)) = ((MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) ↾t
((Base‘𝐾) ∩ 𝐴))) |
28 | | inss1 4117 |
. . . . 5
⊢
((Base‘𝐾)
∩ 𝐴) ⊆
(Base‘𝐾) |
29 | | xpss12 5534 |
. . . . . . . . 9
⊢
((((Base‘𝐾)
∩ 𝐴) ⊆
(Base‘𝐾) ∧
((Base‘𝐾) ∩ 𝐴) ⊆ (Base‘𝐾)) → (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴)) ⊆ ((Base‘𝐾) × (Base‘𝐾))) |
30 | 28, 28, 29 | mp2an 692 |
. . . . . . . 8
⊢
(((Base‘𝐾)
∩ 𝐴) ×
((Base‘𝐾) ∩ 𝐴)) ⊆ ((Base‘𝐾) × (Base‘𝐾)) |
31 | | resabs1 5849 |
. . . . . . . 8
⊢
((((Base‘𝐾)
∩ 𝐴) ×
((Base‘𝐾) ∩ 𝐴)) ⊆ ((Base‘𝐾) × (Base‘𝐾)) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) = ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴)))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
↾ (((Base‘𝐾)
∩ 𝐴) ×
((Base‘𝐾) ∩ 𝐴))) = ((dist‘𝐾) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) |
33 | 10, 32 | eqtr4i 2764 |
. . . . . 6
⊢
(((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
↾ (𝐴 × 𝐴)) = (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (((Base‘𝐾) ∩ 𝐴) × ((Base‘𝐾) ∩ 𝐴))) |
34 | | eqid 2738 |
. . . . . 6
⊢
(MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) = (MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
35 | | eqid 2738 |
. . . . . 6
⊢
(MetOpen‘(((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴))) = (MetOpen‘(((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴))) |
36 | 33, 34, 35 | metrest 23270 |
. . . . 5
⊢
((((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾)))
∈ (∞Met‘(Base‘𝐾)) ∧ ((Base‘𝐾) ∩ 𝐴) ⊆ (Base‘𝐾)) → ((MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) ↾t
((Base‘𝐾) ∩ 𝐴)) =
(MetOpen‘(((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)))) |
37 | 4, 28, 36 | sylancl 589 |
. . . 4
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((MetOpen‘((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) ↾t
((Base‘𝐾) ∩ 𝐴)) =
(MetOpen‘(((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)))) |
38 | 27, 37 | eqtrd 2773 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t ((Base‘𝐾) ∩ 𝐴)) = (MetOpen‘(((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴)))) |
39 | | xmstps 23199 |
. . . . . . . . 9
⊢ (𝐾 ∈ ∞MetSp →
𝐾 ∈
TopSp) |
40 | 1, 24 | tpsuni 21680 |
. . . . . . . . 9
⊢ (𝐾 ∈ TopSp →
(Base‘𝐾) = ∪ (TopOpen‘𝐾)) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ ∞MetSp →
(Base‘𝐾) = ∪ (TopOpen‘𝐾)) |
42 | 41 | adantr 484 |
. . . . . . 7
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (Base‘𝐾) = ∪
(TopOpen‘𝐾)) |
43 | 42 | ineq2d 4101 |
. . . . . 6
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ (Base‘𝐾)) = (𝐴 ∩ ∪
(TopOpen‘𝐾))) |
44 | 15, 43 | syl5eq 2785 |
. . . . 5
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((Base‘𝐾) ∩ 𝐴) = (𝐴 ∩ ∪
(TopOpen‘𝐾))) |
45 | 44 | oveq2d 7180 |
. . . 4
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t ((Base‘𝐾) ∩ 𝐴)) = ((TopOpen‘𝐾) ↾t (𝐴 ∩ ∪
(TopOpen‘𝐾)))) |
46 | 1, 24 | istps 21678 |
. . . . . 6
⊢ (𝐾 ∈ TopSp ↔
(TopOpen‘𝐾) ∈
(TopOn‘(Base‘𝐾))) |
47 | 39, 46 | sylib 221 |
. . . . 5
⊢ (𝐾 ∈ ∞MetSp →
(TopOpen‘𝐾) ∈
(TopOn‘(Base‘𝐾))) |
48 | | eqid 2738 |
. . . . . 6
⊢ ∪ (TopOpen‘𝐾) = ∪
(TopOpen‘𝐾) |
49 | 48 | restin 21910 |
. . . . 5
⊢
(((TopOpen‘𝐾)
∈ (TopOn‘(Base‘𝐾)) ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t 𝐴) = ((TopOpen‘𝐾) ↾t (𝐴 ∩ ∪
(TopOpen‘𝐾)))) |
50 | 47, 49 | sylan 583 |
. . . 4
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t 𝐴) = ((TopOpen‘𝐾) ↾t (𝐴 ∩ ∪
(TopOpen‘𝐾)))) |
51 | 45, 50 | eqtr4d 2776 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t ((Base‘𝐾) ∩ 𝐴)) = ((TopOpen‘𝐾) ↾t 𝐴)) |
52 | 21 | fveq2d 6672 |
. . 3
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (MetOpen‘(((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ↾ (𝐴 × 𝐴))) = (MetOpen‘((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))) |
53 | 38, 51, 52 | 3eqtr3d 2781 |
. 2
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → ((TopOpen‘𝐾) ↾t 𝐴) = (MetOpen‘((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))) |
54 | 11, 24 | resstopn 21930 |
. . 3
⊢
((TopOpen‘𝐾)
↾t 𝐴) =
(TopOpen‘(𝐾
↾s 𝐴)) |
55 | | eqid 2738 |
. . 3
⊢
(Base‘(𝐾
↾s 𝐴)) =
(Base‘(𝐾
↾s 𝐴)) |
56 | | eqid 2738 |
. . 3
⊢
((dist‘(𝐾
↾s 𝐴))
↾ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) =
((dist‘(𝐾
↾s 𝐴))
↾ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) |
57 | 54, 55, 56 | isxms2 23194 |
. 2
⊢ ((𝐾 ↾s 𝐴) ∈ ∞MetSp ↔
(((dist‘(𝐾
↾s 𝐴))
↾ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴))))
∈ (∞Met‘(Base‘(𝐾 ↾s 𝐴))) ∧ ((TopOpen‘𝐾) ↾t 𝐴) = (MetOpen‘((dist‘(𝐾 ↾s 𝐴)) ↾ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))))) |
58 | 23, 53, 57 | sylanbrc 586 |
1
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp) |