Step | Hyp | Ref
| Expression |
1 | | efmndtmd.g |
. . 3
β’ π = (EndoFMndβπ΄) |
2 | 1 | efmndmnd 18707 |
. 2
β’ (π΄ β π β π β Mnd) |
3 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
4 | 1, 3 | efmndtopn 18701 |
. . . 4
β’ (π΄ β π β ((βtβ(π΄ Γ {π« π΄})) βΎt
(Baseβπ)) =
(TopOpenβπ)) |
5 | | distopon 22370 |
. . . . . 6
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) |
6 | | eqid 2733 |
. . . . . . 7
β’
(βtβ(π΄ Γ {π« π΄})) = (βtβ(π΄ Γ {π« π΄})) |
7 | 6 | pttoponconst 22971 |
. . . . . 6
β’ ((π΄ β π β§ π« π΄ β (TopOnβπ΄)) β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
8 | 5, 7 | mpdan 686 |
. . . . 5
β’ (π΄ β π β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
9 | 1, 3 | efmndbas 18689 |
. . . . . . . . 9
β’
(Baseβπ) =
(π΄ βm π΄) |
10 | 9 | eleq2i 2826 |
. . . . . . . 8
β’ (π₯ β (Baseβπ) β π₯ β (π΄ βm π΄)) |
11 | 10 | biimpi 215 |
. . . . . . 7
β’ (π₯ β (Baseβπ) β π₯ β (π΄ βm π΄)) |
12 | 11 | a1i 11 |
. . . . . 6
β’ (π΄ β π β (π₯ β (Baseβπ) β π₯ β (π΄ βm π΄))) |
13 | 12 | ssrdv 3954 |
. . . . 5
β’ (π΄ β π β (Baseβπ) β (π΄ βm π΄)) |
14 | | resttopon 22535 |
. . . . 5
β’
(((βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄)) β§ (Baseβπ) β (π΄ βm π΄)) β ((βtβ(π΄ Γ {π« π΄})) βΎt
(Baseβπ)) β
(TopOnβ(Baseβπ))) |
15 | 8, 13, 14 | syl2anc 585 |
. . . 4
β’ (π΄ β π β ((βtβ(π΄ Γ {π« π΄})) βΎt
(Baseβπ)) β
(TopOnβ(Baseβπ))) |
16 | 4, 15 | eqeltrrd 2835 |
. . 3
β’ (π΄ β π β (TopOpenβπ) β (TopOnβ(Baseβπ))) |
17 | | eqid 2733 |
. . . 4
β’
(TopOpenβπ) =
(TopOpenβπ) |
18 | 3, 17 | istps 22306 |
. . 3
β’ (π β TopSp β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
19 | 16, 18 | sylibr 233 |
. 2
β’ (π΄ β π β π β TopSp) |
20 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
21 | 1, 3, 20 | efmndplusg 18698 |
. . . . . 6
β’
(+gβπ) = (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯ β π¦)) |
22 | | eqid 2733 |
. . . . . . 7
β’
((π« π΄
βko π« π΄) βΎt (Baseβπ)) = ((π« π΄ βko π«
π΄) βΎt
(Baseβπ)) |
23 | | distop 22368 |
. . . . . . . 8
β’ (π΄ β π β π« π΄ β Top) |
24 | | eqid 2733 |
. . . . . . . . 9
β’
(π« π΄
βko π« π΄) = (π« π΄ βko π« π΄) |
25 | 24 | xkotopon 22974 |
. . . . . . . 8
β’
((π« π΄ β
Top β§ π« π΄
β Top) β (π« π΄ βko π« π΄) β (TopOnβ(π«
π΄ Cn π« π΄))) |
26 | 23, 23, 25 | syl2anc 585 |
. . . . . . 7
β’ (π΄ β π β (π« π΄ βko π« π΄) β (TopOnβ(π«
π΄ Cn π« π΄))) |
27 | | cndis 22665 |
. . . . . . . . 9
β’ ((π΄ β π β§ π« π΄ β (TopOnβπ΄)) β (π« π΄ Cn π« π΄) = (π΄ βm π΄)) |
28 | 5, 27 | mpdan 686 |
. . . . . . . 8
β’ (π΄ β π β (π« π΄ Cn π« π΄) = (π΄ βm π΄)) |
29 | 13, 28 | sseqtrrd 3989 |
. . . . . . 7
β’ (π΄ β π β (Baseβπ) β (π« π΄ Cn π« π΄)) |
30 | | disllycmp 22872 |
. . . . . . . . 9
β’ (π΄ β π β π« π΄ β Locally Comp) |
31 | | llynlly 22851 |
. . . . . . . . 9
β’
(π« π΄ β
Locally Comp β π« π΄ β π-Locally
Comp) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
β’ (π΄ β π β π« π΄ β π-Locally
Comp) |
33 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) = (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) |
34 | 33 | xkococn 23034 |
. . . . . . . 8
β’
((π« π΄ β
Top β§ π« π΄
β π-Locally Comp β§ π« π΄ β Top) β (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) β (((π« π΄ βko π« π΄) Γt (π«
π΄ βko
π« π΄)) Cn (π«
π΄ βko
π« π΄))) |
35 | 23, 32, 23, 34 | syl3anc 1372 |
. . . . . . 7
β’ (π΄ β π β (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) β (((π« π΄ βko π« π΄) Γt (π«
π΄ βko
π« π΄)) Cn (π«
π΄ βko
π« π΄))) |
36 | 22, 26, 29, 22, 26, 29, 35 | cnmpt2res 23051 |
. . . . . 6
β’ (π΄ β π β (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯ β π¦)) β ((((π« π΄ βko π« π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) Cn
(π« π΄
βko π« π΄))) |
37 | 21, 36 | eqeltrid 2838 |
. . . . 5
β’ (π΄ β π β (+gβπ) β ((((π« π΄ βko π«
π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) Cn
(π« π΄
βko π« π΄))) |
38 | | xkopt 23029 |
. . . . . . . . . 10
β’
((π« π΄ β
Top β§ π΄ β π) β (π« π΄ βko π«
π΄) =
(βtβ(π΄ Γ {π« π΄}))) |
39 | 23, 38 | mpancom 687 |
. . . . . . . . 9
β’ (π΄ β π β (π« π΄ βko π« π΄) =
(βtβ(π΄ Γ {π« π΄}))) |
40 | 39 | oveq1d 7376 |
. . . . . . . 8
β’ (π΄ β π β ((π« π΄ βko π« π΄) βΎt
(Baseβπ)) =
((βtβ(π΄ Γ {π« π΄})) βΎt (Baseβπ))) |
41 | 40, 4 | eqtrd 2773 |
. . . . . . 7
β’ (π΄ β π β ((π« π΄ βko π« π΄) βΎt
(Baseβπ)) =
(TopOpenβπ)) |
42 | 41, 41 | oveq12d 7379 |
. . . . . 6
β’ (π΄ β π β (((π« π΄ βko π« π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) =
((TopOpenβπ)
Γt (TopOpenβπ))) |
43 | 42 | oveq1d 7376 |
. . . . 5
β’ (π΄ β π β ((((π« π΄ βko π« π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) Cn
(π« π΄
βko π« π΄)) = (((TopOpenβπ) Γt (TopOpenβπ)) Cn (π« π΄ βko π«
π΄))) |
44 | 37, 43 | eleqtrd 2836 |
. . . 4
β’ (π΄ β π β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(π« π΄
βko π« π΄))) |
45 | | vex 3451 |
. . . . . . . . . . 11
β’ π₯ β V |
46 | | vex 3451 |
. . . . . . . . . . 11
β’ π¦ β V |
47 | 45, 46 | coex 7871 |
. . . . . . . . . 10
β’ (π₯ β π¦) β V |
48 | 21, 47 | fnmpoi 8006 |
. . . . . . . . 9
β’
(+gβπ) Fn ((Baseβπ) Γ (Baseβπ)) |
49 | | eqid 2733 |
. . . . . . . . . 10
β’
(+πβπ) = (+πβπ) |
50 | 3, 20, 49 | plusfeq 18513 |
. . . . . . . . 9
β’
((+gβπ) Fn ((Baseβπ) Γ (Baseβπ)) β (+πβπ) = (+gβπ)) |
51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
β’
(+πβπ) = (+gβπ) |
52 | 51 | eqcomi 2742 |
. . . . . . 7
β’
(+gβπ) = (+πβπ) |
53 | 3, 52 | mndplusf 18582 |
. . . . . 6
β’ (π β Mnd β
(+gβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ)) |
54 | | frn 6679 |
. . . . . 6
β’
((+gβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ) β ran (+gβπ) β (Baseβπ)) |
55 | 2, 53, 54 | 3syl 18 |
. . . . 5
β’ (π΄ β π β ran (+gβπ) β (Baseβπ)) |
56 | | cnrest2 22660 |
. . . . 5
β’
(((π« π΄
βko π« π΄) β (TopOnβ(π« π΄ Cn π« π΄)) β§ ran (+gβπ) β (Baseβπ) β§ (Baseβπ) β (π« π΄ Cn π« π΄)) β ((+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(π« π΄
βko π« π΄)) β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
((π« π΄
βko π« π΄) βΎt (Baseβπ))))) |
57 | 26, 55, 29, 56 | syl3anc 1372 |
. . . 4
β’ (π΄ β π β ((+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(π« π΄
βko π« π΄)) β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
((π« π΄
βko π« π΄) βΎt (Baseβπ))))) |
58 | 44, 57 | mpbid 231 |
. . 3
β’ (π΄ β π β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
((π« π΄
βko π« π΄) βΎt (Baseβπ)))) |
59 | 41 | oveq2d 7377 |
. . 3
β’ (π΄ β π β (((TopOpenβπ) Γt (TopOpenβπ)) Cn ((π« π΄ βko π«
π΄) βΎt
(Baseβπ))) =
(((TopOpenβπ)
Γt (TopOpenβπ)) Cn (TopOpenβπ))) |
60 | 58, 59 | eleqtrd 2836 |
. 2
β’ (π΄ β π β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(TopOpenβπ))) |
61 | 52, 17 | istmd 23448 |
. 2
β’ (π β TopMnd β (π β Mnd β§ π β TopSp β§
(+gβπ)
β (((TopOpenβπ)
Γt (TopOpenβπ)) Cn (TopOpenβπ)))) |
62 | 2, 19, 60, 61 | syl3anbrc 1344 |
1
β’ (π΄ β π β π β TopMnd) |