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