Step | Hyp | Ref
| Expression |
1 | | wrdfn 13969 |
. . . . . 6
⊢ (𝐹 ∈ Word 𝑆 → 𝐹 Fn (0..^(♯‘𝐹))) |
2 | | fnfun 6438 |
. . . . . 6
⊢ (𝐹 Fn (0..^(♯‘𝐹)) → Fun 𝐹) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ Word 𝑆 → Fun 𝐹) |
4 | 3 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → Fun 𝐹) |
5 | | wrddm 13962 |
. . . . . 6
⊢ (𝐹 ∈ Word 𝑆 → dom 𝐹 = (0..^(♯‘𝐹))) |
6 | | difssd 4023 |
. . . . . . . . 9
⊢ ((dom
𝐹 =
(0..^(♯‘𝐹))
∧ 𝑁 =
(♯‘𝐹)) →
((0..^(♯‘𝐹))
∖ {𝐽}) ⊆
(0..^(♯‘𝐹))) |
7 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑁 = (♯‘𝐹) → (0..^𝑁) = (0..^(♯‘𝐹))) |
8 | 7 | difeq1d 4012 |
. . . . . . . . . 10
⊢ (𝑁 = (♯‘𝐹) → ((0..^𝑁) ∖ {𝐽}) = ((0..^(♯‘𝐹)) ∖ {𝐽})) |
9 | 8 | adantl 485 |
. . . . . . . . 9
⊢ ((dom
𝐹 =
(0..^(♯‘𝐹))
∧ 𝑁 =
(♯‘𝐹)) →
((0..^𝑁) ∖ {𝐽}) = ((0..^(♯‘𝐹)) ∖ {𝐽})) |
10 | | simpl 486 |
. . . . . . . . 9
⊢ ((dom
𝐹 =
(0..^(♯‘𝐹))
∧ 𝑁 =
(♯‘𝐹)) →
dom 𝐹 =
(0..^(♯‘𝐹))) |
11 | 6, 9, 10 | 3sstr4d 3924 |
. . . . . . . 8
⊢ ((dom
𝐹 =
(0..^(♯‘𝐹))
∧ 𝑁 =
(♯‘𝐹)) →
((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹) |
12 | 11 | a1d 25 |
. . . . . . 7
⊢ ((dom
𝐹 =
(0..^(♯‘𝐹))
∧ 𝑁 =
(♯‘𝐹)) →
(𝐽 ∈ (0..^𝑁) → ((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹)) |
13 | 12 | ex 416 |
. . . . . 6
⊢ (dom
𝐹 =
(0..^(♯‘𝐹))
→ (𝑁 =
(♯‘𝐹) →
(𝐽 ∈ (0..^𝑁) → ((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹))) |
14 | 5, 13 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ Word 𝑆 → (𝑁 = (♯‘𝐹) → (𝐽 ∈ (0..^𝑁) → ((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹))) |
15 | 14 | 3imp 1112 |
. . . 4
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → ((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹) |
16 | 4, 15 | jca 515 |
. . 3
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (Fun 𝐹 ∧ ((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹)) |
17 | | dfimafn 6732 |
. . 3
⊢ ((Fun
𝐹 ∧ ((0..^𝑁) ∖ {𝐽}) ⊆ dom 𝐹) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = {𝑧 ∣ ∃𝑥 ∈ ((0..^𝑁) ∖ {𝐽})(𝐹‘𝑥) = 𝑧}) |
18 | 16, 17 | syl 17 |
. 2
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = {𝑧 ∣ ∃𝑥 ∈ ((0..^𝑁) ∖ {𝐽})(𝐹‘𝑥) = 𝑧}) |
19 | | modsumfzodifsn 13403 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝑦 ∈ (1..^𝑁)) → ((𝑦 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |
20 | 19 | 3ad2antl3 1188 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → ((𝑦 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |
21 | | oveq2 7178 |
. . . . . . . . . 10
⊢
((♯‘𝐹) =
𝑁 → ((𝑦 + 𝐽) mod (♯‘𝐹)) = ((𝑦 + 𝐽) mod 𝑁)) |
22 | 21 | eqcoms 2746 |
. . . . . . . . 9
⊢ (𝑁 = (♯‘𝐹) → ((𝑦 + 𝐽) mod (♯‘𝐹)) = ((𝑦 + 𝐽) mod 𝑁)) |
23 | 22 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑁 = (♯‘𝐹) → (((𝑦 + 𝐽) mod (♯‘𝐹)) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ ((𝑦 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽}))) |
24 | 23 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝑦 + 𝐽) mod (♯‘𝐹)) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ ((𝑦 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽}))) |
25 | 24 | adantr 484 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → (((𝑦 + 𝐽) mod (♯‘𝐹)) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ ((𝑦 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽}))) |
26 | 20, 25 | mpbird 260 |
. . . . 5
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → ((𝑦 + 𝐽) mod (♯‘𝐹)) ∈ ((0..^𝑁) ∖ {𝐽})) |
27 | | modfzo0difsn 13402 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝑥 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod 𝑁)) |
28 | 27 | 3ad2antl3 1188 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod 𝑁)) |
29 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑁 = (♯‘𝐹) → ((𝑦 + 𝐽) mod 𝑁) = ((𝑦 + 𝐽) mod (♯‘𝐹))) |
30 | 29 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝑁 = (♯‘𝐹) → ((𝑦 + 𝐽) mod (♯‘𝐹)) = ((𝑦 + 𝐽) mod 𝑁)) |
31 | 30 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑁 = (♯‘𝐹) → (𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹)) ↔ 𝑥 = ((𝑦 + 𝐽) mod 𝑁))) |
32 | 31 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑁 = (♯‘𝐹) → (∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹)) ↔ ∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod 𝑁))) |
33 | 32 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹)) ↔ ∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod 𝑁))) |
34 | 33 | adantr 484 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ((0..^𝑁) ∖ {𝐽})) → (∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹)) ↔ ∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod 𝑁))) |
35 | 28, 34 | mpbird 260 |
. . . . 5
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑦 ∈ (1..^𝑁)𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹))) |
36 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹)) → (𝐹‘𝑥) = (𝐹‘((𝑦 + 𝐽) mod (♯‘𝐹)))) |
37 | 36 | 3ad2ant3 1136 |
. . . . . . 7
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹))) → (𝐹‘𝑥) = (𝐹‘((𝑦 + 𝐽) mod (♯‘𝐹)))) |
38 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝑆) |
39 | | elfzoelz 13129 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
40 | 39 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐽 ∈ ℤ) |
41 | 40 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → 𝐽 ∈ ℤ) |
42 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (𝑁 = (♯‘𝐹) → (1..^𝑁) = (1..^(♯‘𝐹))) |
43 | 42 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝑁 = (♯‘𝐹) → (𝑦 ∈ (1..^𝑁) ↔ 𝑦 ∈ (1..^(♯‘𝐹)))) |
44 | | fzo0ss1 13158 |
. . . . . . . . . . . . 13
⊢
(1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹)) |
45 | 44 | sseli 3873 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(1..^(♯‘𝐹))
→ 𝑦 ∈
(0..^(♯‘𝐹))) |
46 | 43, 45 | syl6bi 256 |
. . . . . . . . . . 11
⊢ (𝑁 = (♯‘𝐹) → (𝑦 ∈ (1..^𝑁) → 𝑦 ∈ (0..^(♯‘𝐹)))) |
47 | 46 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑦 ∈ (1..^𝑁) → 𝑦 ∈ (0..^(♯‘𝐹)))) |
48 | 47 | imp 410 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → 𝑦 ∈ (0..^(♯‘𝐹))) |
49 | | cshwidxmod 14254 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝐽)‘𝑦) = (𝐹‘((𝑦 + 𝐽) mod (♯‘𝐹)))) |
50 | 49 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝐹‘((𝑦 + 𝐽) mod (♯‘𝐹))) = ((𝐹 cyclShift 𝐽)‘𝑦)) |
51 | 38, 41, 48, 50 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁)) → (𝐹‘((𝑦 + 𝐽) mod (♯‘𝐹))) = ((𝐹 cyclShift 𝐽)‘𝑦)) |
52 | 51 | 3adant3 1133 |
. . . . . . 7
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹))) → (𝐹‘((𝑦 + 𝐽) mod (♯‘𝐹))) = ((𝐹 cyclShift 𝐽)‘𝑦)) |
53 | 37, 52 | eqtrd 2773 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹))) → (𝐹‘𝑥) = ((𝐹 cyclShift 𝐽)‘𝑦)) |
54 | 53 | eqeq1d 2740 |
. . . . 5
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑦 ∈ (1..^𝑁) ∧ 𝑥 = ((𝑦 + 𝐽) mod (♯‘𝐹))) → ((𝐹‘𝑥) = 𝑧 ↔ ((𝐹 cyclShift 𝐽)‘𝑦) = 𝑧)) |
55 | 26, 35, 54 | rexxfrd2 5280 |
. . . 4
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑥 ∈ ((0..^𝑁) ∖ {𝐽})(𝐹‘𝑥) = 𝑧 ↔ ∃𝑦 ∈ (1..^𝑁)((𝐹 cyclShift 𝐽)‘𝑦) = 𝑧)) |
56 | 55 | abbidv 2802 |
. . 3
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → {𝑧 ∣ ∃𝑥 ∈ ((0..^𝑁) ∖ {𝐽})(𝐹‘𝑥) = 𝑧} = {𝑧 ∣ ∃𝑦 ∈ (1..^𝑁)((𝐹 cyclShift 𝐽)‘𝑦) = 𝑧}) |
57 | 39 | anim2i 620 |
. . . . . . 7
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ)) |
58 | 57 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ)) |
59 | | cshwfn 14252 |
. . . . . 6
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐽 ∈ ℤ) → (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) |
61 | | fnfun 6438 |
. . . . . . 7
⊢ ((𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹)) → Fun (𝐹 cyclShift 𝐽)) |
62 | 61 | adantl 485 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) → Fun (𝐹 cyclShift 𝐽)) |
63 | 42, 44 | eqsstrdi 3931 |
. . . . . . . . 9
⊢ (𝑁 = (♯‘𝐹) → (1..^𝑁) ⊆ (0..^(♯‘𝐹))) |
64 | 63 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (1..^𝑁) ⊆ (0..^(♯‘𝐹))) |
65 | 64 | adantr 484 |
. . . . . . 7
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) → (1..^𝑁) ⊆ (0..^(♯‘𝐹))) |
66 | | fndm 6440 |
. . . . . . . 8
⊢ ((𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹)) → dom (𝐹 cyclShift 𝐽) = (0..^(♯‘𝐹))) |
67 | 66 | adantl 485 |
. . . . . . 7
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) → dom (𝐹 cyclShift 𝐽) = (0..^(♯‘𝐹))) |
68 | 65, 67 | sseqtrrd 3918 |
. . . . . 6
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) → (1..^𝑁) ⊆ dom (𝐹 cyclShift 𝐽)) |
69 | 62, 68 | jca 515 |
. . . . 5
⊢ (((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) ∧ (𝐹 cyclShift 𝐽) Fn (0..^(♯‘𝐹))) → (Fun (𝐹 cyclShift 𝐽) ∧ (1..^𝑁) ⊆ dom (𝐹 cyclShift 𝐽))) |
70 | 60, 69 | mpdan 687 |
. . . 4
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (Fun (𝐹 cyclShift 𝐽) ∧ (1..^𝑁) ⊆ dom (𝐹 cyclShift 𝐽))) |
71 | | dfimafn 6732 |
. . . 4
⊢ ((Fun
(𝐹 cyclShift 𝐽) ∧ (1..^𝑁) ⊆ dom (𝐹 cyclShift 𝐽)) → ((𝐹 cyclShift 𝐽) “ (1..^𝑁)) = {𝑧 ∣ ∃𝑦 ∈ (1..^𝑁)((𝐹 cyclShift 𝐽)‘𝑦) = 𝑧}) |
72 | 70, 71 | syl 17 |
. . 3
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐹 cyclShift 𝐽) “ (1..^𝑁)) = {𝑧 ∣ ∃𝑦 ∈ (1..^𝑁)((𝐹 cyclShift 𝐽)‘𝑦) = 𝑧}) |
73 | 56, 72 | eqtr4d 2776 |
. 2
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → {𝑧 ∣ ∃𝑥 ∈ ((0..^𝑁) ∖ {𝐽})(𝐹‘𝑥) = 𝑧} = ((𝐹 cyclShift 𝐽) “ (1..^𝑁))) |
74 | 18, 73 | eqtrd 2773 |
1
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐽) “ (1..^𝑁))) |