# Metamath Proof Explorer

## Theorem 2cshwid

Description: Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by AV, 1-Nov-2018)

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

### Proof

Step Hyp Ref Expression
1 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
2 1 nn0zd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℤ$
3 zsubcl ${⊢}\left(\left|{W}\right|\in ℤ\wedge {N}\in ℤ\right)\to \left|{W}\right|-{N}\in ℤ$
4 2 3 sylan ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to \left|{W}\right|-{N}\in ℤ$
5 2cshw ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\wedge \left|{W}\right|-{N}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{N}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{N}\right)={W}\mathrm{cyclShift}\left({N}+\left|{W}\right|-{N}\right)$
6 4 5 mpd3an3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{N}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{N}\right)={W}\mathrm{cyclShift}\left({N}+\left|{W}\right|-{N}\right)$
7 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
8 1 nn0cnd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℂ$
9 pncan3 ${⊢}\left({N}\in ℂ\wedge \left|{W}\right|\in ℂ\right)\to {N}+\left|{W}\right|-{N}=\left|{W}\right|$
10 7 8 9 syl2anr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {N}+\left|{W}\right|-{N}=\left|{W}\right|$
11 10 oveq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}\left({N}+\left|{W}\right|-{N}\right)={W}\mathrm{cyclShift}\left|{W}\right|$
12 cshwn ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}$
13 12 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}\left|{W}\right|={W}$
14 6 11 13 3eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{N}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{N}\right)={W}$