Metamath Proof Explorer


Theorem cvmliftlem6

Description: Lemma for cvmlift . Induction step for cvmliftlem7 . Assuming that Q ( M - 1 ) is defined at ( M - 1 ) / N and is a preimage of G ( ( M - 1 ) / N ) , the next segment Q ( M ) is also defined and is a function on W which is a lift G for this segment. This follows explicitly from the definition Q ( M ) =`' ( F |`I ) o. G since G is in 1st( FM ) for the entire interval so that ` ``' ( F |`I ) maps this into I and F o. Q maps back to G . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
cvmliftlem.b B=C
cvmliftlem.x X=J
cvmliftlem.f φFCCovMapJ
cvmliftlem.g φGIICnJ
cvmliftlem.p φPB
cvmliftlem.e φFP=G0
cvmliftlem.n φN
cvmliftlem.t φT:1NjJj×Sj
cvmliftlem.a φk1NGk1NkN1stTk
cvmliftlem.l L=topGenran.
cvmliftlem.q Q=seq0xV,mzm1NmNFιb2ndTm|xm1Nb-1GzI00P
cvmliftlem5.3 W=M1NMN
cvmliftlem6.1 φψM1N
cvmliftlem6.2 φψQM1M1NF-1GM1N
Assertion cvmliftlem6 φψQM:WBFQM=GW

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
2 cvmliftlem.b B=C
3 cvmliftlem.x X=J
4 cvmliftlem.f φFCCovMapJ
5 cvmliftlem.g φGIICnJ
6 cvmliftlem.p φPB
7 cvmliftlem.e φFP=G0
8 cvmliftlem.n φN
9 cvmliftlem.t φT:1NjJj×Sj
10 cvmliftlem.a φk1NGk1NkN1stTk
11 cvmliftlem.l L=topGenran.
12 cvmliftlem.q Q=seq0xV,mzm1NmNFιb2ndTm|xm1Nb-1GzI00P
13 cvmliftlem5.3 W=M1NMN
14 cvmliftlem6.1 φψM1N
15 cvmliftlem6.2 φψQM1M1NF-1GM1N
16 14 adantrr φψzWM1N
17 1 2 3 4 5 6 7 8 9 10 11 16 cvmliftlem1 φψzW2ndTMS1stTM
18 1 cvmsss 2ndTMS1stTM2ndTMC
19 17 18 syl φψzW2ndTMC
20 4 adantr φψzWFCCovMapJ
21 15 adantrr φψzWQM1M1NF-1GM1N
22 cvmcn FCCovMapJFCCnJ
23 2 3 cnf FCCnJF:BX
24 20 22 23 3syl φψzWF:BX
25 ffn F:BXFFnB
26 fniniseg FFnBQM1M1NF-1GM1NQM1M1NBFQM1M1N=GM1N
27 24 25 26 3syl φψzWQM1M1NF-1GM1NQM1M1NBFQM1M1N=GM1N
28 21 27 mpbid φψzWQM1M1NBFQM1M1N=GM1N
29 28 simpld φψzWQM1M1NB
30 28 simprd φψzWFQM1M1N=GM1N
31 elfznn M1NM
32 16 31 syl φψzWM
33 32 nnred φψzWM
34 peano2rem MM1
35 33 34 syl φψzWM1
36 8 adantr φψzWN
37 35 36 nndivred φψzWM1N
38 37 rexrd φψzWM1N*
39 33 36 nndivred φψzWMN
40 39 rexrd φψzWMN*
41 33 ltm1d φψzWM1<M
42 36 nnred φψzWN
43 36 nngt0d φψzW0<N
44 ltdiv1 M1MN0<NM1<MM1N<MN
45 35 33 42 43 44 syl112anc φψzWM1<MM1N<MN
46 41 45 mpbid φψzWM1N<MN
47 37 39 46 ltled φψzWM1NMN
48 lbicc2 M1N*MN*M1NMNM1NM1NMN
49 38 40 47 48 syl3anc φψzWM1NM1NMN
50 49 13 eleqtrrdi φψzWM1NW
51 1 2 3 4 5 6 7 8 9 10 11 16 13 50 cvmliftlem3 φψzWGM1N1stTM
52 30 51 eqeltrd φψzWFQM1M1N1stTM
53 eqid ιb2ndTM|QM1M1Nb=ιb2ndTM|QM1M1Nb
54 1 2 53 cvmsiota FCCovMapJ2ndTMS1stTMQM1M1NBFQM1M1N1stTMιb2ndTM|QM1M1Nb2ndTMQM1M1Nιb2ndTM|QM1M1Nb
55 20 17 29 52 54 syl13anc φψzWιb2ndTM|QM1M1Nb2ndTMQM1M1Nιb2ndTM|QM1M1Nb
56 55 simpld φψzWιb2ndTM|QM1M1Nb2ndTM
57 19 56 sseldd φψzWιb2ndTM|QM1M1NbC
58 elssuni ιb2ndTM|QM1M1NbCιb2ndTM|QM1M1NbC
59 57 58 syl φψzWιb2ndTM|QM1M1NbC
60 59 2 sseqtrrdi φψzWιb2ndTM|QM1M1NbB
61 1 cvmsf1o FCCovMapJ2ndTMS1stTMιb2ndTM|QM1M1Nb2ndTMFιb2ndTM|QM1M1Nb:ιb2ndTM|QM1M1Nb1-1 onto1stTM
62 20 17 56 61 syl3anc φψzWFιb2ndTM|QM1M1Nb:ιb2ndTM|QM1M1Nb1-1 onto1stTM
63 f1ocnv Fιb2ndTM|QM1M1Nb:ιb2ndTM|QM1M1Nb1-1 onto1stTMFιb2ndTM|QM1M1Nb-1:1stTM1-1 ontoιb2ndTM|QM1M1Nb
64 f1of Fιb2ndTM|QM1M1Nb-1:1stTM1-1 ontoιb2ndTM|QM1M1NbFιb2ndTM|QM1M1Nb-1:1stTMιb2ndTM|QM1M1Nb
65 62 63 64 3syl φψzWFιb2ndTM|QM1M1Nb-1:1stTMιb2ndTM|QM1M1Nb
66 simprr φψzWzW
67 1 2 3 4 5 6 7 8 9 10 11 16 13 66 cvmliftlem3 φψzWGz1stTM
68 65 67 ffvelrnd φψzWFιb2ndTM|QM1M1Nb-1Gzιb2ndTM|QM1M1Nb
69 60 68 sseldd φψzWFιb2ndTM|QM1M1Nb-1GzB
70 69 anassrs φψzWFιb2ndTM|QM1M1Nb-1GzB
71 70 fmpttd φψzWFιb2ndTM|QM1M1Nb-1Gz:WB
72 14 31 syl φψM
73 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem5 φMQM=zWFιb2ndTM|QM1M1Nb-1Gz
74 72 73 syldan φψQM=zWFιb2ndTM|QM1M1Nb-1Gz
75 74 feq1d φψQM:WBzWFιb2ndTM|QM1M1Nb-1Gz:WB
76 71 75 mpbird φψQM:WB
77 fvres zWGWz=Gz
78 66 77 syl φψzWGWz=Gz
79 f1ocnvfv2 Fιb2ndTM|QM1M1Nb:ιb2ndTM|QM1M1Nb1-1 onto1stTMGz1stTMFιb2ndTM|QM1M1NbFιb2ndTM|QM1M1Nb-1Gz=Gz
80 62 67 79 syl2anc φψzWFιb2ndTM|QM1M1NbFιb2ndTM|QM1M1Nb-1Gz=Gz
81 fvres Fιb2ndTM|QM1M1Nb-1Gzιb2ndTM|QM1M1NbFιb2ndTM|QM1M1NbFιb2ndTM|QM1M1Nb-1Gz=FFιb2ndTM|QM1M1Nb-1Gz
82 68 81 syl φψzWFιb2ndTM|QM1M1NbFιb2ndTM|QM1M1Nb-1Gz=FFιb2ndTM|QM1M1Nb-1Gz
83 78 80 82 3eqtr2rd φψzWFFιb2ndTM|QM1M1Nb-1Gz=GWz
84 83 anassrs φψzWFFιb2ndTM|QM1M1Nb-1Gz=GWz
85 84 mpteq2dva φψzWFFιb2ndTM|QM1M1Nb-1Gz=zWGWz
86 4 22 23 3syl φF:BX
87 86 adantr φψF:BX
88 87 feqmptd φψF=yBFy
89 fveq2 y=Fιb2ndTM|QM1M1Nb-1GzFy=FFιb2ndTM|QM1M1Nb-1Gz
90 70 74 88 89 fmptco φψFQM=zWFFιb2ndTM|QM1M1Nb-1Gz
91 iiuni 01=II
92 91 3 cnf GIICnJG:01X
93 5 92 syl φG:01X
94 93 adantr φψG:01X
95 1 2 3 4 5 6 7 8 9 10 11 14 13 cvmliftlem2 φψW01
96 94 95 fssresd φψGW:WX
97 96 feqmptd φψGW=zWGWz
98 85 90 97 3eqtr4d φψFQM=GW
99 76 98 jca φψQM:WBFQM=GW