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