This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )