# Metamath Proof Explorer

## Theorem cshwn

Description: A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

Ref Expression
Assertion cshwn ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )

### Proof

Step Hyp Ref Expression
1 0csh0 ( ∅ cyclShift ( ♯ ‘ 𝑊 ) ) = ∅
2 oveq1 ( ∅ = 𝑊 → ( ∅ cyclShift ( ♯ ‘ 𝑊 ) ) = ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) )
3 id ( ∅ = 𝑊 → ∅ = 𝑊 )
4 1 2 3 3eqtr3a ( ∅ = 𝑊 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
5 4 a1d ( ∅ = 𝑊 → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 ) )
6 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7 6 nn0zd ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
8 cshwmodn ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = ( 𝑊 cyclShift ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) ) )
9 7 8 mpdan ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = ( 𝑊 cyclShift ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) ) )
10 9 adantl ( ( ∅ ≠ 𝑊𝑊 ∈ Word 𝑉 ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = ( 𝑊 cyclShift ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) ) )
11 necom ( ∅ ≠ 𝑊𝑊 ≠ ∅ )
12 lennncl ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
13 11 12 sylan2b ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
14 13 nnrpd ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
15 14 ancoms ( ( ∅ ≠ 𝑊𝑊 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
16 modid0 ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
17 15 16 syl ( ( ∅ ≠ 𝑊𝑊 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
18 17 oveq2d ( ( ∅ ≠ 𝑊𝑊 ∈ Word 𝑉 ) → ( 𝑊 cyclShift ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 cyclShift 0 ) )
19 cshw0 ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 )
20 19 adantl ( ( ∅ ≠ 𝑊𝑊 ∈ Word 𝑉 ) → ( 𝑊 cyclShift 0 ) = 𝑊 )
21 10 18 20 3eqtrd ( ( ∅ ≠ 𝑊𝑊 ∈ Word 𝑉 ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
22 21 ex ( ∅ ≠ 𝑊 → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 ) )
23 5 22 pm2.61ine ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )