# Metamath Proof Explorer

## Theorem cshwshashnsame

Description: If a word (not consisting of identical symbols) 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. (Contributed by AV, 19-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion cshwshashnsame ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ) )

### Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2 1 cshwsiun ( 𝑊 ∈ Word 𝑉𝑀 = 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )
3 2 ad2antrr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → 𝑀 = 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )
4 3 fveq2d ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ) )
5 fzofi ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin
6 5 a1i ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin )
7 snfi { ( 𝑊 cyclShift 𝑛 ) } ∈ Fin
8 7 a1i ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → { ( 𝑊 cyclShift 𝑛 ) } ∈ Fin )
9 id ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
10 9 cshwsdisj ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Disj 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )
11 6 8 10 hashiun ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ♯ ‘ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ) = Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ♯ ‘ { ( 𝑊 cyclShift 𝑛 ) } ) )
12 ovex ( 𝑊 cyclShift 𝑛 ) ∈ V
13 hashsng ( ( 𝑊 cyclShift 𝑛 ) ∈ V → ( ♯ ‘ { ( 𝑊 cyclShift 𝑛 ) } ) = 1 )
14 12 13 mp1i ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ♯ ‘ { ( 𝑊 cyclShift 𝑛 ) } ) = 1 )
15 14 sumeq2sdv ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ♯ ‘ { ( 𝑊 cyclShift 𝑛 ) } ) = Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 1 )
16 1cnd ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 1 ∈ ℂ )
17 fsumconst ( ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 1 = ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) · 1 ) )
18 5 16 17 sylancr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 1 = ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) · 1 ) )
19 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
20 19 adantr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
21 hashfzo0 ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
22 20 21 syl ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
23 22 oveq1d ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) · 1 ) = ( ( ♯ ‘ 𝑊 ) · 1 ) )
24 prmnn ( ( ♯ ‘ 𝑊 ) ∈ ℙ → ( ♯ ‘ 𝑊 ) ∈ ℕ )
25 24 nnred ( ( ♯ ‘ 𝑊 ) ∈ ℙ → ( ♯ ‘ 𝑊 ) ∈ ℝ )
26 25 adantl ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
27 ax-1rid ( ( ♯ ‘ 𝑊 ) ∈ ℝ → ( ( ♯ ‘ 𝑊 ) · 1 ) = ( ♯ ‘ 𝑊 ) )
28 26 27 syl ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( ♯ ‘ 𝑊 ) · 1 ) = ( ♯ ‘ 𝑊 ) )
29 18 23 28 3eqtrd ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 1 = ( ♯ ‘ 𝑊 ) )
30 29 adantr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 1 = ( ♯ ‘ 𝑊 ) )
31 15 30 eqtrd ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → Σ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ♯ ‘ { ( 𝑊 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑊 ) )
32 4 11 31 3eqtrd ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) )
33 32 ex ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ) )