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 = 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
cvmliftlem5.3 ⊢ W = M − 1 N M N
cvmliftlem6.1 ⊢ φ ∧ ψ → M ∈ 1 … N
cvmliftlem6.2 ⊢ φ ∧ ψ → Q ⁡ M − 1 ⁡ M − 1 N ∈ F -1 G ⁡ M − 1 N
Assertion cvmliftlem6 ⊢ φ ∧ ψ → Q ⁡ M : W ⟶ B ∧ F ∘ Q ⁡ M = G ↾ W

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 cvmliftlem5.3 ⊢ W = M − 1 N M N
14 cvmliftlem6.1 ⊢ φ ∧ ψ → M ∈ 1 … N
15 cvmliftlem6.2 ⊢ φ ∧ ψ → Q ⁡ M − 1 ⁡ M − 1 N ∈ F -1 G ⁡ M − 1 N
16 14 adantrr ⊢ φ ∧ ψ ∧ z ∈ W → M ∈ 1 … N
17 1 2 3 4 5 6 7 8 9 10 11 16 cvmliftlem1 ⊢ φ ∧ ψ ∧ z ∈ W → 2 nd ⁡ T ⁡ M ∈ S ⁡ 1 st ⁡ T ⁡ M
18 1 cvmsss ⊢ 2 nd ⁡ T ⁡ M ∈ S ⁡ 1 st ⁡ T ⁡ M → 2 nd ⁡ T ⁡ M ⊆ C
19 17 18 syl ⊢ φ ∧ ψ ∧ z ∈ W → 2 nd ⁡ T ⁡ M ⊆ C
20 4 adantr ⊢ φ ∧ ψ ∧ z ∈ W → F ∈ C CovMap J
21 15 adantrr ⊢ φ ∧ ψ ∧ z ∈ W → Q ⁡ M − 1 ⁡ M − 1 N ∈ F -1 G ⁡ M − 1 N
22 cvmcn ⊢ F ∈ C CovMap J → F ∈ C Cn J
23 2 3 cnf ⊢ F ∈ C Cn J → F : B ⟶ X
24 20 22 23 3syl ⊢ φ ∧ ψ ∧ z ∈ W → F : B ⟶ X
25 ffn ⊢ F : B ⟶ X → F Fn B
26 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
27 24 25 26 3syl ⊢ φ ∧ ψ ∧ z ∈ W → 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
28 21 27 mpbid ⊢ φ ∧ ψ ∧ z ∈ W → Q ⁡ M − 1 ⁡ M − 1 N ∈ B ∧ F ⁡ Q ⁡ M − 1 ⁡ M − 1 N = G ⁡ M − 1 N
29 28 simpld ⊢ φ ∧ ψ ∧ z ∈ W → Q ⁡ M − 1 ⁡ M − 1 N ∈ B
30 28 simprd ⊢ φ ∧ ψ ∧ z ∈ W → F ⁡ Q ⁡ M − 1 ⁡ M − 1 N = G ⁡ M − 1 N
31 elfznn ⊢ M ∈ 1 … N → M ∈ ℕ
32 16 31 syl ⊢ φ ∧ ψ ∧ z ∈ W → M ∈ ℕ
33 32 nnred ⊢ φ ∧ ψ ∧ z ∈ W → M ∈ ℝ
34 peano2rem ⊢ M ∈ ℝ → M − 1 ∈ ℝ
35 33 34 syl ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 ∈ ℝ
36 8 adantr ⊢ φ ∧ ψ ∧ z ∈ W → N ∈ ℕ
37 35 36 nndivred ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 N ∈ ℝ
38 37 rexrd ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 N ∈ ℝ *
39 33 36 nndivred ⊢ φ ∧ ψ ∧ z ∈ W → M N ∈ ℝ
40 39 rexrd ⊢ φ ∧ ψ ∧ z ∈ W → M N ∈ ℝ *
41 33 ltm1d ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 < M
42 36 nnred ⊢ φ ∧ ψ ∧ z ∈ W → N ∈ ℝ
43 36 nngt0d ⊢ φ ∧ ψ ∧ z ∈ W → 0 < N
44 ltdiv1 ⊢ M − 1 ∈ ℝ ∧ M ∈ ℝ ∧ N ∈ ℝ ∧ 0 < N → M − 1 < M ↔ M − 1 N < M N
45 35 33 42 43 44 syl112anc ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 < M ↔ M − 1 N < M N
46 41 45 mpbid ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 N < M N
47 37 39 46 ltled ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 N ≤ M N
48 lbicc2 ⊢ M − 1 N ∈ ℝ * ∧ M N ∈ ℝ * ∧ M − 1 N ≤ M N → M − 1 N ∈ M − 1 N M N
49 38 40 47 48 syl3anc ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 N ∈ M − 1 N M N
50 49 13 eleqtrrdi ⊢ φ ∧ ψ ∧ z ∈ W → M − 1 N ∈ W
51 1 2 3 4 5 6 7 8 9 10 11 16 13 50 cvmliftlem3 ⊢ φ ∧ ψ ∧ z ∈ W → G ⁡ M − 1 N ∈ 1 st ⁡ T ⁡ M
52 30 51 eqeltrd ⊢ φ ∧ ψ ∧ z ∈ W → F ⁡ Q ⁡ M − 1 ⁡ M − 1 N ∈ 1 st ⁡ T ⁡ M
53 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
54 1 2 53 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
55 20 17 29 52 54 syl13anc ⊢ φ ∧ ψ ∧ z ∈ W → ι 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
56 55 simpld ⊢ φ ∧ ψ ∧ z ∈ W → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ 2 nd ⁡ T ⁡ M
57 19 56 sseldd ⊢ φ ∧ ψ ∧ z ∈ W → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ C
58 elssuni ⊢ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ C → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ⊆ ⋃ C
59 57 58 syl ⊢ φ ∧ ψ ∧ z ∈ W → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ⊆ ⋃ C
60 59 2 sseqtrrdi ⊢ φ ∧ ψ ∧ z ∈ W → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ⊆ B
61 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
62 20 17 56 61 syl3anc ⊢ φ ∧ ψ ∧ z ∈ W → 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
63 f1ocnv ⊢ 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 → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 : 1 st ⁡ T ⁡ M ⟶ 1-1 onto ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
64 f1of ⊢ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 : 1 st ⁡ T ⁡ M ⟶ 1-1 onto ι 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 -1 : 1 st ⁡ T ⁡ M ⟶ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
65 62 63 64 3syl ⊢ φ ∧ ψ ∧ z ∈ W → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 : 1 st ⁡ T ⁡ M ⟶ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
66 simprr ⊢ φ ∧ ψ ∧ z ∈ W → z ∈ W
67 1 2 3 4 5 6 7 8 9 10 11 16 13 66 cvmliftlem3 ⊢ φ ∧ ψ ∧ z ∈ W → G ⁡ z ∈ 1 st ⁡ T ⁡ M
68 65 67 ffvelcdmd ⊢ φ ∧ ψ ∧ z ∈ W → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
69 60 68 sseldd ⊢ φ ∧ ψ ∧ z ∈ W → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ B
70 69 anassrs ⊢ φ ∧ ψ ∧ z ∈ W → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ B
71 70 fmpttd ⊢ φ ∧ ψ → z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z : W ⟶ B
72 14 31 syl ⊢ φ ∧ ψ → M ∈ ℕ
73 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem5 ⊢ φ ∧ M ∈ ℕ → Q ⁡ M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
74 72 73 syldan ⊢ φ ∧ ψ → Q ⁡ M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
75 74 feq1d ⊢ φ ∧ ψ → Q ⁡ M : W ⟶ B ↔ z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z : W ⟶ B
76 71 75 mpbird ⊢ φ ∧ ψ → Q ⁡ M : W ⟶ B
77 fvres ⊢ z ∈ W → G ↾ W ⁡ z = G ⁡ z
78 66 77 syl ⊢ φ ∧ ψ ∧ z ∈ W → G ↾ W ⁡ z = G ⁡ z
79 f1ocnvfv2 ⊢ 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 ∧ G ⁡ z ∈ 1 st ⁡ T ⁡ M → F ↾ ι 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 -1 ⁡ G ⁡ z = G ⁡ z
80 62 67 79 syl2anc ⊢ φ ∧ ψ ∧ z ∈ W → F ↾ ι 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 -1 ⁡ G ⁡ z = G ⁡ z
81 fvres ⊢ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ ι 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 ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z = F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
82 68 81 syl ⊢ φ ∧ ψ ∧ z ∈ W → F ↾ ι 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 -1 ⁡ G ⁡ z = F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
83 78 80 82 3eqtr2rd ⊢ φ ∧ ψ ∧ z ∈ W → F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z = G ↾ W ⁡ z
84 83 anassrs ⊢ φ ∧ ψ ∧ z ∈ W → F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z = G ↾ W ⁡ z
85 84 mpteq2dva ⊢ φ ∧ ψ → z ∈ W ⟼ F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z = z ∈ W ⟼ G ↾ W ⁡ z
86 4 22 23 3syl ⊢ φ → F : B ⟶ X
87 86 adantr ⊢ φ ∧ ψ → F : B ⟶ X
88 87 feqmptd ⊢ φ ∧ ψ → F = y ∈ B ⟼ F ⁡ y
89 fveq2 ⊢ y = F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z → F ⁡ y = F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
90 70 74 88 89 fmptco ⊢ φ ∧ ψ → F ∘ Q ⁡ M = z ∈ W ⟼ F ⁡ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
91 iiuni ⊢ 0 1 = ⋃ II
92 91 3 cnf ⊢ G ∈ II Cn J → G : 0 1 ⟶ X
93 5 92 syl ⊢ φ → G : 0 1 ⟶ X
94 93 adantr ⊢ φ ∧ ψ → G : 0 1 ⟶ X
95 1 2 3 4 5 6 7 8 9 10 11 14 13 cvmliftlem2 ⊢ φ ∧ ψ → W ⊆ 0 1
96 94 95 fssresd ⊢ φ ∧ ψ → G ↾ W : W ⟶ X
97 96 feqmptd ⊢ φ ∧ ψ → G ↾ W = z ∈ W ⟼ G ↾ W ⁡ z
98 85 90 97 3eqtr4d ⊢ φ ∧ ψ → F ∘ Q ⁡ M = G ↾ W
99 76 98 jca ⊢ φ ∧ ψ → Q ⁡ M : W ⟶ B ∧ F ∘ Q ⁡ M = G ↾ W