Step | Hyp | Ref
| Expression |
1 | | knoppcnlem10.f |
. . . 4
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) |
2 | | simpr 484 |
. . . 4
β’ ((π β§ π§ β β) β π§ β β) |
3 | | knoppcnlem10.2 |
. . . . 5
β’ (π β π β
β0) |
4 | 3 | adantr 480 |
. . . 4
β’ ((π β§ π§ β β) β π β
β0) |
5 | 1, 2, 4 | knoppcnlem1 35891 |
. . 3
β’ ((π β§ π§ β β) β ((πΉβπ§)βπ) = ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π§)))) |
6 | 5 | mpteq2dva 5242 |
. 2
β’ (π β (π§ β β β¦ ((πΉβπ§)βπ)) = (π§ β β β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π§))))) |
7 | | retopon 24654 |
. . . 4
β’
(topGenβran (,)) β (TopOnββ) |
8 | 7 | a1i 11 |
. . 3
β’ (π β (topGenβran (,))
β (TopOnββ)) |
9 | | eqid 2727 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
10 | 9 | cnfldtopon 24673 |
. . . . 5
β’
(TopOpenββfld) β
(TopOnββ) |
11 | 10 | a1i 11 |
. . . 4
β’ (π β
(TopOpenββfld) β
(TopOnββ)) |
12 | | knoppcnlem10.1 |
. . . . . 6
β’ (π β πΆ β β) |
13 | 12 | recnd 11258 |
. . . . 5
β’ (π β πΆ β β) |
14 | 13, 3 | expcld 14128 |
. . . 4
β’ (π β (πΆβπ) β β) |
15 | 8, 11, 14 | cnmptc 23540 |
. . 3
β’ (π β (π§ β β β¦ (πΆβπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
16 | | 2cnd 12306 |
. . . . . . . . . 10
β’ (π β 2 β
β) |
17 | | knoppcnlem10.n |
. . . . . . . . . . 11
β’ (π β π β β) |
18 | 17 | nncnd 12244 |
. . . . . . . . . 10
β’ (π β π β β) |
19 | 16, 18 | mulcld 11250 |
. . . . . . . . 9
β’ (π β (2 Β· π) β
β) |
20 | 19, 3 | expcld 14128 |
. . . . . . . 8
β’ (π β ((2 Β· π)βπ) β β) |
21 | 8, 11, 20 | cnmptc 23540 |
. . . . . . 7
β’ (π β (π§ β β β¦ ((2 Β· π)βπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
22 | 9 | tgioo2 24693 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
23 | 22 | oveq2i 7425 |
. . . . . . . . 9
β’
((topGenβran (,)) Cn (topGenβran (,))) = ((topGenβran
(,)) Cn ((TopOpenββfld) βΎt
β)) |
24 | 9 | cnfldtop 24674 |
. . . . . . . . . 10
β’
(TopOpenββfld) β Top |
25 | | cnrest2r 23165 |
. . . . . . . . . 10
β’
((TopOpenββfld) β Top β
((topGenβran (,)) Cn ((TopOpenββfld)
βΎt β)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . 9
β’
((topGenβran (,)) Cn ((TopOpenββfld)
βΎt β)) β ((topGenβran (,)) Cn
(TopOpenββfld)) |
27 | 23, 26 | eqsstri 4012 |
. . . . . . . 8
β’
((topGenβran (,)) Cn (topGenβran (,))) β
((topGenβran (,)) Cn
(TopOpenββfld)) |
28 | 8 | cnmptid 23539 |
. . . . . . . 8
β’ (π β (π§ β β β¦ π§) β ((topGenβran (,)) Cn
(topGenβran (,)))) |
29 | 27, 28 | sselid 3976 |
. . . . . . 7
β’ (π β (π§ β β β¦ π§) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
30 | 9 | mpomulcn 24759 |
. . . . . . . 8
β’ (π’ β β, π£ β β β¦ (π’ Β· π£)) β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
31 | 30 | a1i 11 |
. . . . . . 7
β’ (π β (π’ β β, π£ β β β¦ (π’ Β· π£)) β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
32 | | oveq12 7423 |
. . . . . . 7
β’ ((π’ = ((2 Β· π)βπ) β§ π£ = π§) β (π’ Β· π£) = (((2 Β· π)βπ) Β· π§)) |
33 | 8, 21, 29, 11, 11, 31, 32 | cnmpt12 23545 |
. . . . . 6
β’ (π β (π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
34 | | 2re 12302 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
35 | 34 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 2 β
β) |
36 | 17 | nnred 12243 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
37 | 35, 36 | remulcld 11260 |
. . . . . . . . . . . 12
β’ (π β (2 Β· π) β
β) |
38 | 37, 3 | reexpcld 14145 |
. . . . . . . . . . 11
β’ (π β ((2 Β· π)βπ) β β) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β ((2 Β· π)βπ) β β) |
40 | 39, 2 | remulcld 11260 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β (((2 Β· π)βπ) Β· π§) β β) |
41 | 40 | fmpttd 7119 |
. . . . . . . 8
β’ (π β (π§ β β β¦ (((2 Β· π)βπ) Β· π§)):ββΆβ) |
42 | 41 | frnd 6724 |
. . . . . . 7
β’ (π β ran (π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β β) |
43 | | ax-resscn 11181 |
. . . . . . . 8
β’ β
β β |
44 | 43 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
45 | | cnrest2 23164 |
. . . . . . 7
β’
(((TopOpenββfld) β (TopOnββ)
β§ ran (π§ β β
β¦ (((2 Β· π)βπ) Β· π§)) β β β§ β β
β) β ((π§ β
β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
(TopOpenββfld)) β (π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
((TopOpenββfld) βΎt
β)))) |
46 | 10, 42, 44, 45 | mp3an2i 1463 |
. . . . . 6
β’ (π β ((π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
(TopOpenββfld)) β (π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
((TopOpenββfld) βΎt
β)))) |
47 | 33, 46 | mpbid 231 |
. . . . 5
β’ (π β (π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
((TopOpenββfld) βΎt
β))) |
48 | 47, 23 | eleqtrrdi 2839 |
. . . 4
β’ (π β (π§ β β β¦ (((2 Β· π)βπ) Β· π§)) β ((topGenβran (,)) Cn
(topGenβran (,)))) |
49 | | ssid 4000 |
. . . . . . 7
β’ β
β β |
50 | | cncfss 24793 |
. . . . . . 7
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
51 | 43, 49, 50 | mp2an 691 |
. . . . . 6
β’
(ββcnββ)
β (ββcnββ) |
52 | | knoppcnlem10.t |
. . . . . . . 8
β’ π = (π₯ β β β¦
(absβ((ββ(π₯ + (1 / 2))) β π₯))) |
53 | 52 | dnicn 35890 |
. . . . . . 7
β’ π β (ββcnββ) |
54 | 53 | a1i 11 |
. . . . . 6
β’ (π β π β (ββcnββ)) |
55 | 51, 54 | sselid 3976 |
. . . . 5
β’ (π β π β (ββcnββ)) |
56 | 10 | toponrestid 22797 |
. . . . . . 7
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
57 | 9, 22, 56 | cncfcn 24804 |
. . . . . 6
β’ ((β
β β β§ β β β) β (ββcnββ) = ((topGenβran (,)) Cn
(TopOpenββfld))) |
58 | 43, 49, 57 | mp2an 691 |
. . . . 5
β’
(ββcnββ) =
((topGenβran (,)) Cn
(TopOpenββfld)) |
59 | 55, 58 | eleqtrdi 2838 |
. . . 4
β’ (π β π β ((topGenβran (,)) Cn
(TopOpenββfld))) |
60 | 8, 48, 59 | cnmpt11f 23542 |
. . 3
β’ (π β (π§ β β β¦ (πβ(((2 Β· π)βπ) Β· π§))) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
61 | | oveq12 7423 |
. . 3
β’ ((π’ = (πΆβπ) β§ π£ = (πβ(((2 Β· π)βπ) Β· π§))) β (π’ Β· π£) = ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π§)))) |
62 | 8, 15, 60, 11, 11, 31, 61 | cnmpt12 23545 |
. 2
β’ (π β (π§ β β β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π§)))) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
63 | 6, 62 | eqeltrd 2828 |
1
β’ (π β (π§ β β β¦ ((πΉβπ§)βπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |