Step | Hyp | Ref
| Expression |
1 | | cnmpt1vsca.l |
. . . . . 6
β’ (π β πΏ β (TopOnβπ)) |
2 | | cnmpt1vsca.w |
. . . . . . . 8
β’ (π β π β TopMod) |
3 | | tlmtrg.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
4 | 3 | tlmscatps 23558 |
. . . . . . . 8
β’ (π β TopMod β πΉ β TopSp) |
5 | 2, 4 | syl 17 |
. . . . . . 7
β’ (π β πΉ β TopSp) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΉ) =
(BaseβπΉ) |
7 | | cnmpt1vsca.k |
. . . . . . . 8
β’ πΎ = (TopOpenβπΉ) |
8 | 6, 7 | istps 22299 |
. . . . . . 7
β’ (πΉ β TopSp β πΎ β
(TopOnβ(BaseβπΉ))) |
9 | 5, 8 | sylib 217 |
. . . . . 6
β’ (π β πΎ β (TopOnβ(BaseβπΉ))) |
10 | | cnmpt1vsca.a |
. . . . . 6
β’ (π β (π₯ β π β¦ π΄) β (πΏ Cn πΎ)) |
11 | | cnf2 22616 |
. . . . . 6
β’ ((πΏ β (TopOnβπ) β§ πΎ β (TopOnβ(BaseβπΉ)) β§ (π₯ β π β¦ π΄) β (πΏ Cn πΎ)) β (π₯ β π β¦ π΄):πβΆ(BaseβπΉ)) |
12 | 1, 9, 10, 11 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β π β¦ π΄):πβΆ(BaseβπΉ)) |
13 | 12 | fvmptelcdm 7062 |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β (BaseβπΉ)) |
14 | | tlmtps 23555 |
. . . . . . . 8
β’ (π β TopMod β π β TopSp) |
15 | 2, 14 | syl 17 |
. . . . . . 7
β’ (π β π β TopSp) |
16 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
17 | | cnmpt1vsca.j |
. . . . . . . 8
β’ π½ = (TopOpenβπ) |
18 | 16, 17 | istps 22299 |
. . . . . . 7
β’ (π β TopSp β π½ β
(TopOnβ(Baseβπ))) |
19 | 15, 18 | sylib 217 |
. . . . . 6
β’ (π β π½ β (TopOnβ(Baseβπ))) |
20 | | cnmpt1vsca.b |
. . . . . 6
β’ (π β (π₯ β π β¦ π΅) β (πΏ Cn π½)) |
21 | | cnf2 22616 |
. . . . . 6
β’ ((πΏ β (TopOnβπ) β§ π½ β (TopOnβ(Baseβπ)) β§ (π₯ β π β¦ π΅) β (πΏ Cn π½)) β (π₯ β π β¦ π΅):πβΆ(Baseβπ)) |
22 | 1, 19, 20, 21 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β π β¦ π΅):πβΆ(Baseβπ)) |
23 | 22 | fvmptelcdm 7062 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β (Baseβπ)) |
24 | | eqid 2733 |
. . . . 5
β’ (
Β·sf βπ) = ( Β·sf
βπ) |
25 | | cnmpt1vsca.t |
. . . . 5
β’ Β· = (
Β·π βπ) |
26 | 16, 3, 6, 24, 25 | scafval 20356 |
. . . 4
β’ ((π΄ β (BaseβπΉ) β§ π΅ β (Baseβπ)) β (π΄( Β·sf
βπ)π΅) = (π΄ Β· π΅)) |
27 | 13, 23, 26 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β π) β (π΄( Β·sf
βπ)π΅) = (π΄ Β· π΅)) |
28 | 27 | mpteq2dva 5206 |
. 2
β’ (π β (π₯ β π β¦ (π΄( Β·sf
βπ)π΅)) = (π₯ β π β¦ (π΄ Β· π΅))) |
29 | 24, 17, 3, 7 | vscacn 23553 |
. . . 4
β’ (π β TopMod β (
Β·sf βπ) β ((πΎ Γt π½) Cn π½)) |
30 | 2, 29 | syl 17 |
. . 3
β’ (π β (
Β·sf βπ) β ((πΎ Γt π½) Cn π½)) |
31 | 1, 10, 20, 30 | cnmpt12f 23033 |
. 2
β’ (π β (π₯ β π β¦ (π΄( Β·sf
βπ)π΅)) β (πΏ Cn π½)) |
32 | 28, 31 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πΏ Cn π½)) |