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 ( ♯ ‘ 𝑊 ) ) = 𝑊 )