Proof of Theorem cvmliftlem13
Step | Hyp | Ref
| Expression |
1 | | cvmliftlem.1 |
. . . . . . 7
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
2 | | cvmliftlem.b |
. . . . . . 7
⊢ 𝐵 = ∪
𝐶 |
3 | | cvmliftlem.x |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
4 | | cvmliftlem.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
5 | | cvmliftlem.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
6 | | cvmliftlem.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
7 | | cvmliftlem.e |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) |
8 | | cvmliftlem.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | | cvmliftlem.t |
. . . . . . 7
⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪
𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) |
10 | | cvmliftlem.a |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) |
11 | | cvmliftlem.l |
. . . . . . 7
⊢ 𝐿 = (topGen‘ran
(,)) |
12 | | cvmliftlem.q |
. . . . . . 7
⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})) |
13 | | cvmliftlem.k |
. . . . . . 7
⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | cvmliftlem11 33251 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = 𝐺)) |
15 | 14 | simpld 495 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (II Cn 𝐶)) |
16 | | iiuni 24040 |
. . . . . 6
⊢ (0[,]1) =
∪ II |
17 | 16, 2 | cnf 22393 |
. . . . 5
⊢ (𝐾 ∈ (II Cn 𝐶) → 𝐾:(0[,]1)⟶𝐵) |
18 | 15, 17 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐾:(0[,]1)⟶𝐵) |
19 | 18 | ffund 6601 |
. . 3
⊢ (𝜑 → Fun 𝐾) |
20 | | nnuz 12618 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
21 | 8, 20 | eleqtrdi 2851 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
22 | | eluzfz1 13260 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → 1 ∈ (1...𝑁)) |
24 | | fveq2 6769 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1)) |
25 | 24 | ssiun2s 4983 |
. . . . 5
⊢ (1 ∈
(1...𝑁) → (𝑄‘1) ⊆ ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)) |
26 | 23, 25 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑄‘1) ⊆ ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)) |
27 | 26, 13 | sseqtrrdi 3977 |
. . 3
⊢ (𝜑 → (𝑄‘1) ⊆ 𝐾) |
28 | | 0xr 11021 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ*) |
30 | 8 | nnrecred 12022 |
. . . . . . 7
⊢ (𝜑 → (1 / 𝑁) ∈ ℝ) |
31 | 30 | rexrd 11024 |
. . . . . 6
⊢ (𝜑 → (1 / 𝑁) ∈
ℝ*) |
32 | | 1red 10975 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
33 | | 0le1 11496 |
. . . . . . . 8
⊢ 0 ≤
1 |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 1) |
35 | 8 | nnred 11986 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
36 | 8 | nngt0d 12020 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑁) |
37 | | divge0 11842 |
. . . . . . 7
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (1 / 𝑁)) |
38 | 32, 34, 35, 36, 37 | syl22anc 836 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (1 / 𝑁)) |
39 | | lbicc2 13193 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (1 / 𝑁) ∈ ℝ* ∧ 0 ≤ (1
/ 𝑁)) → 0 ∈
(0[,](1 / 𝑁))) |
40 | 29, 31, 38, 39 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → 0 ∈ (0[,](1 / 𝑁))) |
41 | | 1m1e0 12043 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
42 | 41 | oveq1i 7279 |
. . . . . . 7
⊢ ((1
− 1) / 𝑁) = (0 /
𝑁) |
43 | 8 | nncnd 11987 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
44 | 8 | nnne0d 12021 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ≠ 0) |
45 | 43, 44 | div0d 11748 |
. . . . . . 7
⊢ (𝜑 → (0 / 𝑁) = 0) |
46 | 42, 45 | eqtrid 2792 |
. . . . . 6
⊢ (𝜑 → ((1 − 1) / 𝑁) = 0) |
47 | 46 | oveq1d 7284 |
. . . . 5
⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁))) |
48 | 40, 47 | eleqtrrd 2844 |
. . . 4
⊢ (𝜑 → 0 ∈ (((1 − 1) /
𝑁)[,](1 / 𝑁))) |
49 | | eqid 2740 |
. . . . . . . 8
⊢ (((1
− 1) / 𝑁)[,](1 /
𝑁)) = (((1 − 1) /
𝑁)[,](1 / 𝑁)) |
50 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁)) |
51 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 49 | cvmliftlem7 33247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁)) ∈ (◡𝐹 “ {(𝐺‘((1 − 1) / 𝑁))})) |
52 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 49, 50, 51 | cvmliftlem6 33246 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) |
53 | 23, 52 | mpdan 684 |
. . . . . 6
⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) |
54 | 53 | simpld 495 |
. . . . 5
⊢ (𝜑 → (𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵) |
55 | 54 | fdmd 6608 |
. . . 4
⊢ (𝜑 → dom (𝑄‘1) = (((1 − 1) / 𝑁)[,](1 / 𝑁))) |
56 | 48, 55 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → 0 ∈ dom (𝑄‘1)) |
57 | | funssfv 6790 |
. . 3
⊢ ((Fun
𝐾 ∧ (𝑄‘1) ⊆ 𝐾 ∧ 0 ∈ dom (𝑄‘1)) → (𝐾‘0) = ((𝑄‘1)‘0)) |
58 | 19, 27, 56, 57 | syl3anc 1370 |
. 2
⊢ (𝜑 → (𝐾‘0) = ((𝑄‘1)‘0)) |
59 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cvmliftlem9 33249 |
. . . 4
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1)‘((1 − 1) / 𝑁)) = ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁))) |
60 | 23, 59 | mpdan 684 |
. . 3
⊢ (𝜑 → ((𝑄‘1)‘((1 − 1) / 𝑁)) = ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁))) |
61 | 46 | fveq2d 6773 |
. . 3
⊢ (𝜑 → ((𝑄‘1)‘((1 − 1) / 𝑁)) = ((𝑄‘1)‘0)) |
62 | 41 | fveq2i 6772 |
. . . . . 6
⊢ (𝑄‘(1 − 1)) = (𝑄‘0) |
63 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cvmliftlem4 33244 |
. . . . . 6
⊢ (𝑄‘0) = {〈0, 𝑃〉} |
64 | 62, 63 | eqtri 2768 |
. . . . 5
⊢ (𝑄‘(1 − 1)) =
{〈0, 𝑃〉} |
65 | 64 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑄‘(1 − 1)) = {〈0, 𝑃〉}) |
66 | 65, 46 | fveq12d 6776 |
. . 3
⊢ (𝜑 → ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁)) = ({〈0, 𝑃〉}‘0)) |
67 | 60, 61, 66 | 3eqtr3d 2788 |
. 2
⊢ (𝜑 → ((𝑄‘1)‘0) = ({〈0, 𝑃〉}‘0)) |
68 | | 0nn0 12246 |
. . 3
⊢ 0 ∈
ℕ0 |
69 | | fvsng 7047 |
. . 3
⊢ ((0
∈ ℕ0 ∧ 𝑃 ∈ 𝐵) → ({〈0, 𝑃〉}‘0) = 𝑃) |
70 | 68, 6, 69 | sylancr 587 |
. 2
⊢ (𝜑 → ({〈0, 𝑃〉}‘0) = 𝑃) |
71 | 58, 67, 70 | 3eqtrd 2784 |
1
⊢ (𝜑 → (𝐾‘0) = 𝑃) |