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 ( ♯ ‘ 𝑊 ) ) ) ) )