Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
2 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
3 | 2 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
4 | 3 | ifbid 4058 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
5 | 4 | csbeq1d 3506 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
6 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
7 | 6 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
8 | 6 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
9 | 8 | imaeq1d 5384 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
10 | 9 | xpeq1d 5062 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
11 | 8 | imaeq1d 5384 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
12 | 11 | xpeq1d 5062 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
13 | 10, 12 | uneq12d 3730 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
14 | 7, 13 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
15 | 14 | csbeq2dv 3944 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
16 | 5, 15 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
17 | 16 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
18 | 17 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
19 | | poimirlem22.s |
. . . . . 6
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
20 | 18, 19 | elrab2 3333 |
. . . . 5
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
21 | 20 | simprbi 479 |
. . . 4
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
22 | 1, 21 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
23 | | breq1 4586 |
. . . . . . 7
⊢ (𝑦 = 0 → (𝑦 < (2nd ‘𝑇) ↔ 0 < (2nd
‘𝑇))) |
24 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 0 → 𝑦 = 0) |
25 | 23, 24 | ifbieq1d 4059 |
. . . . . 6
⊢ (𝑦 = 0 → if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) = if(0 < (2nd
‘𝑇), 0, (𝑦 + 1))) |
26 | | poimirlem5.2 |
. . . . . . 7
⊢ (𝜑 → 0 < (2nd
‘𝑇)) |
27 | 26 | iftrued 4044 |
. . . . . 6
⊢ (𝜑 → if(0 < (2nd
‘𝑇), 0, (𝑦 + 1)) = 0) |
28 | 25, 27 | sylan9eqr 2666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 0) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 0) |
29 | 28 | csbeq1d 3506 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 0) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
30 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
31 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → (1...𝑗) = (1...0)) |
32 | | fz10 12233 |
. . . . . . . . . . . . 13
⊢ (1...0) =
∅ |
33 | 31, 32 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → (1...𝑗) = ∅) |
34 | 33 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (𝑗 = 0 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
∅)) |
35 | 34 | xpeq1d 5062 |
. . . . . . . . . 10
⊢ (𝑗 = 0 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ ∅) ×
{1})) |
36 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
37 | | 0p1e1 11009 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
38 | 36, 37 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → (𝑗 + 1) = 1) |
39 | 38 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁)) |
40 | 39 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (𝑗 = 0 → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑁))) |
41 | 40 | xpeq1d 5062 |
. . . . . . . . . 10
⊢ (𝑗 = 0 → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
42 | 35, 41 | uneq12d 3730 |
. . . . . . . . 9
⊢ (𝑗 = 0 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}))) |
43 | | ima0 5400 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
44 | 43 | xpeq1i 5059 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) = (∅
× {1}) |
45 | | 0xp 5122 |
. . . . . . . . . . . 12
⊢ (∅
× {1}) = ∅ |
46 | 44, 45 | eqtri 2632 |
. . . . . . . . . . 11
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) =
∅ |
47 | 46 | uneq1i 3725 |
. . . . . . . . . 10
⊢
((((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = (∅ ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
48 | | uncom 3719 |
. . . . . . . . . 10
⊢ (∅
∪ (((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) ∪
∅) |
49 | | un0 3919 |
. . . . . . . . . 10
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) ∪ ∅) =
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) |
50 | 47, 48, 49 | 3eqtri 2636 |
. . . . . . . . 9
⊢
((((2nd ‘(1st ‘𝑇)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) |
51 | 42, 50 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑗 = 0 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑗 = 0 → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0}))) |
53 | 30, 52 | csbie 3525 |
. . . . . 6
⊢
⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) |
54 | | elrabi 3328 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
55 | 54, 19 | eleq2s 2706 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
56 | 1, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
57 | | xp1st 7089 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
59 | | xp2nd 7090 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
61 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
62 | | f1oeq1 6040 |
. . . . . . . . . . . 12
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
63 | 61, 62 | elab 3319 |
. . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
64 | 60, 63 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
65 | | f1ofo 6057 |
. . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
66 | 64, 65 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
67 | | foima 6033 |
. . . . . . . . 9
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
69 | 68 | xpeq1d 5062 |
. . . . . . 7
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0})) |
70 | 69 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
(((2nd ‘(1st ‘𝑇)) “ (1...𝑁)) × {0})) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{0}))) |
71 | 53, 70 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{0}))) |
72 | 71 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{0}))) |
73 | 29, 72 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑦 = 0) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{0}))) |
74 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
75 | | nnm1nn0 11211 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
76 | 74, 75 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
77 | | 0elfz 12305 |
. . . 4
⊢ ((𝑁 − 1) ∈
ℕ0 → 0 ∈ (0...(𝑁 − 1))) |
78 | 76, 77 | syl 17 |
. . 3
⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1))) |
79 | | ovex 6577 |
. . . 4
⊢
((1st ‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) × {0})) ∈
V |
80 | 79 | a1i 11 |
. . 3
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) × {0})) ∈
V) |
81 | 22, 73, 78, 80 | fvmptd 6197 |
. 2
⊢ (𝜑 → (𝐹‘0) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{0}))) |
82 | | ovex 6577 |
. . . 4
⊢
(1...𝑁) ∈
V |
83 | 82 | a1i 11 |
. . 3
⊢ (𝜑 → (1...𝑁) ∈ V) |
84 | | xp1st 7089 |
. . . . 5
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
85 | 58, 84 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
86 | | elmapfn 7766 |
. . . 4
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
87 | 85, 86 | syl 17 |
. . 3
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
88 | | fnconstg 6006 |
. . . 4
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
89 | 30, 88 | mp1i 13 |
. . 3
⊢ (𝜑 → ((1...𝑁) × {0}) Fn (1...𝑁)) |
90 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘𝑛)) |
91 | 30 | fvconst2 6374 |
. . . 4
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
92 | 91 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
93 | | elmapi 7765 |
. . . . . . . 8
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
94 | 85, 93 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
95 | 94 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
96 | | elfzonn0 12380 |
. . . . . 6
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
97 | 95, 96 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
98 | 97 | nn0cnd 11230 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
99 | 98 | addid1d 10115 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
100 | 83, 87, 89, 87, 90, 92, 99 | offveq 6816 |
. 2
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) × {0})) =
(1st ‘(1st ‘𝑇))) |
101 | 81, 100 | eqtrd 2644 |
1
⊢ (𝜑 → (𝐹‘0) = (1st
‘(1st ‘𝑇))) |