# Metamath Proof Explorer

## Theorem cshwmodn

Description: Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

Ref Expression
Assertion cshwmodn ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )

### Proof

Step Hyp Ref Expression
1 0csh0 ( ∅ cyclShift 𝑁 ) = ∅
2 oveq1 ( 𝑊 = ∅ → ( 𝑊 cyclShift 𝑁 ) = ( ∅ cyclShift 𝑁 ) )
3 oveq1 ( 𝑊 = ∅ → ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ∅ cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
4 0csh0 ( ∅ cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ∅
5 3 4 eqtrdi ( 𝑊 = ∅ → ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ∅ )
6 1 2 5 3eqtr4a ( 𝑊 = ∅ → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
7 6 a1d ( 𝑊 = ∅ → ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
8 lennncl ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
9 8 ex ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ → ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
10 9 adantr ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 ≠ ∅ → ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
11 10 impcom ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
12 simprr ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
13 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
14 nnrp ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
15 modabs2 ( ( 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) )
16 13 14 15 syl2anr ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) )
17 16 opeq1d ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ⟨ ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ = ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ )
18 17 oveq2d ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑊 substr ⟨ ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) )
19 16 oveq2d ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑊 prefix ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
20 18 19 oveq12d ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 substr ⟨ ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
21 11 12 20 syl2anc ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( ( 𝑊 substr ⟨ ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
22 simprl ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → 𝑊 ∈ Word 𝑉 )
23 12 11 zmodcld ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
24 23 nn0zd ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
25 cshword ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ ) → ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 substr ⟨ ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
26 22 24 25 syl2anc ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 substr ⟨ ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
27 cshword ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
28 27 adantl ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
29 21 26 28 3eqtr4rd ( ( 𝑊 ≠ ∅ ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
30 29 ex ( 𝑊 ≠ ∅ → ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
31 7 30 pm2.61ine ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )