Metamath Proof Explorer

Theorem cshwsidrepswmod0

Description: If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 (modulo the length of the word) or the word must be a "repeated symbol word". (Contributed by AV, 18-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Assertion cshwsidrepswmod0 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 orc ⊢ ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
2 1 2a1d ⊢ ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) ) )
3 3simpa ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
4 3 ad2antlr ⊢ ( ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
5 simplr3 ⊢ ( ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝐿 ∈ ℤ )
6 simpll ⊢ ( ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 )
7 simpr ⊢ ( ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝑊 cyclShift 𝐿 ) = 𝑊 )
8 cshwsidrepsw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
9 8 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )
10 4 5 6 7 9 syl13anc ⊢ ( ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )
11 10 olcd ⊢ ( ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
12 11 exp31 ⊢ ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) ≠ 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) ) )
13 2 12 pm2.61ine ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )