Step | Hyp | Ref
| Expression |
1 | | f1f 6014 |
. . . . 5
⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → 𝐹:(0..^(#‘𝐹))⟶𝐴) |
2 | | iswrdi 13164 |
. . . . 5
⊢ (𝐹:(0..^(#‘𝐹))⟶𝐴 → 𝐹 ∈ Word 𝐴) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → 𝐹 ∈ Word 𝐴) |
4 | | cshwf 13397 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴) |
5 | 4 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴) |
6 | 5 | adantr 480 |
. . . . . . 7
⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴) |
7 | | feq1 5939 |
. . . . . . . 8
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴)) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴)) |
9 | 6, 8 | mpbird 246 |
. . . . . 6
⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(#‘𝐹))⟶𝐴) |
10 | | dff13 6416 |
. . . . . . . 8
⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 ↔ (𝐹:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
11 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
14 | | cshwidxmod 13400 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))) |
15 | 14 | 3expia 1259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))) |
16 | 15 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))) |
17 | 16 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))) |
19 | 18 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))) |
20 | 13, 19 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))) |
21 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
22 | 21 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
24 | | cshwidxmod 13400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))) |
25 | 24 | 3expia 1259 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))) |
26 | 25 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))) |
27 | 26 | adantld 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))) |
28 | 27 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))) |
29 | 23, 28 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))) |
30 | 20, 29 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))) |
31 | 30 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))) |
32 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0..^(#‘𝐹)) ↔ (𝑖 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑖 < (#‘𝐹))) |
33 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℤ) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → 𝑖 ∈
ℤ) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → 𝑖 ∈
ℤ) |
36 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → 𝑆 ∈
ℤ) |
37 | 35, 36 | zaddcld 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → (𝑖 + 𝑆) ∈
ℤ) |
38 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (#‘𝐹)
∈ ℕ) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → (#‘𝐹) ∈ ℕ) |
40 | 37, 39 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → ((𝑖 +
𝑆) ∈ ℤ ∧
(#‘𝐹) ∈
ℕ)) |
41 | 40 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧
(#‘𝐹) ∈
ℕ))) |
42 | 41 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ)
→ ((𝑖 + 𝑆) ∈ ℤ ∧
(#‘𝐹) ∈
ℕ))) |
43 | 42 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → ((𝐺 =
(𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
44 | 43 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑖 <
(#‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
45 | 32, 44 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
47 | 46 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ)) |
48 | | zmodfzo 12555 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑖 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹))) |
50 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (0..^(#‘𝐹)) ↔ (𝑗 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑗 < (#‘𝐹))) |
51 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℤ) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → 𝑗 ∈
ℤ) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → 𝑗 ∈
ℤ) |
54 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → 𝑆 ∈
ℤ) |
55 | 53, 54 | zaddcld 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → (𝑗 + 𝑆) ∈
ℤ) |
56 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (#‘𝐹)
∈ ℕ) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → (#‘𝐹) ∈ ℕ) |
58 | 55, 57 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ)) → ((𝑗 +
𝑆) ∈ ℤ ∧
(#‘𝐹) ∈
ℕ)) |
59 | 58 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (𝑆 ∈
ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧
(#‘𝐹) ∈
ℕ))) |
60 | 59 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑗 <
(#‘𝐹)) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
61 | 50, 60 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ (0..^(#‘𝐹)) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
62 | 61 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ ℤ → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
63 | 62 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
64 | 63 | adantld 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ))) |
65 | 64 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈
ℕ)) |
66 | | zmodfzo 12555 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ) → ((𝑗 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑗 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹))) |
68 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → (𝐹‘𝑥) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))) |
69 | 68 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦))) |
70 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → (𝑥 = 𝑦 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦)) |
71 | 69, 70 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦))) |
72 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))) |
73 | 72 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))) |
74 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → (((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) |
75 | 73, 74 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → (((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))) |
76 | 71, 75 | rspc2v 3293 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑖 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹)) ∧ ((𝑗 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))) |
77 | 49, 67, 76 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))) |
78 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) |
79 | | addmodlteq 12607 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)) ∧ 𝑆 ∈ ℤ) → (((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)) ↔ 𝑖 = 𝑗)) |
80 | 79 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) ∧ 𝑆 ∈ ℤ) → (((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)) ↔ 𝑖 = 𝑗)) |
81 | 80 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)) ↔ 𝑖 = 𝑗)) |
82 | 81 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) |
83 | 82 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))) |
84 | 83 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))) |
85 | 84 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) |
87 | 78, 86 | sylibrd 248 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗)) |
88 | 87 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗))) |
89 | 77, 88 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗))) |
90 | 89 | impancom 455 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗))) |
91 | 90 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗)) |
92 | 31, 91 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
93 | 92 | ralrimivva 2954 |
. . . . . . . . . . 11
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
94 | 93 | 3exp1 1275 |
. . . . . . . . . 10
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
95 | 94 | com14 94 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
96 | 95 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
97 | 10, 96 | sylbi 206 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
98 | 97 | 3imp1 1272 |
. . . . . 6
⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
99 | 9, 98 | jca 553 |
. . . . 5
⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
100 | 99 | 3exp1 1275 |
. . . 4
⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))) |
101 | 3, 100 | mpd 15 |
. . 3
⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
102 | 101 | 3imp 1249 |
. 2
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
103 | | dff13 6416 |
. 2
⊢ (𝐺:(0..^(#‘𝐹))–1-1→𝐴 ↔ (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
104 | 102, 103 | sylibr 223 |
1
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(#‘𝐹))–1-1→𝐴) |