Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
2 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
3 | 2 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
4 | 3 | ifbid 4462 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
5 | 4 | csbeq1d 3815 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
6 | | 2fveq3 6722 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
7 | | 2fveq3 6722 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
8 | 7 | imaeq1d 5928 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
9 | 8 | xpeq1d 5580 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
10 | 7 | imaeq1d 5928 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
11 | 10 | xpeq1d 5580 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
12 | 9, 11 | uneq12d 4078 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
13 | 6, 12 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
14 | 13 | csbeq2dv 3818 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
15 | 5, 14 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
16 | 15 | mpteq2dv 5151 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
17 | 16 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
18 | | poimirlem22.s |
. . . . . 6
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
19 | 17, 18 | elrab2 3605 |
. . . . 5
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
20 | 19 | simprbi 500 |
. . . 4
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
21 | 1, 20 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
22 | | breq1 5056 |
. . . . . . 7
⊢ (𝑦 = 0 → (𝑦 < (2nd ‘𝑇) ↔ 0 < (2nd
‘𝑇))) |
23 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 0 → 𝑦 = 0) |
24 | 22, 23 | ifbieq1d 4463 |
. . . . . 6
⊢ (𝑦 = 0 → if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) = if(0 < (2nd
‘𝑇), 0, (𝑦 + 1))) |
25 | | poimirlem5.2 |
. . . . . . 7
⊢ (𝜑 → 0 < (2nd
‘𝑇)) |
26 | 25 | iftrued 4447 |
. . . . . 6
⊢ (𝜑 → if(0 < (2nd
‘𝑇), 0, (𝑦 + 1)) = 0) |
27 | 24, 26 | sylan9eqr 2800 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 0) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 0) |
28 | 27 | csbeq1d 3815 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 0) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
29 | | c0ex 10827 |
. . . . . . 7
⊢ 0 ∈
V |
30 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → (1...𝑗) = (1...0)) |
31 | | fz10 13133 |
. . . . . . . . . . . . 13
⊢ (1...0) =
∅ |
32 | 30, 31 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → (1...𝑗) = ∅) |
33 | 32 | imaeq2d 5929 |
. . . . . . . . . . 11
⊢ (𝑗 = 0 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
∅)) |
34 | 33 | xpeq1d 5580 |
. . . . . . . . . 10
⊢ (𝑗 = 0 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ ∅) ×
{1})) |
35 | | oveq1 7220 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
36 | | 0p1e1 11952 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
37 | 35, 36 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → (𝑗 + 1) = 1) |
38 | 37 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁)) |
39 | 38 | imaeq2d 5929 |
. . . . . . . . . . 11
⊢ (𝑗 = 0 → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑁))) |
40 | 39 | xpeq1d 5580 |
. . . . . . . . . 10
⊢ (𝑗 = 0 → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
41 | 34, 40 | uneq12d 4078 |
. . . . . . . . 9
⊢ (𝑗 = 0 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}))) |
42 | | ima0 5945 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
43 | 42 | xpeq1i 5577 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) = (∅
× {1}) |
44 | | 0xp 5646 |
. . . . . . . . . . . 12
⊢ (∅
× {1}) = ∅ |
45 | 43, 44 | eqtri 2765 |
. . . . . . . . . . 11
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) =
∅ |
46 | 45 | uneq1i 4073 |
. . . . . . . . . 10
⊢
((((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = (∅ ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
47 | | uncom 4067 |
. . . . . . . . . 10
⊢ (∅
∪ (((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) ∪
∅) |
48 | | un0 4305 |
. . . . . . . . . 10
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) ∪ ∅) =
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) |
49 | 46, 47, 48 | 3eqtri 2769 |
. . . . . . . . 9
⊢
((((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) |
50 | 41, 49 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑗 = 0 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
51 | 50 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑗 = 0 → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}))) |
52 | 29, 51 | csbie 3847 |
. . . . . 6
⊢
⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
53 | | elrabi 3596 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
54 | 53, 18 | eleq2s 2856 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
55 | 1, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
56 | | xp1st 7793 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
58 | | xp2nd 7794 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
60 | | fvex 6730 |
. . . . . . . . . . . 12
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
61 | | f1oeq1 6649 |
. . . . . . . . . . . 12
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
62 | 60, 61 | elab 3587 |
. . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
63 | 59, 62 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
64 | | f1ofo 6668 |
. . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
66 | | foima 6638 |
. . . . . . . . 9
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
67 | 65, 66 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
68 | 67 | xpeq1d 5580 |
. . . . . . 7
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0})) |
69 | 68 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘f + (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{0}))) |
70 | 52, 69 | syl5eq 2790 |
. . . . 5
⊢ (𝜑 → ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{0}))) |
71 | 70 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{0}))) |
72 | 28, 71 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑦 = 0) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{0}))) |
73 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
74 | | nnm1nn0 12131 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
75 | 73, 74 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
76 | | 0elfz 13209 |
. . . 4
⊢ ((𝑁 − 1) ∈
ℕ0 → 0 ∈ (0...(𝑁 − 1))) |
77 | 75, 76 | syl 17 |
. . 3
⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1))) |
78 | | ovexd 7248 |
. . 3
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) × {0})) ∈
V) |
79 | 21, 72, 77, 78 | fvmptd 6825 |
. 2
⊢ (𝜑 → (𝐹‘0) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{0}))) |
80 | | ovexd 7248 |
. . 3
⊢ (𝜑 → (1...𝑁) ∈ V) |
81 | | xp1st 7793 |
. . . . 5
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
82 | 57, 81 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
83 | | elmapfn 8546 |
. . . 4
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
84 | 82, 83 | syl 17 |
. . 3
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
85 | | fnconstg 6607 |
. . . 4
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
86 | 29, 85 | mp1i 13 |
. . 3
⊢ (𝜑 → ((1...𝑁) × {0}) Fn (1...𝑁)) |
87 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘𝑛)) |
88 | 29 | fvconst2 7019 |
. . . 4
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
89 | 88 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
90 | | elmapi 8530 |
. . . . . . . 8
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
91 | 82, 90 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
92 | 91 | ffvelrnda 6904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
93 | | elfzonn0 13287 |
. . . . . 6
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
94 | 92, 93 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
95 | 94 | nn0cnd 12152 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
96 | 95 | addid1d 11032 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
97 | 80, 84, 86, 84, 87, 89, 96 | offveq 7492 |
. 2
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) × {0})) =
(1st ‘(1st ‘𝑇))) |
98 | 79, 97 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐹‘0) = (1st
‘(1st ‘𝑇))) |