| Step | Hyp | Ref
| Expression |
| 1 | | f1f 6804 |
. . . . 5
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → 𝐹:(0..^(♯‘𝐹))⟶𝐴) |
| 2 | | iswrdi 14556 |
. . . . 5
⊢ (𝐹:(0..^(♯‘𝐹))⟶𝐴 → 𝐹 ∈ Word 𝐴) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → 𝐹 ∈ Word 𝐴) |
| 4 | | cshwf 14838 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴) |
| 5 | 4 | 3adant1 1131 |
. . . . . . . 8
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴) |
| 7 | | feq1 6716 |
. . . . . . . 8
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)) |
| 8 | 7 | adantl 481 |
. . . . . . 7
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)) |
| 9 | 6, 8 | mpbird 257 |
. . . . . 6
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))⟶𝐴) |
| 10 | | dff13 7275 |
. . . . . . . 8
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ↔ (𝐹:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 11 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
| 12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖)) |
| 14 | | cshwidxmod 14841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))) |
| 15 | 14 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))) |
| 16 | 15 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . 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 407 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))) |
| 20 | 13, 19 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))) |
| 21 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
| 22 | 21 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗)) |
| 24 | | cshwidxmod 14841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 25 | 24 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 26 | 25 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 27 | 26 | adantld 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 28 | 27 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 29 | 23, 28 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 30 | 20, 29 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 31 | 30 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 32 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈
(0..^(♯‘𝐹))
↔ (𝑖 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑖 < (♯‘𝐹))) |
| 33 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℤ) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → 𝑖
∈ ℤ) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑖
∈ ℤ) |
| 36 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑆
∈ ℤ) |
| 37 | 35, 36 | zaddcld 12726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (𝑖
+ 𝑆) ∈
ℤ) |
| 38 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (♯‘𝐹) ∈ ℕ) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (♯‘𝐹) ∈ ℕ) |
| 40 | 37, 39 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → ((𝑖
+ 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ)) |
| 41 | 40 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → ((𝑖
+ 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
| 42 | 41 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
| 43 | 42 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → ((𝐺
= (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 44 | 43 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑖 <
(♯‘𝐹)) →
((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 45 | 32, 44 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈
(0..^(♯‘𝐹))
→ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹)))
→ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 47 | 46 | impcom 407 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ)) |
| 48 | | zmodfzo 13934 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
| 50 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈
(0..^(♯‘𝐹))
↔ (𝑗 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑗 < (♯‘𝐹))) |
| 51 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℤ) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → 𝑗
∈ ℤ) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑗
∈ ℤ) |
| 54 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → 𝑆
∈ ℤ) |
| 55 | 53, 54 | zaddcld 12726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (𝑗
+ 𝑆) ∈
ℤ) |
| 56 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (♯‘𝐹) ∈ ℕ) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → (♯‘𝐹) ∈ ℕ) |
| 58 | 55, 57 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ)) → ((𝑗
+ 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ)) |
| 59 | 58 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (𝑆
∈ ℤ → ((𝑗 +
𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
| 60 | 59 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑗 <
(♯‘𝐹)) →
(𝑆 ∈ ℤ →
((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 61 | 50, 60 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈
(0..^(♯‘𝐹))
→ (𝑆 ∈ ℤ
→ ((𝑗 + 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
| 62 | 61 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ ℤ → (𝑗 ∈
(0..^(♯‘𝐹))
→ ((𝑗 + 𝑆) ∈ ℤ ∧
(♯‘𝐹) ∈
ℕ))) |
| 63 | 62 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 64 | 63 | adantld 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ))) |
| 65 | 64 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈
ℕ)) |
| 66 | | zmodfzo 13934 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) |
| 68 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦))) |
| 69 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → (𝑥 = 𝑦 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦)) |
| 70 | 68, 69 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦))) |
| 71 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 72 | 71 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 73 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 74 | 72, 73 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 75 | 70, 74 | rspc2v 3633 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ∧ ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) → (∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 76 | 49, 67, 75 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))) |
| 77 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 78 | | addmodlteq 13987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹))
∧ 𝑆 ∈ ℤ)
→ (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗)) |
| 79 | 78 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹)))
∧ 𝑆 ∈ ℤ)
→ (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗)) |
| 80 | 79 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹))))
→ (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗)) |
| 81 | 80 | bicomd 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈
(0..^(♯‘𝐹))
∧ 𝑗 ∈
(0..^(♯‘𝐹))))
→ (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 82 | 81 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) |
| 84 | 77, 83 | sylibrd 259 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)) |
| 85 | 84 | ex 412 |
. . . . . . . . . . . . . . . 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 451 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗))) |
| 88 | 87 | imp 406 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)) |
| 89 | 31, 88 | sylbid 240 |
. . . . . . . . . . . 12
⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
| 90 | 89 | ralrimivva 3202 |
. . . . . . . . . . 11
⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
| 91 | 90 | 3exp1 1353 |
. . . . . . . . . 10
⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
| 92 | 91 | com14 96 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
| 93 | 92 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
| 94 | 10, 93 | sylbi 217 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))) |
| 95 | 94 | 3imp1 1348 |
. . . . . 6
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)) |
| 96 | 9, 95 | jca 511 |
. . . . 5
⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
| 97 | 96 | 3exp1 1353 |
. . . 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 1111 |
. 2
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
| 100 | | dff13 7275 |
. 2
⊢ (𝐺:(0..^(♯‘𝐹))–1-1→𝐴 ↔ (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))) |
| 101 | 99, 100 | sylibr 234 |
1
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))–1-1→𝐴) |