# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)$

### Proof

Step Hyp Ref Expression
1 0csh0 ${⊢}\varnothing \mathrm{cyclShift}{N}=\varnothing$
2 oveq1 ${⊢}{W}=\varnothing \to {W}\mathrm{cyclShift}{N}=\varnothing \mathrm{cyclShift}{N}$
3 oveq1 ${⊢}{W}=\varnothing \to {W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)=\varnothing \mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)$
4 0csh0 ${⊢}\varnothing \mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)=\varnothing$
5 3 4 syl6eq ${⊢}{W}=\varnothing \to {W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)=\varnothing$
6 1 2 5 3eqtr4a ${⊢}{W}=\varnothing \to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)$
7 6 a1d ${⊢}{W}=\varnothing \to \left(\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)\right)$
8 lennncl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\to \left|{W}\right|\in ℕ$
9 8 ex ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}\ne \varnothing \to \left|{W}\right|\in ℕ\right)$
10 9 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to \left({W}\ne \varnothing \to \left|{W}\right|\in ℕ\right)$
11 10 impcom ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to \left|{W}\right|\in ℕ$
12 simprr ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {N}\in ℤ$
13 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
14 nnrp ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in {ℝ}^{+}$
15 modabs2 ${⊢}\left({N}\in ℝ\wedge \left|{W}\right|\in {ℝ}^{+}\right)\to \left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|={N}\mathrm{mod}\left|{W}\right|$
16 13 14 15 syl2anr ${⊢}\left(\left|{W}\right|\in ℕ\wedge {N}\in ℤ\right)\to \left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|={N}\mathrm{mod}\left|{W}\right|$
17 16 opeq1d ${⊢}\left(\left|{W}\right|\in ℕ\wedge {N}\in ℤ\right)\to ⟨\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩=⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩$
18 17 oveq2d ${⊢}\left(\left|{W}\right|\in ℕ\wedge {N}\in ℤ\right)\to {W}\mathrm{substr}⟨\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩={W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩$
19 16 oveq2d ${⊢}\left(\left|{W}\right|\in ℕ\wedge {N}\in ℤ\right)\to {W}\mathrm{prefix}\left(\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)={W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)$
20 18 19 oveq12d ${⊢}\left(\left|{W}\right|\in ℕ\wedge {N}\in ℤ\right)\to \left({W}\mathrm{substr}⟨\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)\right)=\left({W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)\right)$
21 11 12 20 syl2anc ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to \left({W}\mathrm{substr}⟨\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)\right)=\left({W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)\right)$
22 simprl ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\in \mathrm{Word}{V}$
23 12 11 zmodcld ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {N}\mathrm{mod}\left|{W}\right|\in {ℕ}_{0}$
24 23 nn0zd ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {N}\mathrm{mod}\left|{W}\right|\in ℤ$
25 cshword ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\mathrm{mod}\left|{W}\right|\in ℤ\right)\to {W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)=\left({W}\mathrm{substr}⟨\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)\right)$
26 22 24 25 syl2anc ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)=\left({W}\mathrm{substr}⟨\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(\left({N}\mathrm{mod}\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)\right)$
27 cshword ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}=\left({W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)\right)$
28 27 adantl ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}{N}=\left({W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)\right)$
29 21 26 28 3eqtr4rd ${⊢}\left({W}\ne \varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)$
30 29 ex ${⊢}{W}\ne \varnothing \to \left(\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)\right)$
31 7 30 pm2.61ine ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)$