Step |
Hyp |
Ref |
Expression |
1 |
|
hasheq0 |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) ) |
2 |
|
elfzo0 |
⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) ) |
3 |
|
elnnne0 |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) ) |
4 |
|
eqneqall |
⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
5 |
4
|
com12 |
⊢ ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
6 |
5
|
adantl |
⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
7 |
3 6
|
sylbi |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
8 |
7
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
9 |
2 8
|
sylbi |
⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
10 |
9
|
com13 |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
11 |
1 10
|
sylbird |
⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ∅ → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
12 |
11
|
com23 |
⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 = ∅ → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
13 |
12
|
imp |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 = ∅ → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) |
14 |
13
|
com12 |
⊢ ( 𝑊 = ∅ → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) |
15 |
|
simpl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 ) |
16 |
15
|
adantl |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑊 ∈ Word 𝑉 ) |
17 |
|
simpl |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑊 ≠ ∅ ) |
18 |
|
elfzoelz |
⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ ) |
19 |
18
|
ad2antll |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑁 ∈ ℤ ) |
20 |
|
cshwidx0mod |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) |
21 |
16 17 19 20
|
syl3anc |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) |
22 |
|
zmodidfzoimp |
⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = 𝑁 ) |
23 |
22
|
ad2antll |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = 𝑁 ) |
24 |
23
|
fveq2d |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝑁 ) ) |
25 |
21 24
|
eqtrd |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) |
26 |
25
|
ex |
⊢ ( 𝑊 ≠ ∅ → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) ) |
27 |
14 26
|
pm2.61ine |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ 𝑁 ) ) |