Metamath Proof Explorer

Theorem cvmliftlem9

Description: Lemma for cvmlift . The Q ( M ) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the Q functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
cvmliftlem.b ⊢B=⋃C
cvmliftlem.x ⊢X=⋃J
cvmliftlem.f ⊢φ→F∈CCovMapJ
cvmliftlem.g ⊢φ→G∈IICnJ
cvmliftlem.p ⊢φ→P∈B
cvmliftlem.e ⊢φ→F⁡P=G⁡0
cvmliftlem.n ⊢φ→N∈ℕ
cvmliftlem.t ⊢φ→T:1…N⟶⋃j∈Jj×S⁡j
cvmliftlem.a ⊢φ→∀k∈1…NGk−1NkN⊆1st⁡T⁡k
cvmliftlem.l ⊢L=topGen⁡ran⁡.
cvmliftlem.q ⊢Q=seq0x∈V,m∈ℕ⟼z∈m−1NmN⟼F↾ιb∈2nd⁡T⁡m|x⁡m−1N∈b-1⁡G⁡zI↾ℕ∪00P
Assertion cvmliftlem9 ⊢φ∧M∈1…N→Q⁡M⁡M−1N=Q⁡M−1⁡M−1N

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
2 cvmliftlem.b ⊢B=⋃C
3 cvmliftlem.x ⊢X=⋃J
4 cvmliftlem.f ⊢φ→F∈CCovMapJ
5 cvmliftlem.g ⊢φ→G∈IICnJ
6 cvmliftlem.p ⊢φ→P∈B
7 cvmliftlem.e ⊢φ→F⁡P=G⁡0
8 cvmliftlem.n ⊢φ→N∈ℕ
9 cvmliftlem.t ⊢φ→T:1…N⟶⋃j∈Jj×S⁡j
10 cvmliftlem.a ⊢φ→∀k∈1…NGk−1NkN⊆1st⁡T⁡k
11 cvmliftlem.l ⊢L=topGen⁡ran⁡.
12 cvmliftlem.q ⊢Q=seq0x∈V,m∈ℕ⟼z∈m−1NmN⟼F↾ιb∈2nd⁡T⁡m|x⁡m−1N∈b-1⁡G⁡zI↾ℕ∪00P
13 elfznn ⊢M∈1…N→M∈ℕ
14 eqid ⊢M−1NMN=M−1NMN
15 1 2 3 4 5 6 7 8 9 10 11 12 14 cvmliftlem5 ⊢φ∧M∈ℕ→Q⁡M=z∈M−1NMN⟼F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡z
16 13 15 sylan2 ⊢φ∧M∈1…N→Q⁡M=z∈M−1NMN⟼F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡z
17 simpr ⊢φ∧M∈1…N∧z=M−1N→z=M−1N
18 17 fveq2d ⊢φ∧M∈1…N∧z=M−1N→G⁡z=G⁡M−1N
19 18 fveq2d ⊢φ∧M∈1…N∧z=M−1N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡z=F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡M−1N
20 13 adantl ⊢φ∧M∈1…N→M∈ℕ
21 20 nnred ⊢φ∧M∈1…N→M∈ℝ
22 peano2rem ⊢M∈ℝ→M−1∈ℝ
23 21 22 syl ⊢φ∧M∈1…N→M−1∈ℝ
24 8 adantr ⊢φ∧M∈1…N→N∈ℕ
25 23 24 nndivred ⊢φ∧M∈1…N→M−1N∈ℝ
26 25 rexrd ⊢φ∧M∈1…N→M−1N∈ℝ*
27 21 24 nndivred ⊢φ∧M∈1…N→MN∈ℝ
28 27 rexrd ⊢φ∧M∈1…N→MN∈ℝ*
29 21 ltm1d ⊢φ∧M∈1…N→M−1<M
30 24 nnred ⊢φ∧M∈1…N→N∈ℝ
31 24 nngt0d ⊢φ∧M∈1…N→0<N
32 ltdiv1 ⊢M−1∈ℝ∧M∈ℝ∧N∈ℝ∧0<N→M−1<M↔M−1N<MN
33 23 21 30 31 32 syl112anc ⊢φ∧M∈1…N→M−1<M↔M−1N<MN
34 29 33 mpbid ⊢φ∧M∈1…N→M−1N<MN
35 25 27 34 ltled ⊢φ∧M∈1…N→M−1N≤MN
36 lbicc2 ⊢M−1N∈ℝ*∧MN∈ℝ*∧M−1N≤MN→M−1N∈M−1NMN
37 26 28 35 36 syl3anc ⊢φ∧M∈1…N→M−1N∈M−1NMN
38 fvexd ⊢φ∧M∈1…N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡M−1N∈V
39 16 19 37 38 fvmptd ⊢φ∧M∈1…N→Q⁡M⁡M−1N=F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡M−1N
40 4 adantr ⊢φ∧M∈1…N→F∈CCovMapJ
41 simpr ⊢φ∧M∈1…N→M∈1…N
42 1 2 3 4 5 6 7 8 9 10 11 41 cvmliftlem1 ⊢φ∧M∈1…N→2nd⁡T⁡M∈S⁡1st⁡T⁡M
43 1 2 3 4 5 6 7 8 9 10 11 12 14 cvmliftlem7 ⊢φ∧M∈1…N→Q⁡M−1⁡M−1N∈F-1G⁡M−1N
44 cvmcn ⊢F∈CCovMapJ→F∈CCnJ
45 2 3 cnf ⊢F∈CCnJ→F:B⟶X
46 40 44 45 3syl ⊢φ∧M∈1…N→F:B⟶X
47 ffn ⊢F:B⟶X→FFnB
48 fniniseg ⊢FFnB→Q⁡M−1⁡M−1N∈F-1G⁡M−1N↔Q⁡M−1⁡M−1N∈B∧F⁡Q⁡M−1⁡M−1N=G⁡M−1N
49 46 47 48 3syl ⊢φ∧M∈1…N→Q⁡M−1⁡M−1N∈F-1G⁡M−1N↔Q⁡M−1⁡M−1N∈B∧F⁡Q⁡M−1⁡M−1N=G⁡M−1N
50 43 49 mpbid ⊢φ∧M∈1…N→Q⁡M−1⁡M−1N∈B∧F⁡Q⁡M−1⁡M−1N=G⁡M−1N
51 50 simpld ⊢φ∧M∈1…N→Q⁡M−1⁡M−1N∈B
52 50 simprd ⊢φ∧M∈1…N→F⁡Q⁡M−1⁡M−1N=G⁡M−1N
53 1 2 3 4 5 6 7 8 9 10 11 41 14 37 cvmliftlem3 ⊢φ∧M∈1…N→G⁡M−1N∈1st⁡T⁡M
54 52 53 eqeltrd ⊢φ∧M∈1…N→F⁡Q⁡M−1⁡M−1N∈1st⁡T⁡M
55 eqid ⊢ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b=ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b
56 1 2 55 cvmsiota ⊢F∈CCovMapJ∧2nd⁡T⁡M∈S⁡1st⁡T⁡M∧Q⁡M−1⁡M−1N∈B∧F⁡Q⁡M−1⁡M−1N∈1st⁡T⁡M→ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b∈2nd⁡T⁡M∧Q⁡M−1⁡M−1N∈ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b
57 40 42 51 54 56 syl13anc ⊢φ∧M∈1…N→ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b∈2nd⁡T⁡M∧Q⁡M−1⁡M−1N∈ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b
58 57 simprd ⊢φ∧M∈1…N→Q⁡M−1⁡M−1N∈ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b
59 fvres ⊢Q⁡M−1⁡M−1N∈ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⁡Q⁡M−1⁡M−1N=F⁡Q⁡M−1⁡M−1N
60 58 59 syl ⊢φ∧M∈1…N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⁡Q⁡M−1⁡M−1N=F⁡Q⁡M−1⁡M−1N
61 60 52 eqtrd ⊢φ∧M∈1…N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⁡Q⁡M−1⁡M−1N=G⁡M−1N
62 57 simpld ⊢φ∧M∈1…N→ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b∈2nd⁡T⁡M
63 1 cvmsf1o ⊢F∈CCovMapJ∧2nd⁡T⁡M∈S⁡1st⁡T⁡M∧ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b∈2nd⁡T⁡M→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b:ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⟶1-1 onto1st⁡T⁡M
64 40 42 62 63 syl3anc ⊢φ∧M∈1…N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b:ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⟶1-1 onto1st⁡T⁡M
65 f1ocnvfv ⊢F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b:ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⟶1-1 onto1st⁡T⁡M∧Q⁡M−1⁡M−1N∈ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⁡Q⁡M−1⁡M−1N=G⁡M−1N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡M−1N=Q⁡M−1⁡M−1N
66 64 58 65 syl2anc ⊢φ∧M∈1…N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b⁡Q⁡M−1⁡M−1N=G⁡M−1N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡M−1N=Q⁡M−1⁡M−1N
67 61 66 mpd ⊢φ∧M∈1…N→F↾ιb∈2nd⁡T⁡M|Q⁡M−1⁡M−1N∈b-1⁡G⁡M−1N=Q⁡M−1⁡M−1N
68 39 67 eqtrd ⊢φ∧M∈1…N→Q⁡M⁡M−1N=Q⁡M−1⁡M−1N