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