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 -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
cvmliftlem.b ⊢ B = ⋃ C
cvmliftlem.x ⊢ X = ⋃ J
cvmliftlem.f ⊢ φ → F ∈ C CovMap J
cvmliftlem.g ⊢ φ → G ∈ II Cn J
cvmliftlem.p ⊢ φ → P ∈ B
cvmliftlem.e ⊢ φ → F ⁡ P = G ⁡ 0
cvmliftlem.n ⊢ φ → N ∈ ℕ
cvmliftlem.t ⊢ φ → T : 1 … N ⟶ ⋃ j ∈ J j × S ⁡ j
cvmliftlem.a ⊢ φ → ∀ k ∈ 1 … N G k − 1 N k N ⊆ 1 st ⁡ T ⁡ k
cvmliftlem.l ⊢ L = topGen ⁡ ran ⁡ .
cvmliftlem.q ⊢ Q = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P
Assertion cvmliftlem9 ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M ⁡ M − 1 N = Q ⁡ M − 1 ⁡ M − 1 N

Proof

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