Metamath Proof Explorer

Theorem cshwshash

Description: If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by AV, 19-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
Assertion cshwshash ⊢ W ∈ Word V ∧ W ∈ ℙ → M = W ∨ M = 1

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
2 repswsymballbi ⊢ W ∈ Word V → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
3 2 adantr ⊢ W ∈ Word V ∧ W ∈ ℙ → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
4 prmnn ⊢ W ∈ ℙ → W ∈ ℕ
5 4 nnge1d ⊢ W ∈ ℙ → 1 ≤ W
6 wrdsymb1 ⊢ W ∈ Word V ∧ 1 ≤ W → W ⁡ 0 ∈ V
7 5 6 sylan2 ⊢ W ∈ Word V ∧ W ∈ ℙ → W ⁡ 0 ∈ V
8 7 adantr ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ W = W ⁡ 0 repeatS W → W ⁡ 0 ∈ V
9 4 ad2antlr ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ W = W ⁡ 0 repeatS W → W ∈ ℕ
10 simpr ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ W = W ⁡ 0 repeatS W → W = W ⁡ 0 repeatS W
11 1 cshwrepswhash1 ⊢ W ⁡ 0 ∈ V ∧ W ∈ ℕ ∧ W = W ⁡ 0 repeatS W → M = 1
12 8 9 10 11 syl3anc ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ W = W ⁡ 0 repeatS W → M = 1
13 12 ex ⊢ W ∈ Word V ∧ W ∈ ℙ → W = W ⁡ 0 repeatS W → M = 1
14 3 13 sylbird ⊢ W ∈ Word V ∧ W ∈ ℙ → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → M = 1
15 olc ⊢ M = 1 → M = W ∨ M = 1
16 14 15 syl6com ⊢ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → W ∈ Word V ∧ W ∈ ℙ → M = W ∨ M = 1
17 rexnal ⊢ ∃ i ∈ 0 ..^ W ¬ W ⁡ i = W ⁡ 0 ↔ ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
18 df-ne ⊢ W ⁡ i ≠ W ⁡ 0 ↔ ¬ W ⁡ i = W ⁡ 0
19 18 bicomi ⊢ ¬ W ⁡ i = W ⁡ 0 ↔ W ⁡ i ≠ W ⁡ 0
20 19 rexbii ⊢ ∃ i ∈ 0 ..^ W ¬ W ⁡ i = W ⁡ 0 ↔ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0
21 17 20 bitr3i ⊢ ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 ↔ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0
22 1 cshwshashnsame ⊢ W ∈ Word V ∧ W ∈ ℙ → ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → M = W
23 orc ⊢ M = W → M = W ∨ M = 1
24 22 23 syl6com ⊢ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W ∈ Word V ∧ W ∈ ℙ → M = W ∨ M = 1
25 21 24 sylbi ⊢ ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → W ∈ Word V ∧ W ∈ ℙ → M = W ∨ M = 1
26 16 25 pm2.61i ⊢ W ∈ Word V ∧ W ∈ ℙ → M = W ∨ M = 1