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	addridd	⊢ ( 𝐼 ∈ ( 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	mullidd	⊢ ( 𝐿 ∈ ℝ → ( 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 ( ♯ ‘ 𝑊 ) ) ) ) )