Proof of Theorem poimirlem20
Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . . . 9
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) − 1) = (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) |
2 | 1 | eleq1d 2686 |
. . . . . . . 8
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) − 1) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)) ∈ (0..^𝐾))) |
3 | | oveq2 6658 |
. . . . . . . . 9
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) − 0) = (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) |
4 | 3 | eleq1d 2686 |
. . . . . . . 8
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) − 0) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)) ∈ (0..^𝐾))) |
5 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
6 | 5 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → (((1st
‘(1st ‘𝑇))‘𝑛) − 1) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1)) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − 1) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1)) |
8 | | poimirlem22.2 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
9 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
10 | | poimirlem22.s |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
11 | 9, 10 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
12 | 8, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
13 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
15 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
17 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
19 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
20 | 14, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
21 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
22 | | f1oeq1 6127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
23 | 21, 22 | elab 3350 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
24 | 20, 23 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
25 | | f1of 6137 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
27 | | poimir.0 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℕ) |
28 | | elfz1end 12371 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
29 | 27, 28 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
30 | 26, 29 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)) |
31 | 18, 30 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ (0..^𝐾)) |
32 | | elfzonn0 12512 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈
ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈
ℕ0) |
34 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑇))‘𝑁) ∈ V |
35 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → (𝑛 ∈ (1...𝑁) ↔ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁))) |
36 | 35 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)))) |
37 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → (𝑝‘𝑛) = (𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
38 | 37 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → ((𝑝‘𝑛) ≠ 0 ↔ (𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0)) |
39 | 38 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → (∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0 ↔ ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0)) |
40 | 36, 39 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑁) → (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) ↔ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0))) |
41 | | poimirlem22.3 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
42 | 34, 40, 41 | vtocl 3259 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0) |
43 | 30, 42 | mpdan 702 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0) |
44 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) = (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
45 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
46 | 18, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
48 | | 1ex 10035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
V |
49 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑦))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) |
51 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
V |
52 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) |
54 | 50, 53 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
55 | | dff1o3 6143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) |
56 | 55 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) |
57 | 24, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → Fun ◡(2nd ‘(1st
‘𝑇))) |
58 | | imain 5974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))) |
60 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0) |
61 | 60 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) |
62 | 61 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1)) |
63 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅) |
65 | 64 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
66 | | ima0 5481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
67 | 65, 66 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅) |
68 | 59, 67 | sylan9req 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅) |
69 | | fnun 5997 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) ∧ (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))) |
70 | 54, 68, 69 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))) |
71 | | imaundi 5545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
72 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ) |
73 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ℕ =
(ℤ≥‘1) |
74 | 72, 73 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
(ℤ≥‘1)) |
75 | 60, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈
(ℤ≥‘1)) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈
(ℤ≥‘1)) |
77 | 27 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝑁 ∈ ℂ) |
78 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
80 | 79 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
81 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑦)) |
82 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘𝑦)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘𝑦)) |
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘𝑦)) |
85 | 80, 84 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘𝑦)) |
86 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑦 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) |
87 | 76, 85, 86 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) |
88 | 87 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))) |
89 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
90 | | foima 6120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
91 | 24, 89, 90 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
93 | 88, 92 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁)) |
94 | 71, 93 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = (1...𝑁)) |
95 | 94 | fneq2d 5982 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) ↔ ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
96 | 70, 95 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
97 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1...𝑁) ∈
V |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V) |
99 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
100 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
101 | | f1ofn 6138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
102 | 24, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
104 | | fzss1 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) ∈
(ℤ≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁)) |
105 | 75, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁)) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁)) |
107 | | eluzp1p1 11713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
108 | | uzss 11708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1)) →
(ℤ≥‘((𝑁 − 1) + 1)) ⊆
(ℤ≥‘(𝑦 + 1))) |
109 | 81, 107, 108 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) →
(ℤ≥‘((𝑁 − 1) + 1)) ⊆
(ℤ≥‘(𝑦 + 1))) |
110 | 109 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) →
(ℤ≥‘((𝑁 − 1) + 1)) ⊆
(ℤ≥‘(𝑦 + 1))) |
111 | 27 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝑁 ∈ ℤ) |
112 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑁)) |
114 | 79 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 →
(ℤ≥‘((𝑁 − 1) + 1)) =
(ℤ≥‘𝑁)) |
115 | 113, 114 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
117 | 110, 116 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) |
118 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁)) |
120 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
121 | 103, 106,
119, 120 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
122 | | fvun2 6270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) ∧ ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
123 | 50, 53, 122 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
124 | 68, 121, 123 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
125 | 51 | fvconst2 6469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇))‘𝑁) ∈ ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) → ((((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑁)) = 0) |
126 | 121, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑁)) = 0) |
127 | 124, 126 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = 0) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = 0) |
129 | 47, 96, 98, 98, 99, 100, 128 | ofval 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) + 0)) |
130 | 30, 129 | mpidan 704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) + 0)) |
131 | 33 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℂ) |
132 | 131 | addid1d 10236 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) + 0) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
133 | 132 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) + 0) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
134 | 130, 133 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
135 | 44, 134 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑦)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
136 | 135 | adantllr 755 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ ran 𝐹) ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑦)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
137 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
138 | 137 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
139 | 138 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
140 | 139 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 𝑇 → ⦋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})))) |
141 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
143 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
144 | 143 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
145 | 144 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
146 | 143 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
147 | 146 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
148 | 145, 147 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
149 | 142, 148 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
150 | 149 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 𝑇 → ⦋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})))) |
151 | 140, 150 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → ⦋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})))) |
152 | 151 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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}))))) |
153 | 152 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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})))))) |
154 | 153, 10 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
155 | 154 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
156 | 8, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
157 | 61 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ) |
158 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
159 | 111, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
160 | 159 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
162 | 27 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → 𝑁 ∈ ℝ) |
163 | 162 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
164 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1)) |
165 | 164 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1)) |
166 | 162 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
167 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
168 | 157, 161,
163, 165, 167 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) |
169 | | poimirlem21.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (2nd
‘𝑇) = 𝑁) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) = 𝑁) |
171 | 168, 170 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < (2nd ‘𝑇)) |
172 | 171 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦) |
173 | 172 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
174 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑦 ∈ V |
175 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦)) |
176 | 175 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑦))) |
177 | 176 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1})) |
178 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1)) |
179 | 178 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁)) |
180 | 179 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
181 | 180 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) |
182 | 177, 181 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = 𝑦 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
183 | 182 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = 𝑦 → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
184 | 174, 183 | csbie 3559 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
⦋𝑦 /
𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
185 | 173, 184 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
186 | 185 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
187 | 156, 186 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
188 | 187 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ran 𝐹 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
189 | 188 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
190 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
191 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) ∈ V |
192 | 190, 191 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑦)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
193 | 189, 192 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑦)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
194 | 193 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑦)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
195 | 136, 194 | r19.29a 3078 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
196 | 195 | neeq1d 2853 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0 ↔ ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0)) |
197 | 196 | biimpd 219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0)) |
198 | 197 | rexlimdva 3031 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0)) |
199 | 43, 198 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0) |
200 | | elnnne0 11306 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℕ ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℕ0 ∧
((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ≠ 0)) |
201 | 33, 199, 200 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℕ) |
202 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℕ → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈
ℕ0) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈
ℕ0) |
204 | | elfzo0 12508 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℕ0 ∧ 𝐾 ∈ ℕ ∧
((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) < 𝐾)) |
205 | 31, 204 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℕ0 ∧ 𝐾 ∈ ℕ ∧
((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) < 𝐾)) |
206 | 205 | simp2d 1074 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℕ) |
207 | 203 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈
ℝ) |
208 | 33 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ ℝ) |
209 | 206 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℝ) |
210 | 208 | ltm1d 10956 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) < ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁))) |
211 | | elfzolt2 12479 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) < 𝐾) |
212 | 31, 211 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) < 𝐾) |
213 | 207, 208,
209, 210, 212 | lttrd 10198 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) < 𝐾) |
214 | | elfzo0 12508 |
. . . . . . . . . . . 12
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈ (0..^𝐾) ↔ ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ (((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) < 𝐾)) |
215 | 203, 206,
213, 214 | syl3anbrc 1246 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈ (0..^𝐾)) |
216 | 215 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁)) → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑁)) − 1) ∈ (0..^𝐾)) |
217 | 7, 216 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − 1) ∈ (0..^𝐾)) |
218 | 217 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − 1) ∈ (0..^𝐾)) |
219 | 18 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
220 | | elfzonn0 12512 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
222 | 221 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
223 | 222 | subid1d 10381 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − 0) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
224 | 223, 219 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − 0) ∈ (0..^𝐾)) |
225 | 224 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − 0) ∈ (0..^𝐾)) |
226 | 2, 4, 218, 225 | ifbothda 4123 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)) ∈ (0..^𝐾)) |
227 | | eqid 2622 |
. . . . . . 7
⊢ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) |
228 | 226, 227 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))):(1...𝑁)⟶(0..^𝐾)) |
229 | | ovex 6678 |
. . . . . . 7
⊢
(0..^𝐾) ∈
V |
230 | 229, 97 | elmap 7886 |
. . . . . 6
⊢ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) ∈ ((0..^𝐾) ↑𝑚
(1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))):(1...𝑁)⟶(0..^𝐾)) |
231 | 228, 230 | sylibr 224 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) ∈ ((0..^𝐾) ↑𝑚
(1...𝑁))) |
232 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → 𝑛 ∈ ((1 + 1)...𝑁)) |
233 | | 1z 11407 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℤ |
234 | | peano2z 11418 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ → (1 + 1) ∈ ℤ) |
235 | 233, 234 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1)
∈ ℤ |
236 | 111, 235 | jctil 560 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1 + 1) ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
237 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ∈ ℤ) |
238 | 237, 233 | jctir 561 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ((1 + 1)...𝑁) → (𝑛 ∈ ℤ ∧ 1 ∈
ℤ)) |
239 | | fzsubel 12377 |
. . . . . . . . . . . . . 14
⊢ ((((1 +
1) ∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑛
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((1 + 1)...𝑁) ↔ (𝑛 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
240 | 236, 238,
239 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 ∈ ((1 + 1)...𝑁) ↔ (𝑛 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
241 | 232, 240 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1))) |
242 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
243 | 242, 242 | pncan3oi 10297 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
− 1) = 1 |
244 | 243 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢ (((1 + 1)
− 1)...(𝑁 − 1))
= (1...(𝑁 −
1)) |
245 | 241, 244 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 − 1) ∈ (1...(𝑁 − 1))) |
246 | 245 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑛 − 1) ∈ (1...(𝑁 − 1))) |
247 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → 𝑦 ∈ (1...(𝑁 − 1))) |
248 | 159, 233 | jctil 560 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 ∈ ℤ ∧
(𝑁 − 1) ∈
ℤ)) |
249 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1...(𝑁 − 1)) → 𝑦 ∈ ℤ) |
250 | 249, 233 | jctir 561 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1...(𝑁 − 1)) → (𝑦 ∈ ℤ ∧ 1 ∈
ℤ)) |
251 | | fzaddel 12375 |
. . . . . . . . . . . . . . 15
⊢ (((1
∈ ℤ ∧ (𝑁
− 1) ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑦 ∈
(1...(𝑁 − 1)) ↔
(𝑦 + 1) ∈ ((1 +
1)...((𝑁 − 1) +
1)))) |
252 | 248, 250,
251 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 ∈ (1...(𝑁 − 1)) ↔ (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))) |
253 | 247, 252 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))) |
254 | 79 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) |
255 | 254 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) |
256 | 253, 255 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 + 1) ∈ ((1 + 1)...𝑁)) |
257 | 237 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ∈ ℂ) |
258 | 249 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1...(𝑁 − 1)) → 𝑦 ∈ ℂ) |
259 | | subadd2 10285 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑦 ∈
ℂ) → ((𝑛 −
1) = 𝑦 ↔ (𝑦 + 1) = 𝑛)) |
260 | 242, 259 | mp3an2 1412 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑛 − 1) = 𝑦 ↔ (𝑦 + 1) = 𝑛)) |
261 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑛 − 1) ↔ (𝑛 − 1) = 𝑦) |
262 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑦 + 1) ↔ (𝑦 + 1) = 𝑛) |
263 | 260, 261,
262 | 3bitr4g 303 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) |
264 | 257, 258,
263 | syl2anr 495 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (1...(𝑁 − 1)) ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) |
265 | 264 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...(𝑁 − 1)) → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) |
266 | 265 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) |
267 | | reu6i 3397 |
. . . . . . . . . . . 12
⊢ (((𝑦 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) → ∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1)) |
268 | 256, 266,
267 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → ∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1)) |
269 | 268 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (1...(𝑁 − 1))∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1)) |
270 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) = (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) |
271 | 270 | f1ompt 6382 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ↔ (∀𝑛 ∈ ((1 + 1)...𝑁)(𝑛 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑦 ∈ (1...(𝑁 − 1))∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))) |
272 | 246, 269,
271 | sylanbrc 698 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1))) |
273 | | f1osng 6177 |
. . . . . . . . . 10
⊢ ((1
∈ V ∧ 𝑁 ∈
ℕ) → {〈1, 𝑁〉}:{1}–1-1-onto→{𝑁}) |
274 | 48, 27, 273 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → {〈1, 𝑁〉}:{1}–1-1-onto→{𝑁}) |
275 | 160, 162 | ltnled 10184 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
276 | 166, 275 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
277 | | elfzle2 12345 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
278 | 276, 277 | nsyl 135 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
279 | | disjsn 4246 |
. . . . . . . . . 10
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
280 | 278, 279 | sylibr 224 |
. . . . . . . . 9
⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) |
281 | | 1re 10039 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
282 | 281 | ltp1i 10927 |
. . . . . . . . . . . . 13
⊢ 1 < (1
+ 1) |
283 | 235 | zrei 11383 |
. . . . . . . . . . . . . 14
⊢ (1 + 1)
∈ ℝ |
284 | 281, 283 | ltnlei 10158 |
. . . . . . . . . . . . 13
⊢ (1 <
(1 + 1) ↔ ¬ (1 + 1) ≤ 1) |
285 | 282, 284 | mpbi 220 |
. . . . . . . . . . . 12
⊢ ¬ (1
+ 1) ≤ 1 |
286 | | elfzle1 12344 |
. . . . . . . . . . . 12
⊢ (1 ∈
((1 + 1)...𝑁) → (1 +
1) ≤ 1) |
287 | 285, 286 | mto 188 |
. . . . . . . . . . 11
⊢ ¬ 1
∈ ((1 + 1)...𝑁) |
288 | | disjsn 4246 |
. . . . . . . . . . 11
⊢ ((((1 +
1)...𝑁) ∩ {1}) =
∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁)) |
289 | 287, 288 | mpbir 221 |
. . . . . . . . . 10
⊢ (((1 +
1)...𝑁) ∩ {1}) =
∅ |
290 | | f1oun 6156 |
. . . . . . . . . 10
⊢ ((((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ∧ {〈1, 𝑁〉}:{1}–1-1-onto→{𝑁}) ∧ ((((1 + 1)...𝑁) ∩ {1}) = ∅ ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)) → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {〈1, 𝑁〉}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁})) |
291 | 289, 290 | mpanr1 719 |
. . . . . . . . 9
⊢ ((((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ∧ {〈1, 𝑁〉}:{1}–1-1-onto→{𝑁}) ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {〈1, 𝑁〉}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁})) |
292 | 272, 274,
280, 291 | syl21anc 1325 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {〈1, 𝑁〉}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁})) |
293 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 ∈ ((1 + 1)...𝑁) ↔ 1 ∈ ((1 + 1)...𝑁))) |
294 | 287, 293 | mtbiri 317 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → ¬ 𝑛 ∈ ((1 + 1)...𝑁)) |
295 | 294 | necon2ai 2823 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ≠ 1) |
296 | | ifnefalse 4098 |
. . . . . . . . . . . . 13
⊢ (𝑛 ≠ 1 → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1)) |
297 | 295, 296 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ((1 + 1)...𝑁) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1)) |
298 | 297 | mpteq2ia 4740 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) |
299 | 298 | uneq1i 3763 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∪ {〈1, 𝑁〉}) = ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {〈1, 𝑁〉}) |
300 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
V) |
301 | | ssv 3625 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ V |
302 | 301, 27 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ V) |
303 | 27, 73 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
304 | | fzpred 12389 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁))) |
305 | 303, 304 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁))) |
306 | | uncom 3757 |
. . . . . . . . . . . 12
⊢ ({1}
∪ ((1 + 1)...𝑁)) = (((1
+ 1)...𝑁) ∪
{1}) |
307 | 305, 306 | syl6req 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 1)...𝑁) ∪ {1}) = (1...𝑁)) |
308 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = 𝑁) |
309 | 308 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 = 1) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = 𝑁) |
310 | 300, 302,
307, 309 | fmptapd 6437 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∪ {〈1, 𝑁〉}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) |
311 | 299, 310 | syl5eqr 2670 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {〈1, 𝑁〉}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) |
312 | 79, 303 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
313 | | uzid 11702 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
314 | | peano2uz 11741 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
315 | 159, 313,
314 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
316 | 79, 315 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
317 | | fzsplit2 12366 |
. . . . . . . . . . 11
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
318 | 312, 316,
317 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
319 | 79 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
320 | | fzsn 12383 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
321 | 111, 320 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
322 | 319, 321 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
323 | 322 | uneq2d 3767 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
324 | 318, 323 | eqtr2d 2657 |
. . . . . . . . 9
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁)) |
325 | 311, 307,
324 | f1oeq123d 6133 |
. . . . . . . 8
⊢ (𝜑 → (((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {〈1, 𝑁〉}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁))) |
326 | 292, 325 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁)) |
327 | | f1oco 6159 |
. . . . . . 7
⊢
(((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
328 | 24, 326, 327 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
329 | 97 | mptex 6486 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∈ V |
330 | 21, 329 | coex 7118 |
. . . . . . 7
⊢
((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ V |
331 | | f1oeq1 6127 |
. . . . . . 7
⊢ (𝑓 = ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁))) |
332 | 330, 331 | elab 3350 |
. . . . . 6
⊢
(((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
333 | 328, 332 | sylibr 224 |
. . . . 5
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
334 | | opelxpi 5148 |
. . . . 5
⊢ (((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) ∈ ((0..^𝐾) ↑𝑚
(1...𝑁)) ∧
((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉 ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
335 | 231, 333,
334 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉 ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
336 | 27 | nnnn0d 11351 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
337 | | 0elfz 12436 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
338 | 336, 337 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
339 | | opelxpi 5148 |
. . . 4
⊢
((〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉 ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 0 ∈ (0...𝑁)) → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ∈
((((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
340 | 335, 338,
339 | syl2anc 693 |
. . 3
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ∈
((((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
341 | | poimirlem22.1 |
. . . . 5
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁))) |
342 | 27, 10, 341, 8, 41, 169 | poimirlem19 33428 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
343 | | elfzle1 12344 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦) |
344 | | 0re 10040 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
345 | | lenlt 10116 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → (0 ≤ 𝑦 ↔ ¬ 𝑦 < 0)) |
346 | 344, 61, 345 | sylancr 695 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (0 ≤ 𝑦 ↔ ¬ 𝑦 < 0)) |
347 | 343, 346 | mpbid 222 |
. . . . . . . 8
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ¬ 𝑦 < 0) |
348 | 347 | iffalsed 4097 |
. . . . . . 7
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → if(𝑦 < 0, 𝑦, (𝑦 + 1)) = (𝑦 + 1)) |
349 | 348 | csbeq1d 3540 |
. . . . . 6
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))) |
350 | | ovex 6678 |
. . . . . . 7
⊢ (𝑦 + 1) ∈ V |
351 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1))) |
352 | 351 | imaeq2d 5466 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) = (((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))) |
353 | 352 | xpeq1d 5138 |
. . . . . . . . 9
⊢ (𝑗 = (𝑦 + 1) → ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) =
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ×
{1})) |
354 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1)) |
355 | 354 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁)) |
356 | 355 | imaeq2d 5466 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) = (((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))) |
357 | 356 | xpeq1d 5138 |
. . . . . . . . 9
⊢ (𝑗 = (𝑦 + 1) → ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) |
358 | 353, 357 | uneq12d 3768 |
. . . . . . . 8
⊢ (𝑗 = (𝑦 + 1) → (((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
359 | 358 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑗 = (𝑦 + 1) → ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
360 | 350, 359 | csbie 3559 |
. . . . . 6
⊢
⦋(𝑦 +
1) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
361 | 349, 360 | syl6eq 2672 |
. . . . 5
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
362 | 361 | mpteq2ia 4740 |
. . . 4
⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
363 | 342, 362 | syl6eqr 2674 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
364 | | opex 4932 |
. . . . . . . . . . 11
⊢
〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉 ∈
V |
365 | 364, 51 | op2ndd 7179 |
. . . . . . . . . 10
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(2nd ‘𝑡) =
0) |
366 | 365 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 → (𝑦 < (2nd
‘𝑡) ↔ 𝑦 < 0)) |
367 | 366 | ifbid 4108 |
. . . . . . . 8
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 → if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < 0, 𝑦, (𝑦 + 1))) |
368 | 367 | csbeq1d 3540 |
. . . . . . 7
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
⦋if(𝑦 <
(2nd ‘𝑡),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
369 | 364, 51 | op1std 7178 |
. . . . . . . . . 10
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(1st ‘𝑡) =
〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉) |
370 | 97 | mptex 6486 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))) ∈
V |
371 | 370, 330 | op1std 7178 |
. . . . . . . . . 10
⊢
((1st ‘𝑡) = 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉 → (1st
‘(1st ‘𝑡)) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))) |
372 | 369, 371 | syl 17 |
. . . . . . . . 9
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(1st ‘(1st ‘𝑡)) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))) |
373 | 370, 330 | op2ndd 7179 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑡) = 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉 → (2nd
‘(1st ‘𝑡)) = ((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))) |
374 | 369, 373 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(2nd ‘(1st ‘𝑡)) = ((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))) |
375 | 374 | imaeq1d 5465 |
. . . . . . . . . . 11
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) = (((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗))) |
376 | 375 | xpeq1d 5138 |
. . . . . . . . . 10
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) ×
{1})) |
377 | 374 | imaeq1d 5465 |
. . . . . . . . . . 11
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = (((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁))) |
378 | 377 | xpeq1d 5138 |
. . . . . . . . . 10
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})) |
379 | 376, 378 | uneq12d 3768 |
. . . . . . . . 9
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) |
380 | 372, 379 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
((1st ‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))) |
381 | 380 | csbeq2dv 3992 |
. . . . . . 7
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
⦋if(𝑦 < 0,
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))) |
382 | 368, 381 | eqtrd 2656 |
. . . . . 6
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
⦋if(𝑦 <
(2nd ‘𝑡),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))) |
383 | 382 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
384 | 383 | eqeq2d 2632 |
. . . 4
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
385 | 384, 10 | elrab2 3366 |
. . 3
⊢
(〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ∈ 𝑆 ↔ (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ∈
((((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0)))
∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪
((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
386 | 340, 363,
385 | sylanbrc 698 |
. 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ∈ 𝑆) |
387 | 364, 51 | op2ndd 7179 |
. . . . . 6
⊢ (𝑇 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 →
(2nd ‘𝑇) =
0) |
388 | 387 | eqcoms 2630 |
. . . . 5
⊢
(〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 = 𝑇 → (2nd
‘𝑇) =
0) |
389 | 27 | nnne0d 11065 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ≠ 0) |
390 | 389 | necomd 2849 |
. . . . . 6
⊢ (𝜑 → 0 ≠ 𝑁) |
391 | | neeq1 2856 |
. . . . . 6
⊢
((2nd ‘𝑇) = 0 → ((2nd ‘𝑇) ≠ 𝑁 ↔ 0 ≠ 𝑁)) |
392 | 390, 391 | syl5ibrcom 237 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝑇) = 0 →
(2nd ‘𝑇)
≠ 𝑁)) |
393 | 388, 392 | syl5 34 |
. . . 4
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 = 𝑇 → (2nd
‘𝑇) ≠ 𝑁)) |
394 | 393 | necon2d 2817 |
. . 3
⊢ (𝜑 → ((2nd
‘𝑇) = 𝑁 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ≠ 𝑇)) |
395 | 169, 394 | mpd 15 |
. 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ≠ 𝑇) |
396 | | neeq1 2856 |
. . 3
⊢ (𝑧 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 → (𝑧 ≠ 𝑇 ↔ 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ≠ 𝑇)) |
397 | 396 | rspcev 3309 |
. 2
⊢
((〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ∈ 𝑆 ∧ 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑁), 1, 0))), ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))〉, 0〉 ≠ 𝑇) → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
398 | 386, 395,
397 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |