Step | Hyp | Ref
| Expression |
1 | | f1f 6633 |
. . . . 5
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → 𝐹:(0..^(♯‘𝐹))⟶𝐴) |
2 | | iswrdi 14097 |
. . . . 5
⊢ (𝐹:(0..^(♯‘𝐹))⟶𝐴 → 𝐹 ∈ Word 𝐴) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → 𝐹 ∈ Word 𝐴) |
4 | | cshwf 14389 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴) |
5 | 4 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴) |
6 | 5 | adantr 484 |
. . . . . . 7
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴) |
7 | | feq1 6544 |
. . . . . . . 8
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)) |
8 | 7 | adantl 485 |
. . . . . . 7
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)) |
9 | 6, 8 | mpbird 260 |
. . . . . 6
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))⟶𝐴) |
10 | | dff13 7085 |
. . . . . . . 8
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ↔ (𝐹:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
11 | | fveq1 6734 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
12 | 11 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
13 | 12 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
14 | | cshwidxmod 14392 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))) |
15 | 14 | 3expia 1123 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))) |
16 | 15 | 3adant1 1132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))) |
17 | 16 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(0..^(♯‘𝐹))
→ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))) |
18 | 17 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹)))
→ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))) |
19 | 18 | impcom 411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))) |
20 | 13, 19 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))) |
21 | | fveq1 6734 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
22 | 21 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
24 | | cshwidxmod 14392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
25 | 24 | 3expia 1123 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
26 | 25 | 3adant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
27 | 26 | adantld 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
28 | 27 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
29 | 23, 28 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
30 | 20, 29 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
31 | 30 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
32 | | elfzo0 13307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈
(0..^(♯‘𝐹))
↔ (𝑖 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑖 < (♯‘𝐹))) |
33 | | nn0z 12224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℤ) |
34 | 33 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → 𝑖
∈ ℤ) |
35 | 34 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑖
∈ ℤ) |
36 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑆
∈ ℤ) |
37 | 35, 36 | zaddcld 12310 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (𝑖
+ 𝑆) ∈
ℤ) |
38 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (♯‘𝐹) ∈ ℕ) |
39 | 38 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (♯‘𝐹) ∈ ℕ) |
40 | 37, 39 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → ((𝑖
+ 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ)) |
41 | 40 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → ((𝑖
+ 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
42 | 41 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
43 | 42 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → ((𝐺
= (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
44 | 43 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑖 <
(♯‘𝐹)) →
((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
45 | 32, 44 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈
(0..^(♯‘𝐹))
→ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
46 | 45 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹)))
→ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
47 | 46 | impcom 411 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ)) |
48 | | zmodfzo 13491 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
50 | | elfzo0 13307 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈
(0..^(♯‘𝐹))
↔ (𝑗 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑗 < (♯‘𝐹))) |
51 | | nn0z 12224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℤ) |
52 | 51 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → 𝑗
∈ ℤ) |
53 | 52 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑗
∈ ℤ) |
54 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑆
∈ ℤ) |
55 | 53, 54 | zaddcld 12310 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (𝑗
+ 𝑆) ∈
ℤ) |
56 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (♯‘𝐹) ∈ ℕ) |
57 | 56 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (♯‘𝐹) ∈ ℕ) |
58 | 55, 57 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → ((𝑗
+ 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ)) |
59 | 58 | expcom 417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (𝑆
∈ ℤ → ((𝑗 +
𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
60 | 59 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑗 <
(♯‘𝐹)) →
(𝑆 ∈ ℤ →
((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
61 | 50, 60 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈
(0..^(♯‘𝐹))
→ (𝑆 ∈ ℤ
→ ((𝑗 + 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
62 | 61 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ ℤ → (𝑗 ∈
(0..^(♯‘𝐹))
→ ((𝑗 + 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
63 | 62 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
64 | 63 | adantld 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
65 | 64 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ)) |
66 | | zmodfzo 13491 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
68 | | fveqeq2 6744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦))) |
69 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → (𝑥 = 𝑦 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦)) |
70 | 68, 69 | imbi12d 348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦))) |
71 | | fveq2 6735 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
72 | 71 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
73 | | eqeq2 2750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
74 | 72, 73 | imbi12d 348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))) |
75 | 70, 74 | rspc2v 3559 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ∧ ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) → (∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))) |
76 | 49, 67, 75 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))) |
77 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
78 | | addmodlteq 13543 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹))
∧ 𝑆 ∈ ℤ)
→ (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗)) |
79 | 78 | 3expa 1120 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹)))
∧ 𝑆 ∈ ℤ)
→ (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗)) |
80 | 79 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹))))
→ (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗)) |
81 | 80 | bicomd 226 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹))))
→ (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
82 | 81 | 3ad2antl3 1189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
83 | 82 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
84 | 77, 83 | sylibrd 262 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)) |
85 | 84 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗))) |
86 | 76, 85 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗))) |
87 | 86 | impancom 455 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗))) |
88 | 87 | imp 410 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)) |
89 | 31, 88 | sylbid 243 |
. . . . . . . . . . . 12
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
90 | 89 | ralrimivva 3113 |
. . . . . . . . . . 11
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
91 | 90 | 3exp1 1354 |
. . . . . . . . . 10
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
92 | 91 | com14 96 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
93 | 92 | adantl 485 |
. . . . . . . 8
⊢ ((𝐹:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
94 | 10, 93 | sylbi 220 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
95 | 94 | 3imp1 1349 |
. . . . . 6
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
96 | 9, 95 | jca 515 |
. . . . 5
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
97 | 96 | 3exp1 1354 |
. . . 4
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))) |
98 | 3, 97 | mpd 15 |
. . 3
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
99 | 98 | 3imp 1113 |
. 2
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
100 | | dff13 7085 |
. 2
⊢ (𝐺:(0..^(♯‘𝐹))–1-1→𝐴 ↔ (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
101 | 99, 100 | sylibr 237 |
1
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))–1-1→𝐴) |