Step | Hyp | Ref
| Expression |
1 | | cnmpt1vsca.l |
. . . . . . . . . 10
β’ (π β πΏ β (TopOnβπ)) |
2 | | cnmpt2vsca.m |
. . . . . . . . . 10
β’ (π β π β (TopOnβπ)) |
3 | | txtopon 22958 |
. . . . . . . . . 10
β’ ((πΏ β (TopOnβπ) β§ π β (TopOnβπ)) β (πΏ Γt π) β (TopOnβ(π Γ π))) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΏ Γt π) β (TopOnβ(π Γ π))) |
5 | | cnmpt1vsca.w |
. . . . . . . . . . 11
β’ (π β π β TopMod) |
6 | | tlmtrg.f |
. . . . . . . . . . . 12
β’ πΉ = (Scalarβπ) |
7 | 6 | tlmscatps 23558 |
. . . . . . . . . . 11
β’ (π β TopMod β πΉ β TopSp) |
8 | 5, 7 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ β TopSp) |
9 | | eqid 2733 |
. . . . . . . . . . 11
β’
(BaseβπΉ) =
(BaseβπΉ) |
10 | | cnmpt1vsca.k |
. . . . . . . . . . 11
β’ πΎ = (TopOpenβπΉ) |
11 | 9, 10 | istps 22299 |
. . . . . . . . . 10
β’ (πΉ β TopSp β πΎ β
(TopOnβ(BaseβπΉ))) |
12 | 8, 11 | sylib 217 |
. . . . . . . . 9
β’ (π β πΎ β (TopOnβ(BaseβπΉ))) |
13 | | cnmpt2vsca.a |
. . . . . . . . 9
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΏ Γt π) Cn πΎ)) |
14 | | cnf2 22616 |
. . . . . . . . 9
β’ (((πΏ Γt π) β (TopOnβ(π Γ π)) β§ πΎ β (TopOnβ(BaseβπΉ)) β§ (π₯ β π, π¦ β π β¦ π΄) β ((πΏ Γt π) Cn πΎ)) β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆ(BaseβπΉ)) |
15 | 4, 12, 13, 14 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆ(BaseβπΉ)) |
16 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ π΄) = (π₯ β π, π¦ β π β¦ π΄) |
17 | 16 | fmpo 8001 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π π΄ β (BaseβπΉ) β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆ(BaseβπΉ)) |
18 | 15, 17 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β π βπ¦ β π π΄ β (BaseβπΉ)) |
19 | 18 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π π΄ β (BaseβπΉ)) |
20 | 19 | r19.21bi 3233 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β π΄ β (BaseβπΉ)) |
21 | | tlmtps 23555 |
. . . . . . . . . . 11
β’ (π β TopMod β π β TopSp) |
22 | 5, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β π β TopSp) |
23 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
24 | | cnmpt1vsca.j |
. . . . . . . . . . 11
β’ π½ = (TopOpenβπ) |
25 | 23, 24 | istps 22299 |
. . . . . . . . . 10
β’ (π β TopSp β π½ β
(TopOnβ(Baseβπ))) |
26 | 22, 25 | sylib 217 |
. . . . . . . . 9
β’ (π β π½ β (TopOnβ(Baseβπ))) |
27 | | cnmpt2vsca.b |
. . . . . . . . 9
β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΏ Γt π) Cn π½)) |
28 | | cnf2 22616 |
. . . . . . . . 9
β’ (((πΏ Γt π) β (TopOnβ(π Γ π)) β§ π½ β (TopOnβ(Baseβπ)) β§ (π₯ β π, π¦ β π β¦ π΅) β ((πΏ Γt π) Cn π½)) β (π₯ β π, π¦ β π β¦ π΅):(π Γ π)βΆ(Baseβπ)) |
29 | 4, 26, 27, 28 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β π, π¦ β π β¦ π΅):(π Γ π)βΆ(Baseβπ)) |
30 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ π΅) = (π₯ β π, π¦ β π β¦ π΅) |
31 | 30 | fmpo 8001 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π π΅ β (Baseβπ) β (π₯ β π, π¦ β π β¦ π΅):(π Γ π)βΆ(Baseβπ)) |
32 | 29, 31 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β π βπ¦ β π π΅ β (Baseβπ)) |
33 | 32 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π π΅ β (Baseβπ)) |
34 | 33 | r19.21bi 3233 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β π΅ β (Baseβπ)) |
35 | | eqid 2733 |
. . . . . 6
β’ (
Β·sf βπ) = ( Β·sf
βπ) |
36 | | cnmpt1vsca.t |
. . . . . 6
β’ Β· = (
Β·π βπ) |
37 | 23, 6, 9, 35, 36 | scafval 20356 |
. . . . 5
β’ ((π΄ β (BaseβπΉ) β§ π΅ β (Baseβπ)) β (π΄( Β·sf
βπ)π΅) = (π΄ Β· π΅)) |
38 | 20, 34, 37 | syl2anc 585 |
. . . 4
β’ (((π β§ π₯ β π) β§ π¦ β π) β (π΄( Β·sf
βπ)π΅) = (π΄ Β· π΅)) |
39 | 38 | 3impa 1111 |
. . 3
β’ ((π β§ π₯ β π β§ π¦ β π) β (π΄( Β·sf
βπ)π΅) = (π΄ Β· π΅)) |
40 | 39 | mpoeq3dva 7435 |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ (π΄( Β·sf
βπ)π΅)) = (π₯ β π, π¦ β π β¦ (π΄ Β· π΅))) |
41 | 35, 24, 6, 10 | vscacn 23553 |
. . . 4
β’ (π β TopMod β (
Β·sf βπ) β ((πΎ Γt π½) Cn π½)) |
42 | 5, 41 | syl 17 |
. . 3
β’ (π β (
Β·sf βπ) β ((πΎ Γt π½) Cn π½)) |
43 | 1, 2, 13, 27, 42 | cnmpt22f 23042 |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ (π΄( Β·sf
βπ)π΅)) β ((πΏ Γt π) Cn π½)) |
44 | 40, 43 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π, π¦ β π β¦ (π΄ Β· π΅)) β ((πΏ Γt π) Cn π½)) |