Step | Hyp | Ref
| Expression |
1 | | cmsss.x |
. . . . 5
β’ π = (Baseβπ) |
2 | | eqid 2737 |
. . . . 5
β’
((distβπ)
βΎ (π Γ π)) = ((distβπ) βΎ (π Γ π)) |
3 | 1, 2 | msmet 23813 |
. . . 4
β’ (π β MetSp β
((distβπ) βΎ
(π Γ π)) β (Metβπ)) |
4 | 3 | 3ad2ant1 1134 |
. . 3
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β ((distβπ) βΎ (π Γ π)) β (Metβπ)) |
5 | | xpss12 5649 |
. . . . . . . 8
β’ ((π΄ β π β§ π΄ β π) β (π΄ Γ π΄) β (π Γ π)) |
6 | 5 | anidms 568 |
. . . . . . 7
β’ (π΄ β π β (π΄ Γ π΄) β (π Γ π)) |
7 | 6 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β (π΄ Γ π΄) β (π Γ π)) |
8 | 7 | resabs1d 5969 |
. . . . 5
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β (((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) = ((distβπ) βΎ (π΄ Γ π΄))) |
9 | 1 | sseq2i 3974 |
. . . . . . . . 9
β’ (π΄ β π β π΄ β (Baseβπ)) |
10 | | fvex 6856 |
. . . . . . . . . 10
β’
(Baseβπ)
β V |
11 | 10 | ssex 5279 |
. . . . . . . . 9
β’ (π΄ β (Baseβπ) β π΄ β V) |
12 | 9, 11 | sylbi 216 |
. . . . . . . 8
β’ (π΄ β π β π΄ β V) |
13 | 12 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β π΄ β V) |
14 | | cmsss.h |
. . . . . . . 8
β’ πΎ = (π βΎs π΄) |
15 | | eqid 2737 |
. . . . . . . 8
β’
(distβπ) =
(distβπ) |
16 | 14, 15 | ressds 17292 |
. . . . . . 7
β’ (π΄ β V β
(distβπ) =
(distβπΎ)) |
17 | 13, 16 | syl 17 |
. . . . . 6
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β (distβπ) = (distβπΎ)) |
18 | 17 | reseq1d 5937 |
. . . . 5
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β ((distβπ) βΎ (π΄ Γ π΄)) = ((distβπΎ) βΎ (π΄ Γ π΄))) |
19 | 8, 18 | eqtrd 2777 |
. . . 4
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β (((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) = ((distβπΎ) βΎ (π΄ Γ π΄))) |
20 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
21 | | eqid 2737 |
. . . . . . . 8
β’
((distβπΎ)
βΎ ((BaseβπΎ)
Γ (BaseβπΎ))) =
((distβπΎ) βΎ
((BaseβπΎ) Γ
(BaseβπΎ))) |
22 | 20, 21 | iscms 24712 |
. . . . . . 7
β’ (πΎ β CMetSp β (πΎ β MetSp β§
((distβπΎ) βΎ
((BaseβπΎ) Γ
(BaseβπΎ))) β
(CMetβ(BaseβπΎ)))) |
23 | 14, 1 | ressbas2 17121 |
. . . . . . . . . . . . . 14
β’ (π΄ β π β π΄ = (BaseβπΎ)) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ πΎ β MetSp) β π΄ = (BaseβπΎ)) |
25 | 24 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ πΎ β MetSp) β (BaseβπΎ) = π΄) |
26 | 25 | sqxpeqd 5666 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ πΎ β MetSp) β ((BaseβπΎ) Γ (BaseβπΎ)) = (π΄ Γ π΄)) |
27 | 26 | reseq2d 5938 |
. . . . . . . . . 10
β’ ((π΄ β π β§ πΎ β MetSp) β ((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) = ((distβπΎ) βΎ (π΄ Γ π΄))) |
28 | 25 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π΄ β π β§ πΎ β MetSp) β
(CMetβ(BaseβπΎ))
= (CMetβπ΄)) |
29 | 27, 28 | eleq12d 2832 |
. . . . . . . . 9
β’ ((π΄ β π β§ πΎ β MetSp) β (((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) β
(CMetβ(BaseβπΎ))
β ((distβπΎ)
βΎ (π΄ Γ π΄)) β (CMetβπ΄))) |
30 | 29 | biimpd 228 |
. . . . . . . 8
β’ ((π΄ β π β§ πΎ β MetSp) β (((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) β
(CMetβ(BaseβπΎ))
β ((distβπΎ)
βΎ (π΄ Γ π΄)) β (CMetβπ΄))) |
31 | 30 | expimpd 455 |
. . . . . . 7
β’ (π΄ β π β ((πΎ β MetSp β§ ((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) β
(CMetβ(BaseβπΎ))) β ((distβπΎ) βΎ (π΄ Γ π΄)) β (CMetβπ΄))) |
32 | 22, 31 | biimtrid 241 |
. . . . . 6
β’ (π΄ β π β (πΎ β CMetSp β ((distβπΎ) βΎ (π΄ Γ π΄)) β (CMetβπ΄))) |
33 | 32 | imp 408 |
. . . . 5
β’ ((π΄ β π β§ πΎ β CMetSp) β ((distβπΎ) βΎ (π΄ Γ π΄)) β (CMetβπ΄)) |
34 | 33 | 3adant1 1131 |
. . . 4
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β ((distβπΎ) βΎ (π΄ Γ π΄)) β (CMetβπ΄)) |
35 | 19, 34 | eqeltrd 2838 |
. . 3
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β (((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) β (CMetβπ΄)) |
36 | | eqid 2737 |
. . . 4
β’
(MetOpenβ((distβπ) βΎ (π Γ π))) = (MetOpenβ((distβπ) βΎ (π Γ π))) |
37 | 36 | metsscmetcld 24682 |
. . 3
β’
((((distβπ)
βΎ (π Γ π)) β (Metβπ) β§ (((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) β (CMetβπ΄)) β π΄ β
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π))))) |
38 | 4, 35, 37 | syl2anc 585 |
. 2
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β π΄ β
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π))))) |
39 | | cmsss.j |
. . . . 5
β’ π½ = (TopOpenβπ) |
40 | 39, 1, 2 | mstopn 23808 |
. . . 4
β’ (π β MetSp β π½ =
(MetOpenβ((distβπ) βΎ (π Γ π)))) |
41 | 40 | 3ad2ant1 1134 |
. . 3
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β π½ = (MetOpenβ((distβπ) βΎ (π Γ π)))) |
42 | 41 | fveq2d 6847 |
. 2
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β (Clsdβπ½) =
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π))))) |
43 | 38, 42 | eleqtrrd 2841 |
1
β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β π΄ β (Clsdβπ½)) |