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 ⊢ W ∈ Word V ∧ W ∈ ℙ → L ∈ ℤ ∧ L mod W ≠ 0 ∧ W cyclShift L = W → W = W ⁡ 0 repeatS W

Proof

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