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 ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
Assertion cshwshashnsame ⊢ W ∈ Word V ∧ W ∈ ℙ → ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → M = W

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
2 1 cshwsiun ⊢ W ∈ Word V → M = ⋃ n ∈ 0 ..^ W W cyclShift n
3 2 ad2antrr ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → M = ⋃ n ∈ 0 ..^ W W cyclShift n
4 3 fveq2d ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → M = ⋃ n ∈ 0 ..^ W W cyclShift n
5 fzofi ⊢ 0 ..^ W ∈ Fin
6 5 a1i ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → 0 ..^ W ∈ Fin
7 snfi ⊢ W cyclShift n ∈ Fin
8 7 a1i ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ n ∈ 0 ..^ W → W cyclShift n ∈ Fin
9 id ⊢ W ∈ Word V ∧ W ∈ ℙ → W ∈ Word V ∧ W ∈ ℙ
10 9 cshwsdisj ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → Disj n ∈ 0 ..^ W W cyclShift n
11 6 8 10 hashiun ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → ⋃ n ∈ 0 ..^ W W cyclShift n = ∑ n ∈ 0 ..^ W W cyclShift n
12 ovex ⊢ W cyclShift n ∈ V
13 hashsng ⊢ W cyclShift n ∈ V → W cyclShift n = 1
14 12 13 mp1i ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift n = 1
15 14 sumeq2sdv ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → ∑ n ∈ 0 ..^ W W cyclShift n = ∑ n ∈ 0 ..^ W 1
16 1cnd ⊢ W ∈ Word V ∧ W ∈ ℙ → 1 ∈ ℂ
17 fsumconst ⊢ 0 ..^ W ∈ Fin ∧ 1 ∈ ℂ → ∑ n ∈ 0 ..^ W 1 = 0 ..^ W ⋅ 1
18 5 16 17 sylancr ⊢ W ∈ Word V ∧ W ∈ ℙ → ∑ n ∈ 0 ..^ W 1 = 0 ..^ W ⋅ 1
19 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
20 19 adantr ⊢ W ∈ Word V ∧ W ∈ ℙ → W ∈ ℕ 0
21 hashfzo0 ⊢ W ∈ ℕ 0 → 0 ..^ W = W
22 20 21 syl ⊢ W ∈ Word V ∧ W ∈ ℙ → 0 ..^ W = W
23 22 oveq1d ⊢ W ∈ Word V ∧ W ∈ ℙ → 0 ..^ W ⋅ 1 = W ⋅ 1
24 prmnn ⊢ W ∈ ℙ → W ∈ ℕ
25 24 nnred ⊢ W ∈ ℙ → W ∈ ℝ
26 25 adantl ⊢ W ∈ Word V ∧ W ∈ ℙ → W ∈ ℝ
27 ax-1rid ⊢ W ∈ ℝ → W ⋅ 1 = W
28 26 27 syl ⊢ W ∈ Word V ∧ W ∈ ℙ → W ⋅ 1 = W
29 18 23 28 3eqtrd ⊢ W ∈ Word V ∧ W ∈ ℙ → ∑ n ∈ 0 ..^ W 1 = W
30 29 adantr ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → ∑ n ∈ 0 ..^ W 1 = W
31 15 30 eqtrd ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → ∑ n ∈ 0 ..^ W W cyclShift n = W
32 4 11 31 3eqtrd ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → M = W
33 32 ex ⊢ W ∈ Word V ∧ W ∈ ℙ → ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → M = W