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 ) → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ 𝑊 ) ) )