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 30531 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = 𝐺)) |
15 | 14 | simpld 474 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (II Cn 𝐶)) |
16 | | iiuni 22492 |
. . . . . 6
⊢ (0[,]1) =
∪ II |
17 | 16, 2 | cnf 20860 |
. . . . 5
⊢ (𝐾 ∈ (II Cn 𝐶) → 𝐾:(0[,]1)⟶𝐵) |
18 | 15, 17 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐾:(0[,]1)⟶𝐵) |
19 | | ffun 5961 |
. . . 4
⊢ (𝐾:(0[,]1)⟶𝐵 → Fun 𝐾) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝜑 → Fun 𝐾) |
21 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
22 | 8, 21 | syl6eleq 2698 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
23 | | eluzfz1 12219 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → 1 ∈ (1...𝑁)) |
25 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1)) |
26 | 25 | ssiun2s 4500 |
. . . . 5
⊢ (1 ∈
(1...𝑁) → (𝑄‘1) ⊆ ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)) |
27 | 24, 26 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑄‘1) ⊆ ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)) |
28 | 27, 13 | syl6sseqr 3615 |
. . 3
⊢ (𝜑 → (𝑄‘1) ⊆ 𝐾) |
29 | | 0xr 9965 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ*) |
31 | 8 | nnrecred 10943 |
. . . . . . 7
⊢ (𝜑 → (1 / 𝑁) ∈ ℝ) |
32 | 31 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → (1 / 𝑁) ∈
ℝ*) |
33 | | 1red 9934 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
34 | | 0le1 10430 |
. . . . . . . 8
⊢ 0 ≤
1 |
35 | 34 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 1) |
36 | 8 | nnred 10912 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
37 | 8 | nngt0d 10941 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑁) |
38 | | divge0 10771 |
. . . . . . 7
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (1 / 𝑁)) |
39 | 33, 35, 36, 37, 38 | syl22anc 1319 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (1 / 𝑁)) |
40 | | lbicc2 12159 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (1 / 𝑁) ∈ ℝ* ∧ 0 ≤ (1
/ 𝑁)) → 0 ∈
(0[,](1 / 𝑁))) |
41 | 30, 32, 39, 40 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 0 ∈ (0[,](1 / 𝑁))) |
42 | | 1m1e0 10966 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
43 | 42 | oveq1i 6559 |
. . . . . . 7
⊢ ((1
− 1) / 𝑁) = (0 /
𝑁) |
44 | 8 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
45 | 8 | nnne0d 10942 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ≠ 0) |
46 | 44, 45 | div0d 10679 |
. . . . . . 7
⊢ (𝜑 → (0 / 𝑁) = 0) |
47 | 43, 46 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → ((1 − 1) / 𝑁) = 0) |
48 | 47 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁))) |
49 | 41, 48 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 0 ∈ (((1 − 1) /
𝑁)[,](1 / 𝑁))) |
50 | | eqid 2610 |
. . . . . . . 8
⊢ (((1
− 1) / 𝑁)[,](1 /
𝑁)) = (((1 − 1) /
𝑁)[,](1 / 𝑁)) |
51 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁)) |
52 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 50 | cvmliftlem7 30527 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁)) ∈ (◡𝐹 “ {(𝐺‘((1 − 1) / 𝑁))})) |
53 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 50, 51, 52 | cvmliftlem6 30526 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) |
54 | 24, 53 | mpdan 699 |
. . . . . 6
⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) |
55 | 54 | simpld 474 |
. . . . 5
⊢ (𝜑 → (𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵) |
56 | | fdm 5964 |
. . . . 5
⊢ ((𝑄‘1):(((1 − 1) /
𝑁)[,](1 / 𝑁))⟶𝐵 → dom (𝑄‘1) = (((1 − 1) / 𝑁)[,](1 / 𝑁))) |
57 | 55, 56 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑄‘1) = (((1 − 1) / 𝑁)[,](1 / 𝑁))) |
58 | 49, 57 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 0 ∈ dom (𝑄‘1)) |
59 | | funssfv 6119 |
. . 3
⊢ ((Fun
𝐾 ∧ (𝑄‘1) ⊆ 𝐾 ∧ 0 ∈ dom (𝑄‘1)) → (𝐾‘0) = ((𝑄‘1)‘0)) |
60 | 20, 28, 58, 59 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝐾‘0) = ((𝑄‘1)‘0)) |
61 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cvmliftlem9 30529 |
. . . 4
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1)‘((1 − 1) / 𝑁)) = ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁))) |
62 | 24, 61 | mpdan 699 |
. . 3
⊢ (𝜑 → ((𝑄‘1)‘((1 − 1) / 𝑁)) = ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁))) |
63 | 47 | fveq2d 6107 |
. . 3
⊢ (𝜑 → ((𝑄‘1)‘((1 − 1) / 𝑁)) = ((𝑄‘1)‘0)) |
64 | 42 | fveq2i 6106 |
. . . . . 6
⊢ (𝑄‘(1 − 1)) = (𝑄‘0) |
65 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cvmliftlem4 30524 |
. . . . . 6
⊢ (𝑄‘0) = {〈0, 𝑃〉} |
66 | 64, 65 | eqtri 2632 |
. . . . 5
⊢ (𝑄‘(1 − 1)) =
{〈0, 𝑃〉} |
67 | 66 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑄‘(1 − 1)) = {〈0, 𝑃〉}) |
68 | 67, 47 | fveq12d 6109 |
. . 3
⊢ (𝜑 → ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁)) = ({〈0, 𝑃〉}‘0)) |
69 | 62, 63, 68 | 3eqtr3d 2652 |
. 2
⊢ (𝜑 → ((𝑄‘1)‘0) = ({〈0, 𝑃〉}‘0)) |
70 | | 0nn0 11184 |
. . 3
⊢ 0 ∈
ℕ0 |
71 | | fvsng 6352 |
. . 3
⊢ ((0
∈ ℕ0 ∧ 𝑃 ∈ 𝐵) → ({〈0, 𝑃〉}‘0) = 𝑃) |
72 | 70, 6, 71 | sylancr 694 |
. 2
⊢ (𝜑 → ({〈0, 𝑃〉}‘0) = 𝑃) |
73 | 60, 69, 72 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐾‘0) = 𝑃) |