Step | Hyp | Ref
| Expression |
1 | | ffn 5958 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
2 | 1 | 3ad2ant3 1077 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → 𝐹 Fn 𝐴) |
3 | | cshwfn 13398 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) Fn (0..^(#‘𝑊))) |
4 | 3 | 3adant3 1074 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝑊 cyclShift 𝑁) Fn (0..^(#‘𝑊))) |
5 | | cshwrn 13399 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) ⊆ 𝐴) |
6 | 5 | 3adant3 1074 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → ran (𝑊 cyclShift 𝑁) ⊆ 𝐴) |
7 | | fnco 5913 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ (𝑊 cyclShift 𝑁) Fn (0..^(#‘𝑊)) ∧ ran (𝑊 cyclShift 𝑁) ⊆ 𝐴) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) Fn (0..^(#‘𝑊))) |
8 | 2, 4, 6, 7 | syl3anc 1318 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) Fn (0..^(#‘𝑊))) |
9 | | wrdco 13428 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
10 | 9 | 3adant2 1073 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
11 | | simp2 1055 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → 𝑁 ∈ ℤ) |
12 | | cshwfn 13398 |
. . . 4
⊢ (((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑁 ∈ ℤ) → ((𝐹 ∘ 𝑊) cyclShift 𝑁) Fn (0..^(#‘(𝐹 ∘ 𝑊)))) |
13 | 10, 11, 12 | syl2anc 691 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) cyclShift 𝑁) Fn (0..^(#‘(𝐹 ∘ 𝑊)))) |
14 | | lenco 13429 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) |
15 | 14 | 3adant2 1073 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) |
16 | 15 | oveq2d 6565 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (0..^(#‘(𝐹 ∘ 𝑊))) = (0..^(#‘𝑊))) |
17 | 16 | fneq2d 5896 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (((𝐹 ∘ 𝑊) cyclShift 𝑁) Fn (0..^(#‘(𝐹 ∘ 𝑊))) ↔ ((𝐹 ∘ 𝑊) cyclShift 𝑁) Fn (0..^(#‘𝑊)))) |
18 | 13, 17 | mpbid 221 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑊) cyclShift 𝑁) Fn (0..^(#‘𝑊))) |
19 | 15 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) |
20 | 19 | oveq2d 6565 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))) = ((𝑖 + 𝑁) mod (#‘𝑊))) |
21 | 20 | fveq2d 6107 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊)))) = (𝑊‘((𝑖 + 𝑁) mod (#‘𝑊)))) |
22 | 21 | fveq2d 6107 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝐹‘(𝑊‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))))) = (𝐹‘(𝑊‘((𝑖 + 𝑁) mod (#‘𝑊))))) |
23 | | wrdfn 13174 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐴 → 𝑊 Fn (0..^(#‘𝑊))) |
24 | 23 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → 𝑊 Fn (0..^(#‘𝑊))) |
25 | 24 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑊 Fn (0..^(#‘𝑊))) |
26 | | elfzoelz 12339 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → 𝑖 ∈ ℤ) |
27 | | zaddcl 11294 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 + 𝑁) ∈ ℤ) |
28 | 26, 11, 27 | syl2anr 494 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑖 + 𝑁) ∈ ℤ) |
29 | | elfzo0 12376 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^(#‘𝑊)) ↔ (𝑖 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝑖 < (#‘𝑊))) |
30 | 29 | simp2bi 1070 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (#‘𝑊) ∈
ℕ) |
31 | 30 | adantl 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (#‘𝑊) ∈ ℕ) |
32 | | zmodfzo 12555 |
. . . . . . 7
⊢ (((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) |
33 | 28, 31, 32 | syl2anc 691 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) |
34 | 15 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → ((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))) = ((𝑖 + 𝑁) mod (#‘𝑊))) |
35 | 34 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))) ∈ (0..^(#‘𝑊)) ↔ ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))) |
36 | 35 | adantr 480 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))) ∈ (0..^(#‘𝑊)) ↔ ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))) |
37 | 33, 36 | mpbird 246 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))) ∈ (0..^(#‘𝑊))) |
38 | | fvco2 6183 |
. . . . 5
⊢ ((𝑊 Fn (0..^(#‘𝑊)) ∧ ((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))) ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊)))) = (𝐹‘(𝑊‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊)))))) |
39 | 25, 37, 38 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ 𝑊)‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊)))) = (𝐹‘(𝑊‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊)))))) |
40 | | simpl1 1057 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑊 ∈ Word 𝐴) |
41 | 11 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑁 ∈ ℤ) |
42 | | simpr 476 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑖 ∈ (0..^(#‘𝑊))) |
43 | | cshwidxmod 13400 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝑖) = (𝑊‘((𝑖 + 𝑁) mod (#‘𝑊)))) |
44 | 43 | fveq2d 6107 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝐹‘((𝑊 cyclShift 𝑁)‘𝑖)) = (𝐹‘(𝑊‘((𝑖 + 𝑁) mod (#‘𝑊))))) |
45 | 40, 41, 42, 44 | syl3anc 1318 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝐹‘((𝑊 cyclShift 𝑁)‘𝑖)) = (𝐹‘(𝑊‘((𝑖 + 𝑁) mod (#‘𝑊))))) |
46 | 22, 39, 45 | 3eqtr4rd 2655 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝐹‘((𝑊 cyclShift 𝑁)‘𝑖)) = ((𝐹 ∘ 𝑊)‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))))) |
47 | | fvco2 6183 |
. . . 4
⊢ (((𝑊 cyclShift 𝑁) Fn (0..^(#‘𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ (𝑊 cyclShift 𝑁))‘𝑖) = (𝐹‘((𝑊 cyclShift 𝑁)‘𝑖))) |
48 | 4, 47 | sylan 487 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ (𝑊 cyclShift 𝑁))‘𝑖) = (𝐹‘((𝑊 cyclShift 𝑁)‘𝑖))) |
49 | 10 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
50 | 15 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (#‘𝑊) = (#‘(𝐹 ∘ 𝑊))) |
51 | 50 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (0..^(#‘𝑊)) = (0..^(#‘(𝐹 ∘ 𝑊)))) |
52 | 51 | eleq2d 2673 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(#‘(𝐹 ∘ 𝑊))))) |
53 | 52 | biimpa 500 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑖 ∈ (0..^(#‘(𝐹 ∘ 𝑊)))) |
54 | | cshwidxmod 13400 |
. . . 4
⊢ (((𝐹 ∘ 𝑊) ∈ Word 𝐵 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘(𝐹 ∘ 𝑊)))) → (((𝐹 ∘ 𝑊) cyclShift 𝑁)‘𝑖) = ((𝐹 ∘ 𝑊)‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))))) |
55 | 49, 41, 53, 54 | syl3anc 1318 |
. . 3
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝐹 ∘ 𝑊) cyclShift 𝑁)‘𝑖) = ((𝐹 ∘ 𝑊)‘((𝑖 + 𝑁) mod (#‘(𝐹 ∘ 𝑊))))) |
56 | 46, 48, 55 | 3eqtr4d 2654 |
. 2
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝐹 ∘ (𝑊 cyclShift 𝑁))‘𝑖) = (((𝐹 ∘ 𝑊) cyclShift 𝑁)‘𝑖)) |
57 | 8, 18, 56 | eqfnfvd 6222 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁)) |