# Metamath Proof Explorer

## Theorem cshwn

Description: A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

Ref Expression
Assertion cshwn ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}$

### Proof

Step Hyp Ref Expression
1 0csh0 ${⊢}\varnothing \mathrm{cyclShift}\left|{W}\right|=\varnothing$
2 oveq1 ${⊢}\varnothing ={W}\to \varnothing \mathrm{cyclShift}\left|{W}\right|={W}\mathrm{cyclShift}\left|{W}\right|$
3 id ${⊢}\varnothing ={W}\to \varnothing ={W}$
4 1 2 3 3eqtr3a ${⊢}\varnothing ={W}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}$
5 4 a1d ${⊢}\varnothing ={W}\to \left({W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}\right)$
6 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
7 6 nn0zd ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in ℤ$
8 cshwmodn ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℤ\right)\to {W}\mathrm{cyclShift}\left|{W}\right|={W}\mathrm{cyclShift}\left(\left|{W}\right|\mathrm{mod}\left|{W}\right|\right)$
9 7 8 mpdan ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}\mathrm{cyclShift}\left(\left|{W}\right|\mathrm{mod}\left|{W}\right|\right)$
10 9 adantl ${⊢}\left(\varnothing \ne {W}\wedge {W}\in \mathrm{Word}{V}\right)\to {W}\mathrm{cyclShift}\left|{W}\right|={W}\mathrm{cyclShift}\left(\left|{W}\right|\mathrm{mod}\left|{W}\right|\right)$
11 necom ${⊢}\varnothing \ne {W}↔{W}\ne \varnothing$
12 lennncl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\to \left|{W}\right|\in ℕ$
13 11 12 sylan2b ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to \left|{W}\right|\in ℕ$
14 13 nnrpd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to \left|{W}\right|\in {ℝ}^{+}$
15 14 ancoms ${⊢}\left(\varnothing \ne {W}\wedge {W}\in \mathrm{Word}{V}\right)\to \left|{W}\right|\in {ℝ}^{+}$
16 modid0 ${⊢}\left|{W}\right|\in {ℝ}^{+}\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
17 15 16 syl ${⊢}\left(\varnothing \ne {W}\wedge {W}\in \mathrm{Word}{V}\right)\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
18 17 oveq2d ${⊢}\left(\varnothing \ne {W}\wedge {W}\in \mathrm{Word}{V}\right)\to {W}\mathrm{cyclShift}\left(\left|{W}\right|\mathrm{mod}\left|{W}\right|\right)={W}\mathrm{cyclShift}0$
19 cshw0 ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}0={W}$
20 19 adantl ${⊢}\left(\varnothing \ne {W}\wedge {W}\in \mathrm{Word}{V}\right)\to {W}\mathrm{cyclShift}0={W}$
21 10 18 20 3eqtrd ${⊢}\left(\varnothing \ne {W}\wedge {W}\in \mathrm{Word}{V}\right)\to {W}\mathrm{cyclShift}\left|{W}\right|={W}$
22 21 ex ${⊢}\varnothing \ne {W}\to \left({W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}\right)$
23 5 22 pm2.61ine ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}\left|{W}\right|={W}$