Step | Hyp | Ref
| Expression |
1 | | efmndtmd.g |
. . 3
β’ π = (EndoFMndβπ΄) |
2 | 1 | efmndmnd 18806 |
. 2
β’ (π΄ β π β π β Mnd) |
3 | | eqid 2730 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
4 | 1, 3 | efmndtopn 18800 |
. . . 4
β’ (π΄ β π β ((βtβ(π΄ Γ {π« π΄})) βΎt
(Baseβπ)) =
(TopOpenβπ)) |
5 | | distopon 22720 |
. . . . . 6
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) |
6 | | eqid 2730 |
. . . . . . 7
β’
(βtβ(π΄ Γ {π« π΄})) = (βtβ(π΄ Γ {π« π΄})) |
7 | 6 | pttoponconst 23321 |
. . . . . 6
β’ ((π΄ β π β§ π« π΄ β (TopOnβπ΄)) β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
8 | 5, 7 | mpdan 683 |
. . . . 5
β’ (π΄ β π β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
9 | 1, 3 | efmndbas 18788 |
. . . . . . . . 9
β’
(Baseβπ) =
(π΄ βm π΄) |
10 | 9 | eleq2i 2823 |
. . . . . . . 8
β’ (π₯ β (Baseβπ) β π₯ β (π΄ βm π΄)) |
11 | 10 | biimpi 215 |
. . . . . . 7
β’ (π₯ β (Baseβπ) β π₯ β (π΄ βm π΄)) |
12 | 11 | a1i 11 |
. . . . . 6
β’ (π΄ β π β (π₯ β (Baseβπ) β π₯ β (π΄ βm π΄))) |
13 | 12 | ssrdv 3987 |
. . . . 5
β’ (π΄ β π β (Baseβπ) β (π΄ βm π΄)) |
14 | | resttopon 22885 |
. . . . 5
β’
(((βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄)) β§ (Baseβπ) β (π΄ βm π΄)) β ((βtβ(π΄ Γ {π« π΄})) βΎt
(Baseβπ)) β
(TopOnβ(Baseβπ))) |
15 | 8, 13, 14 | syl2anc 582 |
. . . 4
β’ (π΄ β π β ((βtβ(π΄ Γ {π« π΄})) βΎt
(Baseβπ)) β
(TopOnβ(Baseβπ))) |
16 | 4, 15 | eqeltrrd 2832 |
. . 3
β’ (π΄ β π β (TopOpenβπ) β (TopOnβ(Baseβπ))) |
17 | | eqid 2730 |
. . . 4
β’
(TopOpenβπ) =
(TopOpenβπ) |
18 | 3, 17 | istps 22656 |
. . 3
β’ (π β TopSp β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
19 | 16, 18 | sylibr 233 |
. 2
β’ (π΄ β π β π β TopSp) |
20 | | eqid 2730 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
21 | 1, 3, 20 | efmndplusg 18797 |
. . . . . 6
β’
(+gβπ) = (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯ β π¦)) |
22 | | eqid 2730 |
. . . . . . 7
β’
((π« π΄
βko π« π΄) βΎt (Baseβπ)) = ((π« π΄ βko π«
π΄) βΎt
(Baseβπ)) |
23 | | distop 22718 |
. . . . . . . 8
β’ (π΄ β π β π« π΄ β Top) |
24 | | eqid 2730 |
. . . . . . . . 9
β’
(π« π΄
βko π« π΄) = (π« π΄ βko π« π΄) |
25 | 24 | xkotopon 23324 |
. . . . . . . 8
β’
((π« π΄ β
Top β§ π« π΄
β Top) β (π« π΄ βko π« π΄) β (TopOnβ(π«
π΄ Cn π« π΄))) |
26 | 23, 23, 25 | syl2anc 582 |
. . . . . . 7
β’ (π΄ β π β (π« π΄ βko π« π΄) β (TopOnβ(π«
π΄ Cn π« π΄))) |
27 | | cndis 23015 |
. . . . . . . . 9
β’ ((π΄ β π β§ π« π΄ β (TopOnβπ΄)) β (π« π΄ Cn π« π΄) = (π΄ βm π΄)) |
28 | 5, 27 | mpdan 683 |
. . . . . . . 8
β’ (π΄ β π β (π« π΄ Cn π« π΄) = (π΄ βm π΄)) |
29 | 13, 28 | sseqtrrd 4022 |
. . . . . . 7
β’ (π΄ β π β (Baseβπ) β (π« π΄ Cn π« π΄)) |
30 | | disllycmp 23222 |
. . . . . . . . 9
β’ (π΄ β π β π« π΄ β Locally Comp) |
31 | | llynlly 23201 |
. . . . . . . . 9
β’
(π« π΄ β
Locally Comp β π« π΄ β π-Locally
Comp) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
β’ (π΄ β π β π« π΄ β π-Locally
Comp) |
33 | | eqid 2730 |
. . . . . . . . 9
β’ (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) = (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) |
34 | 33 | xkococn 23384 |
. . . . . . . 8
β’
((π« π΄ β
Top β§ π« π΄
β π-Locally Comp β§ π« π΄ β Top) β (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) β (((π« π΄ βko π« π΄) Γt (π«
π΄ βko
π« π΄)) Cn (π«
π΄ βko
π« π΄))) |
35 | 23, 32, 23, 34 | syl3anc 1369 |
. . . . . . 7
β’ (π΄ β π β (π₯ β (π« π΄ Cn π« π΄), π¦ β (π« π΄ Cn π« π΄) β¦ (π₯ β π¦)) β (((π« π΄ βko π« π΄) Γt (π«
π΄ βko
π« π΄)) Cn (π«
π΄ βko
π« π΄))) |
36 | 22, 26, 29, 22, 26, 29, 35 | cnmpt2res 23401 |
. . . . . 6
β’ (π΄ β π β (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯ β π¦)) β ((((π« π΄ βko π« π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) Cn
(π« π΄
βko π« π΄))) |
37 | 21, 36 | eqeltrid 2835 |
. . . . 5
β’ (π΄ β π β (+gβπ) β ((((π« π΄ βko π«
π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) Cn
(π« π΄
βko π« π΄))) |
38 | | xkopt 23379 |
. . . . . . . . . 10
β’
((π« π΄ β
Top β§ π΄ β π) β (π« π΄ βko π«
π΄) =
(βtβ(π΄ Γ {π« π΄}))) |
39 | 23, 38 | mpancom 684 |
. . . . . . . . 9
β’ (π΄ β π β (π« π΄ βko π« π΄) =
(βtβ(π΄ Γ {π« π΄}))) |
40 | 39 | oveq1d 7426 |
. . . . . . . 8
β’ (π΄ β π β ((π« π΄ βko π« π΄) βΎt
(Baseβπ)) =
((βtβ(π΄ Γ {π« π΄})) βΎt (Baseβπ))) |
41 | 40, 4 | eqtrd 2770 |
. . . . . . 7
β’ (π΄ β π β ((π« π΄ βko π« π΄) βΎt
(Baseβπ)) =
(TopOpenβπ)) |
42 | 41, 41 | oveq12d 7429 |
. . . . . 6
β’ (π΄ β π β (((π« π΄ βko π« π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) =
((TopOpenβπ)
Γt (TopOpenβπ))) |
43 | 42 | oveq1d 7426 |
. . . . 5
β’ (π΄ β π β ((((π« π΄ βko π« π΄) βΎt
(Baseβπ))
Γt ((π« π΄ βko π« π΄) βΎt
(Baseβπ))) Cn
(π« π΄
βko π« π΄)) = (((TopOpenβπ) Γt (TopOpenβπ)) Cn (π« π΄ βko π«
π΄))) |
44 | 37, 43 | eleqtrd 2833 |
. . . 4
β’ (π΄ β π β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(π« π΄
βko π« π΄))) |
45 | | vex 3476 |
. . . . . . . . . . 11
β’ π₯ β V |
46 | | vex 3476 |
. . . . . . . . . . 11
β’ π¦ β V |
47 | 45, 46 | coex 7923 |
. . . . . . . . . 10
β’ (π₯ β π¦) β V |
48 | 21, 47 | fnmpoi 8058 |
. . . . . . . . 9
β’
(+gβπ) Fn ((Baseβπ) Γ (Baseβπ)) |
49 | | eqid 2730 |
. . . . . . . . . 10
β’
(+πβπ) = (+πβπ) |
50 | 3, 20, 49 | plusfeq 18573 |
. . . . . . . . 9
β’
((+gβπ) Fn ((Baseβπ) Γ (Baseβπ)) β (+πβπ) = (+gβπ)) |
51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
β’
(+πβπ) = (+gβπ) |
52 | 51 | eqcomi 2739 |
. . . . . . 7
β’
(+gβπ) = (+πβπ) |
53 | 3, 52 | mndplusf 18677 |
. . . . . 6
β’ (π β Mnd β
(+gβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ)) |
54 | | frn 6723 |
. . . . . 6
β’
((+gβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ) β ran (+gβπ) β (Baseβπ)) |
55 | 2, 53, 54 | 3syl 18 |
. . . . 5
β’ (π΄ β π β ran (+gβπ) β (Baseβπ)) |
56 | | cnrest2 23010 |
. . . . 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 1369 |
. . . 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 7427 |
. . 3
β’ (π΄ β π β (((TopOpenβπ) Γt (TopOpenβπ)) Cn ((π« π΄ βko π«
π΄) βΎt
(Baseβπ))) =
(((TopOpenβπ)
Γt (TopOpenβπ)) Cn (TopOpenβπ))) |
60 | 58, 59 | eleqtrd 2833 |
. 2
β’ (π΄ β π β (+gβπ) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(TopOpenβπ))) |
61 | 52, 17 | istmd 23798 |
. 2
β’ (π β TopMnd β (π β Mnd β§ π β TopSp β§
(+gβπ)
β (((TopOpenβπ)
Γt (TopOpenβπ)) Cn (TopOpenβπ)))) |
62 | 2, 19, 60, 61 | syl3anbrc 1341 |
1
β’ (π΄ β π β π β TopMnd) |