Step | Hyp | Ref
| Expression |
1 | | ovexd 7248 |
. 2
⊢ (𝜑 → (1...𝑁) ∈ V) |
2 | | poimirlem22.1 |
. . . 4
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
3 | | poimir.0 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | | nnm1nn0 12131 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
6 | | nn0fz0 13210 |
. . . . 5
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
7 | 5, 6 | sylib 221 |
. . . 4
⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
8 | 2, 7 | ffvelrnd 6905 |
. . 3
⊢ (𝜑 → (𝐹‘(𝑁 − 1)) ∈ ((0...𝐾) ↑m (1...𝑁))) |
9 | | elmapfn 8546 |
. . 3
⊢ ((𝐹‘(𝑁 − 1)) ∈ ((0...𝐾) ↑m (1...𝑁)) → (𝐹‘(𝑁 − 1)) Fn (1...𝑁)) |
10 | 8, 9 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘(𝑁 − 1)) Fn (1...𝑁)) |
11 | | 1ex 10829 |
. . 3
⊢ 1 ∈
V |
12 | | fnconstg 6607 |
. . 3
⊢ (1 ∈
V → ((1...𝑁) ×
{1}) Fn (1...𝑁)) |
13 | 11, 12 | mp1i 13 |
. 2
⊢ (𝜑 → ((1...𝑁) × {1}) Fn (1...𝑁)) |
14 | | poimirlem12.2 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
15 | | elrabi 3596 |
. . . . . . 7
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
16 | | poimirlem22.s |
. . . . . . 7
⊢ 𝑆 = {𝑡 ∈ ((((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}))))} |
17 | 15, 16 | eleq2s 2856 |
. . . . . 6
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
18 | 14, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
19 | | xp1st 7793 |
. . . . 5
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
21 | | xp1st 7793 |
. . . 4
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
22 | 20, 21 | syl 17 |
. . 3
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
23 | | elmapfn 8546 |
. . 3
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
24 | 22, 23 | syl 17 |
. 2
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
25 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
26 | 25 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
27 | 26 | ifbid 4462 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
28 | 27 | csbeq1d 3815 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → ⦋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})))) |
29 | | 2fveq3 6722 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
30 | | 2fveq3 6722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
31 | 30 | imaeq1d 5928 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
32 | 31 | xpeq1d 5580 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
33 | 30 | imaeq1d 5928 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
34 | 33 | xpeq1d 5580 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
35 | 32, 34 | uneq12d 4078 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
36 | 29, 35 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
37 | 36 | csbeq2dv 3818 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → ⦋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})))) |
38 | 28, 37 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ⦋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})))) |
39 | 38 | mpteq2dv 5151 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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}))))) |
40 | 39 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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})))))) |
41 | 40, 16 | elrab2 3605 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((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})))))) |
42 | 41 | simprbi 500 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
43 | 14, 42 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
44 | | poimirlem11.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2nd
‘𝑇) =
0) |
45 | | breq12 5058 |
. . . . . . . . . . . 12
⊢ ((𝑦 = (𝑁 − 1) ∧ (2nd
‘𝑇) = 0) →
(𝑦 < (2nd
‘𝑇) ↔ (𝑁 − 1) <
0)) |
46 | 44, 45 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝑦 = (𝑁 − 1) ∧ 𝜑) → (𝑦 < (2nd ‘𝑇) ↔ (𝑁 − 1) < 0)) |
47 | 46 | ancoms 462 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → (𝑦 < (2nd ‘𝑇) ↔ (𝑁 − 1) < 0)) |
48 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1)) |
49 | 3 | nncnd 11846 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
50 | | npcan1 11257 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
52 | 48, 51 | sylan9eqr 2800 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → (𝑦 + 1) = 𝑁) |
53 | 47, 52 | ifbieq2d 4465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 0, 𝑦, 𝑁)) |
54 | 5 | nn0ge0d 12153 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁 − 1)) |
55 | | 0red 10836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
56 | 5 | nn0red 12151 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
57 | 55, 56 | lenltd 10978 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ ¬ (𝑁 − 1) < 0)) |
58 | 54, 57 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝑁 − 1) < 0) |
59 | 58 | iffalsed 4450 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝑁 − 1) < 0, 𝑦, 𝑁) = 𝑁) |
60 | 59 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → if((𝑁 − 1) < 0, 𝑦, 𝑁) = 𝑁) |
61 | 53, 60 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑁) |
62 | 61 | csbeq1d 3815 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
63 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁)) |
64 | 63 | imaeq2d 5929 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑁 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑁))) |
65 | | xp2nd 7794 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
66 | 20, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
67 | | fvex 6730 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
68 | | f1oeq1 6649 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
69 | 67, 68 | elab 3587 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
70 | 66, 69 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
71 | | f1ofo 6668 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
72 | | foima 6638 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
73 | 70, 71, 72 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
74 | 64, 73 | sylan9eqr 2800 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = (1...𝑁)) |
75 | 74 | xpeq1d 5580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = ((1...𝑁) × {1})) |
76 | | oveq1 7220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
77 | 76 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁)) |
78 | 3 | nnred 11845 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℝ) |
79 | 78 | ltp1d 11762 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
80 | 3 | nnzd 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
81 | 80 | peano2zd 12285 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
82 | | fzn 13128 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅)) |
83 | 81, 80, 82 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅)) |
84 | 79, 83 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅) |
85 | 77, 84 | sylan9eqr 2800 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((𝑗 + 1)...𝑁) = ∅) |
86 | 85 | imaeq2d 5929 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
∅)) |
87 | 86 | xpeq1d 5580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ∅) ×
{0})) |
88 | | ima0 5945 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
89 | 88 | xpeq1i 5577 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {0}) = (∅
× {0}) |
90 | | 0xp 5646 |
. . . . . . . . . . . . . 14
⊢ (∅
× {0}) = ∅ |
91 | 89, 90 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {0}) =
∅ |
92 | 87, 91 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = ∅) |
93 | 75, 92 | uneq12d 4078 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪
∅)) |
94 | | un0 4305 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ×
{1}) ∪ ∅) = ((1...𝑁) × {1}) |
95 | 93, 94 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1})) |
96 | 95 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{1}))) |
97 | 3, 96 | csbied 3849 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑁 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{1}))) |
98 | 97 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → ⦋𝑁 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{1}))) |
99 | 62, 98 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{1}))) |
100 | | ovexd 7248 |
. . . . . 6
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) × {1})) ∈
V) |
101 | 43, 99, 7, 100 | fvmptd 6825 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝑁 − 1)) = ((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) ×
{1}))) |
102 | 101 | fveq1d 6719 |
. . . 4
⊢ (𝜑 → ((𝐹‘(𝑁 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((1...𝑁) × {1}))‘𝑛)) |
103 | 102 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑁 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((1...𝑁) × {1}))‘𝑛)) |
104 | | inidm 4133 |
. . . 4
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
105 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘𝑛)) |
106 | 11 | fvconst2 7019 |
. . . . 5
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {1})‘𝑛) = 1) |
107 | 106 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {1})‘𝑛) = 1) |
108 | 24, 13, 1, 1, 104, 105, 107 | ofval 7479 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((1...𝑁) × {1}))‘𝑛) = (((1st
‘(1st ‘𝑇))‘𝑛) + 1)) |
109 | 103, 108 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑁 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))‘𝑛) + 1)) |
110 | | elmapi 8530 |
. . . . . . 7
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
111 | 22, 110 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
112 | 111 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
113 | | elfzonn0 13287 |
. . . . 5
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
114 | 112, 113 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
115 | 114 | nn0cnd 12152 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
116 | | pncan1 11256 |
. . 3
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ ℂ → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) − 1) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
117 | 115, 116 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) − 1) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
118 | 1, 10, 13, 24, 109, 107, 117 | offveq 7492 |
1
⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘f −
((1...𝑁) × {1})) =
(1st ‘(1st ‘𝑇))) |