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

Proof

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