# Metamath Proof Explorer

## Theorem cshweqrep

Description: If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018) (Revised by AV, 7-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion cshweqrep ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑗 ∈ ℕ0 ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑥 = 0 → ( 𝑥 · 𝐿 ) = ( 0 · 𝐿 ) )
2 1 oveq2d ( 𝑥 = 0 → ( 𝐼 + ( 𝑥 · 𝐿 ) ) = ( 𝐼 + ( 0 · 𝐿 ) ) )
3 2 fvoveq1d ( 𝑥 = 0 → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + ( 0 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
4 3 eqeq2d ( 𝑥 = 0 → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 0 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
5 4 imbi2d ( 𝑥 = 0 → ( ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 0 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
6 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 · 𝐿 ) = ( 𝑦 · 𝐿 ) )
7 6 oveq2d ( 𝑥 = 𝑦 → ( 𝐼 + ( 𝑥 · 𝐿 ) ) = ( 𝐼 + ( 𝑦 · 𝐿 ) ) )
8 7 fvoveq1d ( 𝑥 = 𝑦 → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
9 8 eqeq2d ( 𝑥 = 𝑦 → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
10 9 imbi2d ( 𝑥 = 𝑦 → ( ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
11 oveq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · 𝐿 ) = ( ( 𝑦 + 1 ) · 𝐿 ) )
12 11 oveq2d ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐼 + ( 𝑥 · 𝐿 ) ) = ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) )
13 12 fvoveq1d ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
14 13 eqeq2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
15 14 imbi2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
16 oveq1 ( 𝑥 = 𝑗 → ( 𝑥 · 𝐿 ) = ( 𝑗 · 𝐿 ) )
17 16 oveq2d ( 𝑥 = 𝑗 → ( 𝐼 + ( 𝑥 · 𝐿 ) ) = ( 𝐼 + ( 𝑗 · 𝐿 ) ) )
18 17 fvoveq1d ( 𝑥 = 𝑗 → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
19 18 eqeq2d ( 𝑥 = 𝑗 → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
20 19 imbi2d ( 𝑥 = 𝑗 → ( ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑥 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
21 zcn ( 𝐿 ∈ ℤ → 𝐿 ∈ ℂ )
22 21 mul02d ( 𝐿 ∈ ℤ → ( 0 · 𝐿 ) = 0 )
23 22 adantl ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( 0 · 𝐿 ) = 0 )
24 23 adantr ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 0 · 𝐿 ) = 0 )
25 24 oveq2d ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 + ( 0 · 𝐿 ) ) = ( 𝐼 + 0 ) )
26 elfzoelz ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℤ )
27 26 zcnd ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℂ )
28 27 addid1d ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 + 0 ) = 𝐼 )
29 28 ad2antll ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 + 0 ) = 𝐼 )
30 25 29 eqtrd ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 + ( 0 · 𝐿 ) ) = 𝐼 )
31 30 oveq1d ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝐼 + ( 0 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝐼 mod ( ♯ ‘ 𝑊 ) ) )
32 zmodidfzoimp ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 mod ( ♯ ‘ 𝑊 ) ) = 𝐼 )
33 32 ad2antll ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 mod ( ♯ ‘ 𝑊 ) ) = 𝐼 )
34 31 33 eqtr2d ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝐼 = ( ( 𝐼 + ( 0 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) )
35 34 fveq2d ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 0 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
36 fveq1 ( 𝑊 = ( 𝑊 cyclShift 𝐿 ) → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 cyclShift 𝐿 ) ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
37 36 eqcoms ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 cyclShift 𝐿 ) ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
38 37 ad2antrl ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 cyclShift 𝐿 ) ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
39 38 adantl ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 cyclShift 𝐿 ) ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
40 simprll ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝑊 ∈ Word 𝑉 )
41 simprlr ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝐿 ∈ ℤ )
42 elfzo0 ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
43 nn0z ( 𝐼 ∈ ℕ0𝐼 ∈ ℤ )
44 43 adantr ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → 𝐼 ∈ ℤ )
45 nn0z ( 𝑦 ∈ ℕ0𝑦 ∈ ℤ )
46 zmulcl ( ( 𝑦 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑦 · 𝐿 ) ∈ ℤ )
47 45 46 sylan ( ( 𝑦 ∈ ℕ0𝐿 ∈ ℤ ) → ( 𝑦 · 𝐿 ) ∈ ℤ )
48 47 ancoms ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑦 · 𝐿 ) ∈ ℤ )
49 zaddcl ( ( 𝐼 ∈ ℤ ∧ ( 𝑦 · 𝐿 ) ∈ ℤ ) → ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ )
50 44 48 49 syl2an ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ )
51 simplr ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
52 50 51 jca ( ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
53 52 ex ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
54 53 3adant3 ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
55 42 54 sylbi ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
56 55 adantl ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
57 56 expd ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 ∈ ℤ → ( 𝑦 ∈ ℕ0 → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) ) )
58 57 com12 ( 𝐿 ∈ ℤ → ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑦 ∈ ℕ0 → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) ) )
59 58 adantl ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑦 ∈ ℕ0 → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) ) )
60 59 imp ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑦 ∈ ℕ0 → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
61 60 impcom ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
62 zmodfzo ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
63 61 62 syl ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
64 cshwidxmod ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ∧ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝐿 ) ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) ) )
65 40 41 63 64 syl3anc ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝑊 cyclShift 𝐿 ) ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) ) )
66 nn0re ( 𝐼 ∈ ℕ0𝐼 ∈ ℝ )
67 zre ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
68 nn0re ( 𝑦 ∈ ℕ0𝑦 ∈ ℝ )
69 nnrp ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
70 remulcl ( ( 𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑦 · 𝐿 ) ∈ ℝ )
71 70 ancoms ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 · 𝐿 ) ∈ ℝ )
72 readdcl ( ( 𝐼 ∈ ℝ ∧ ( 𝑦 · 𝐿 ) ∈ ℝ ) → ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℝ )
73 71 72 sylan2 ( ( 𝐼 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℝ )
74 73 ancoms ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℝ )
75 74 adantl ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℝ )
76 simprll ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → 𝐿 ∈ ℝ )
77 simpl ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
78 modaddmod ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) )
79 75 76 77 78 syl3anc ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) )
80 recn ( 𝐼 ∈ ℝ → 𝐼 ∈ ℂ )
81 80 adantl ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → 𝐼 ∈ ℂ )
82 70 recnd ( ( 𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑦 · 𝐿 ) ∈ ℂ )
83 82 ancoms ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 · 𝐿 ) ∈ ℂ )
84 83 adantr ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( 𝑦 · 𝐿 ) ∈ ℂ )
85 recn ( 𝐿 ∈ ℝ → 𝐿 ∈ ℂ )
86 85 adantr ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝐿 ∈ ℂ )
87 86 adantr ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → 𝐿 ∈ ℂ )
88 81 84 87 addassd ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) + 𝐿 ) = ( 𝐼 + ( ( 𝑦 · 𝐿 ) + 𝐿 ) ) )
89 recn ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
90 89 adantl ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
91 1cnd ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
92 90 91 86 adddird ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 1 ) · 𝐿 ) = ( ( 𝑦 · 𝐿 ) + ( 1 · 𝐿 ) ) )
93 85 mulid2d ( 𝐿 ∈ ℝ → ( 1 · 𝐿 ) = 𝐿 )
94 93 adantr ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 · 𝐿 ) = 𝐿 )
95 94 oveq2d ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 · 𝐿 ) + ( 1 · 𝐿 ) ) = ( ( 𝑦 · 𝐿 ) + 𝐿 ) )
96 92 95 eqtr2d ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 · 𝐿 ) + 𝐿 ) = ( ( 𝑦 + 1 ) · 𝐿 ) )
97 96 adantr ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( ( 𝑦 · 𝐿 ) + 𝐿 ) = ( ( 𝑦 + 1 ) · 𝐿 ) )
98 97 oveq2d ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( 𝐼 + ( ( 𝑦 · 𝐿 ) + 𝐿 ) ) = ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) )
99 88 98 eqtrd ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) + 𝐿 ) = ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) )
100 99 adantl ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) + 𝐿 ) = ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) )
101 100 oveq1d ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) )
102 79 101 eqtrd ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ ∧ ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) )
103 102 ex ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
104 69 103 syl ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐼 ∈ ℝ ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
105 104 expd ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐼 ∈ ℝ → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
106 105 com12 ( ( 𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 𝐼 ∈ ℝ → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
107 67 68 106 syl2an ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 𝐼 ∈ ℝ → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
108 107 com13 ( 𝐼 ∈ ℝ → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
109 66 108 syl ( 𝐼 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
110 109 imp ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
111 110 3adant3 ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
112 42 111 sylbi ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
113 112 expd ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐿 ∈ ℤ → ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
114 113 adantld ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
115 114 adantl ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
116 115 impcom ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
117 116 impcom ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) )
118 117 fveq2d ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 ‘ ( ( ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) + 𝐿 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
119 39 65 118 3eqtrd ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
120 119 eqeq2d ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
121 120 biimpd ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
122 121 ex ( 𝑦 ∈ ℕ0 → ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
123 122 a2d ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑦 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( ( 𝑦 + 1 ) · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
124 5 10 15 20 35 123 nn0ind ( 𝑗 ∈ ℕ0 → ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
125 124 com12 ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑗 ∈ ℕ0 → ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
126 125 ralrimiv ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) ∧ ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ∀ 𝑗 ∈ ℕ0 ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
127 126 ex ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑗 ∈ ℕ0 ( 𝑊𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )