# Metamath Proof Explorer

## Theorem cshwsublen

Description: Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018)

Ref Expression
Assertion cshwsublen ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}\left|{W}\right|=0\to {N}-\left|{W}\right|={N}-0$
2 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
3 2 subid1d ${⊢}{N}\in ℤ\to {N}-0={N}$
4 3 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {N}-0={N}$
5 1 4 sylan9eq ${⊢}\left(\left|{W}\right|=0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {N}-\left|{W}\right|={N}$
6 5 eqcomd ${⊢}\left(\left|{W}\right|=0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {N}={N}-\left|{W}\right|$
7 6 oveq2d ${⊢}\left(\left|{W}\right|=0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)$
8 7 ex ${⊢}\left|{W}\right|=0\to \left(\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)\right)$
9 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
10 9 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {N}\in ℝ$
11 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
12 elnnne0 ${⊢}\left|{W}\right|\in ℕ↔\left(\left|{W}\right|\in {ℕ}_{0}\wedge \left|{W}\right|\ne 0\right)$
13 nnrp ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in {ℝ}^{+}$
14 12 13 sylbir ${⊢}\left(\left|{W}\right|\in {ℕ}_{0}\wedge \left|{W}\right|\ne 0\right)\to \left|{W}\right|\in {ℝ}^{+}$
15 14 ex ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left(\left|{W}\right|\ne 0\to \left|{W}\right|\in {ℝ}^{+}\right)$
16 11 15 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left(\left|{W}\right|\ne 0\to \left|{W}\right|\in {ℝ}^{+}\right)$
17 16 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to \left(\left|{W}\right|\ne 0\to \left|{W}\right|\in {ℝ}^{+}\right)$
18 17 impcom ${⊢}\left(\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to \left|{W}\right|\in {ℝ}^{+}$
19 modeqmodmin ${⊢}\left({N}\in ℝ\wedge \left|{W}\right|\in {ℝ}^{+}\right)\to {N}\mathrm{mod}\left|{W}\right|=\left({N}-\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|$
20 10 18 19 syl2an2 ${⊢}\left(\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {N}\mathrm{mod}\left|{W}\right|=\left({N}-\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|$
21 20 oveq2d ${⊢}\left(\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}\left({N}\mathrm{mod}\left|{W}\right|\right)={W}\mathrm{cyclShift}\left(\left({N}-\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)$
22 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)$
23 22 adantl ${⊢}\left(\left|{W}\right|\ne 0\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)$
24 simpl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\in \mathrm{Word}{V}$
25 11 nn0zd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℤ$
26 zsubcl ${⊢}\left({N}\in ℤ\wedge \left|{W}\right|\in ℤ\right)\to {N}-\left|{W}\right|\in ℤ$
27 25 26 sylan2 ${⊢}\left({N}\in ℤ\wedge {W}\in \mathrm{Word}{V}\right)\to {N}-\left|{W}\right|\in ℤ$
28 27 ancoms ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {N}-\left|{W}\right|\in ℤ$
29 24 28 jca ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to \left({W}\in \mathrm{Word}{V}\wedge {N}-\left|{W}\right|\in ℤ\right)$
30 29 adantl ${⊢}\left(\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to \left({W}\in \mathrm{Word}{V}\wedge {N}-\left|{W}\right|\in ℤ\right)$
31 cshwmodn ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}-\left|{W}\right|\in ℤ\right)\to {W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)={W}\mathrm{cyclShift}\left(\left({N}-\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)$
32 30 31 syl ${⊢}\left(\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)={W}\mathrm{cyclShift}\left(\left({N}-\left|{W}\right|\right)\mathrm{mod}\left|{W}\right|\right)$
33 21 23 32 3eqtr4d ${⊢}\left(\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)$
34 33 ex ${⊢}\left|{W}\right|\ne 0\to \left(\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)\right)$
35 8 34 pm2.61ine ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({N}-\left|{W}\right|\right)$