Step | Hyp | Ref
| Expression |
1 | | elfznn 13526 |
. . . 4
β’ (π β (1...π) β π β β) |
2 | | cvmliftlem.1 |
. . . . 5
β’ π = (π β π½ β¦ {π β (π« πΆ β {β
}) β£ (βͺ π =
(β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β
β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) |
3 | | cvmliftlem.b |
. . . . 5
β’ π΅ = βͺ
πΆ |
4 | | cvmliftlem.x |
. . . . 5
β’ π = βͺ
π½ |
5 | | cvmliftlem.f |
. . . . 5
β’ (π β πΉ β (πΆ CovMap π½)) |
6 | | cvmliftlem.g |
. . . . 5
β’ (π β πΊ β (II Cn π½)) |
7 | | cvmliftlem.p |
. . . . 5
β’ (π β π β π΅) |
8 | | cvmliftlem.e |
. . . . 5
β’ (π β (πΉβπ) = (πΊβ0)) |
9 | | cvmliftlem.n |
. . . . 5
β’ (π β π β β) |
10 | | cvmliftlem.t |
. . . . 5
β’ (π β π:(1...π)βΆβͺ
π β π½ ({π} Γ (πβπ))) |
11 | | cvmliftlem.a |
. . . . 5
β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) |
12 | | cvmliftlem.l |
. . . . 5
β’ πΏ = (topGenβran
(,)) |
13 | | cvmliftlem.q |
. . . . 5
β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0,
{β¨0, πβ©}β©})) |
14 | | eqid 2732 |
. . . . 5
β’ (((π β 1) / π)[,](π / π)) = (((π β 1) / π)[,](π / π)) |
15 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cvmliftlem5 34268 |
. . . 4
β’ ((π β§ π β β) β (πβπ) = (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβπ§)))) |
16 | 1, 15 | sylan2 593 |
. . 3
β’ ((π β§ π β (1...π)) β (πβπ) = (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβπ§)))) |
17 | | simpr 485 |
. . . . 5
β’ (((π β§ π β (1...π)) β§ π§ = ((π β 1) / π)) β π§ = ((π β 1) / π)) |
18 | 17 | fveq2d 6892 |
. . . 4
β’ (((π β§ π β (1...π)) β§ π§ = ((π β 1) / π)) β (πΊβπ§) = (πΊβ((π β 1) / π))) |
19 | 18 | fveq2d 6892 |
. . 3
β’ (((π β§ π β (1...π)) β§ π§ = ((π β 1) / π)) β (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβπ§)) = (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβ((π β 1) / π)))) |
20 | 1 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β β) |
21 | 20 | nnred 12223 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β β) |
22 | | peano2rem 11523 |
. . . . . . 7
β’ (π β β β (π β 1) β
β) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (π β 1) β β) |
24 | 9 | adantr 481 |
. . . . . 6
β’ ((π β§ π β (1...π)) β π β β) |
25 | 23, 24 | nndivred 12262 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((π β 1) / π) β β) |
26 | 25 | rexrd 11260 |
. . . 4
β’ ((π β§ π β (1...π)) β ((π β 1) / π) β
β*) |
27 | 21, 24 | nndivred 12262 |
. . . . 5
β’ ((π β§ π β (1...π)) β (π / π) β β) |
28 | 27 | rexrd 11260 |
. . . 4
β’ ((π β§ π β (1...π)) β (π / π) β
β*) |
29 | 21 | ltm1d 12142 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (π β 1) < π) |
30 | 24 | nnred 12223 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β β) |
31 | 24 | nngt0d 12257 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β 0 < π) |
32 | | ltdiv1 12074 |
. . . . . . 7
β’ (((π β 1) β β β§
π β β β§
(π β β β§ 0
< π)) β ((π β 1) < π β ((π β 1) / π) < (π / π))) |
33 | 23, 21, 30, 31, 32 | syl112anc 1374 |
. . . . . 6
β’ ((π β§ π β (1...π)) β ((π β 1) < π β ((π β 1) / π) < (π / π))) |
34 | 29, 33 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((π β 1) / π) < (π / π)) |
35 | 25, 27, 34 | ltled 11358 |
. . . 4
β’ ((π β§ π β (1...π)) β ((π β 1) / π) β€ (π / π)) |
36 | | lbicc2 13437 |
. . . 4
β’ ((((π β 1) / π) β β* β§ (π / π) β β* β§ ((π β 1) / π) β€ (π / π)) β ((π β 1) / π) β (((π β 1) / π)[,](π / π))) |
37 | 26, 28, 35, 36 | syl3anc 1371 |
. . 3
β’ ((π β§ π β (1...π)) β ((π β 1) / π) β (((π β 1) / π)[,](π / π))) |
38 | | fvexd 6903 |
. . 3
β’ ((π β§ π β (1...π)) β (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβ((π β 1) / π))) β V) |
39 | 16, 19, 37, 38 | fvmptd 7002 |
. 2
β’ ((π β§ π β (1...π)) β ((πβπ)β((π β 1) / π)) = (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβ((π β 1) / π)))) |
40 | 5 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β πΉ β (πΆ CovMap π½)) |
41 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β (1...π)) |
42 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 41 | cvmliftlem1 34264 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (2nd β(πβπ)) β (πβ(1st β(πβπ)))) |
43 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cvmliftlem7 34270 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β ((πβ(π β 1))β((π β 1) / π)) β (β‘πΉ β {(πΊβ((π β 1) / π))})) |
44 | | cvmcn 34241 |
. . . . . . . . . . 11
β’ (πΉ β (πΆ CovMap π½) β πΉ β (πΆ Cn π½)) |
45 | 3, 4 | cnf 22741 |
. . . . . . . . . . 11
β’ (πΉ β (πΆ Cn π½) β πΉ:π΅βΆπ) |
46 | 40, 44, 45 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β πΉ:π΅βΆπ) |
47 | | ffn 6714 |
. . . . . . . . . 10
β’ (πΉ:π΅βΆπ β πΉ Fn π΅) |
48 | | fniniseg 7058 |
. . . . . . . . . 10
β’ (πΉ Fn π΅ β (((πβ(π β 1))β((π β 1) / π)) β (β‘πΉ β {(πΊβ((π β 1) / π))}) β (((πβ(π β 1))β((π β 1) / π)) β π΅ β§ (πΉβ((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π))))) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (((πβ(π β 1))β((π β 1) / π)) β (β‘πΉ β {(πΊβ((π β 1) / π))}) β (((πβ(π β 1))β((π β 1) / π)) β π΅ β§ (πΉβ((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π))))) |
50 | 43, 49 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (((πβ(π β 1))β((π β 1) / π)) β π΅ β§ (πΉβ((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π)))) |
51 | 50 | simpld 495 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((πβ(π β 1))β((π β 1) / π)) β π΅) |
52 | 50 | simprd 496 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (πΉβ((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π))) |
53 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 41, 14, 37 | cvmliftlem3 34266 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (πΊβ((π β 1) / π)) β (1st β(πβπ))) |
54 | 52, 53 | eqeltrd 2833 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πΉβ((πβ(π β 1))β((π β 1) / π))) β (1st β(πβπ))) |
55 | | eqid 2732 |
. . . . . . . 8
β’
(β©π
β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) = (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) |
56 | 2, 3, 55 | cvmsiota 34256 |
. . . . . . 7
β’ ((πΉ β (πΆ CovMap π½) β§ ((2nd β(πβπ)) β (πβ(1st β(πβπ))) β§ ((πβ(π β 1))β((π β 1) / π)) β π΅ β§ (πΉβ((πβ(π β 1))β((π β 1) / π))) β (1st β(πβπ)))) β ((β©π β (2nd
β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) β (2nd β(πβπ)) β§ ((πβ(π β 1))β((π β 1) / π)) β (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))) |
57 | 40, 42, 51, 54, 56 | syl13anc 1372 |
. . . . . 6
β’ ((π β§ π β (1...π)) β ((β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) β (2nd β(πβπ)) β§ ((πβ(π β 1))β((π β 1) / π)) β (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))) |
58 | 57 | simprd 496 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((πβ(π β 1))β((π β 1) / π)) β (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)) |
59 | | fvres 6907 |
. . . . 5
β’ (((πβ(π β 1))β((π β 1) / π)) β (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) β ((πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β((πβ(π β 1))β((π β 1) / π))) = (πΉβ((πβ(π β 1))β((π β 1) / π)))) |
60 | 58, 59 | syl 17 |
. . . 4
β’ ((π β§ π β (1...π)) β ((πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β((πβ(π β 1))β((π β 1) / π))) = (πΉβ((πβ(π β 1))β((π β 1) / π)))) |
61 | 60, 52 | eqtrd 2772 |
. . 3
β’ ((π β§ π β (1...π)) β ((πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π))) |
62 | 57 | simpld 495 |
. . . . 5
β’ ((π β§ π β (1...π)) β (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) β (2nd β(πβπ))) |
63 | 2 | cvmsf1o 34251 |
. . . . 5
β’ ((πΉ β (πΆ CovMap π½) β§ (2nd β(πβπ)) β (πβ(1st β(πβπ))) β§ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π) β (2nd β(πβπ))) β (πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)):(β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)β1-1-ontoβ(1st β(πβπ))) |
64 | 40, 42, 62, 63 | syl3anc 1371 |
. . . 4
β’ ((π β§ π β (1...π)) β (πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)):(β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)β1-1-ontoβ(1st β(πβπ))) |
65 | | f1ocnvfv 7272 |
. . . 4
β’ (((πΉ βΎ (β©π β (2nd
β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)):(β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)β1-1-ontoβ(1st β(πβπ)) β§ ((πβ(π β 1))β((π β 1) / π)) β (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π)) β (((πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π)) β (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβ((π β 1) / π))) = ((πβ(π β 1))β((π β 1) / π)))) |
66 | 64, 58, 65 | syl2anc 584 |
. . 3
β’ ((π β§ π β (1...π)) β (((πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β((πβ(π β 1))β((π β 1) / π))) = (πΊβ((π β 1) / π)) β (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβ((π β 1) / π))) = ((πβ(π β 1))β((π β 1) / π)))) |
67 | 61, 66 | mpd 15 |
. 2
β’ ((π β§ π β (1...π)) β (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβ((π β 1) / π))) = ((πβ(π β 1))β((π β 1) / π))) |
68 | 39, 67 | eqtrd 2772 |
1
β’ ((π β§ π β (1...π)) β ((πβπ)β((π β 1) / π)) = ((πβ(π β 1))β((π β 1) / π))) |