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 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion cshwshash ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2 repswsymballbi ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
3 2 adantr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
4 prmnn ( ( ♯ ‘ 𝑊 ) ∈ ℙ → ( ♯ ‘ 𝑊 ) ∈ ℕ )
5 4 nnge1d ( ( ♯ ‘ 𝑊 ) ∈ ℙ → 1 ≤ ( ♯ ‘ 𝑊 ) )
6 wrdsymb1 ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
7 5 6 sylan2 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
8 7 adantr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
9 4 ad2antlr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
10 simpr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )
11 1 cshwrepswhash1 ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑀 ) = 1 )
12 8 9 10 11 syl3anc ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑀 ) = 1 )
13 12 ex ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑀 ) = 1 ) )
14 3 13 sylbird ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( ♯ ‘ 𝑀 ) = 1 ) )
15 olc ( ( ♯ ‘ 𝑀 ) = 1 → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) )
16 14 15 syl6com ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) )
17 rexnal ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
18 df-ne ( ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ↔ ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
19 18 bicomi ( ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) )
20 19 rexbii ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) )
21 17 20 bitr3i ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) )
22 1 cshwshashnsame ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ) )
23 orc ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) )
24 22 23 syl6com ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) )
25 21 24 sylbi ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) ) )
26 16 25 pm2.61i ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ∨ ( ♯ ‘ 𝑀 ) = 1 ) )