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∈WordV|∃n∈0..^WWcyclShiftn=w
Assertion cshwshash ⊢W∈WordV∧W∈ℙ→M=W∨M=1

Proof

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