# Metamath Proof Explorer

## Theorem cshwsidrepsw

Description: If cyclically shifting a word of length being a prime number by a number of positions which is not divisible by the prime number results in the word itself, the word is a "repeated symbol word". (Contributed by AV, 18-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Assertion cshwsidrepsw ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )

### Proof

Step Hyp Ref Expression
1 simpr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ♯ ‘ 𝑊 ) ∈ ℙ )
2 1 adantr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℙ )
3 simp1 ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝐿 ∈ ℤ )
4 3 adantl ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → 𝐿 ∈ ℤ )
5 simpr2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 )
6 2 4 5 3jca ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ) )
7 6 adantr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ) )
8 simpr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 modprmn0modprm0 ( ( ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) )
10 7 8 9 sylc ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
11 oveq1 ( 𝑘 = 𝑗 → ( 𝑘 · 𝐿 ) = ( 𝑗 · 𝐿 ) )
12 11 oveq2d ( 𝑘 = 𝑗 → ( 𝑖 + ( 𝑘 · 𝐿 ) ) = ( 𝑖 + ( 𝑗 · 𝐿 ) ) )
13 12 fvoveq1d ( 𝑘 = 𝑗 → ( 𝑊 ‘ ( ( 𝑖 + ( 𝑘 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
14 13 eqeq2d ( 𝑘 = 𝑗 → ( ( 𝑊𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑘 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
15 simpl ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 𝑊 ∈ Word 𝑉 )
16 15 3 anim12i ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) )
17 16 adantr ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) )
18 17 adantl ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) )
19 simpr3 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝑊 cyclShift 𝐿 ) = 𝑊 )
20 19 anim1i ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
21 20 adantl ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
22 cshweqrep ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝐿 ) = 𝑊𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑊𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑘 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
23 18 21 22 sylc ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑊𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑘 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
24 elfzonn0 ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑗 ∈ ℕ0 )
25 24 ad2antrr ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑗 ∈ ℕ0 )
26 14 23 25 rspcdva ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
27 fveq2 ( ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 → ( 𝑊 ‘ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) )
28 27 adantl ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) → ( 𝑊 ‘ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) )
29 28 adantr ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 ‘ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) )
30 26 29 eqtrd ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) ∧ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
31 30 ex ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 ) → ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
32 31 rexlimiva ( ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑖 + ( 𝑗 · 𝐿 ) ) mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
33 10 32 mpcom ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
34 33 ralrimiva ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
35 repswsymballbi ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
36 35 ad2antrr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
37 34 36 mpbird ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )
38 37 ex ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )