# Metamath Proof Explorer

## Theorem cshw0

Description: A word cyclically shifted by 0 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 cshw0 ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}0={W}$

### Proof

Step Hyp Ref Expression
1 0csh0 ${⊢}\varnothing \mathrm{cyclShift}0=\varnothing$
2 oveq1 ${⊢}\varnothing ={W}\to \varnothing \mathrm{cyclShift}0={W}\mathrm{cyclShift}0$
3 id ${⊢}\varnothing ={W}\to \varnothing ={W}$
4 1 2 3 3eqtr3a ${⊢}\varnothing ={W}\to {W}\mathrm{cyclShift}0={W}$
5 4 a1d ${⊢}\varnothing ={W}\to \left({W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}0={W}\right)$
6 0z ${⊢}0\in ℤ$
7 cshword ${⊢}\left({W}\in \mathrm{Word}{V}\wedge 0\in ℤ\right)\to {W}\mathrm{cyclShift}0=\left({W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)\right)$
8 6 7 mpan2 ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}0=\left({W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)\right)$
9 8 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to {W}\mathrm{cyclShift}0=\left({W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)\right)$
10 necom ${⊢}\varnothing \ne {W}↔{W}\ne \varnothing$
11 lennncl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\to \left|{W}\right|\in ℕ$
12 nnrp ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in {ℝ}^{+}$
13 0mod ${⊢}\left|{W}\right|\in {ℝ}^{+}\to 0\mathrm{mod}\left|{W}\right|=0$
14 13 opeq1d ${⊢}\left|{W}\right|\in {ℝ}^{+}\to ⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩=⟨0,\left|{W}\right|⟩$
15 14 oveq2d ${⊢}\left|{W}\right|\in {ℝ}^{+}\to {W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩={W}\mathrm{substr}⟨0,\left|{W}\right|⟩$
16 13 oveq2d ${⊢}\left|{W}\right|\in {ℝ}^{+}\to {W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)={W}\mathrm{prefix}0$
17 15 16 oveq12d ${⊢}\left|{W}\right|\in {ℝ}^{+}\to \left({W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)\right)=\left({W}\mathrm{substr}⟨0,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}0\right)$
18 11 12 17 3syl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\to \left({W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)\right)=\left({W}\mathrm{substr}⟨0,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}0\right)$
19 10 18 sylan2b ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to \left({W}\mathrm{substr}⟨0\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}\left(0\mathrm{mod}\left|{W}\right|\right)\right)=\left({W}\mathrm{substr}⟨0,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}0\right)$
20 9 19 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to {W}\mathrm{cyclShift}0=\left({W}\mathrm{substr}⟨0,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}0\right)$
21 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
22 pfxval ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in {ℕ}_{0}\right)\to {W}\mathrm{prefix}\left|{W}\right|={W}\mathrm{substr}⟨0,\left|{W}\right|⟩$
23 21 22 mpdan ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{prefix}\left|{W}\right|={W}\mathrm{substr}⟨0,\left|{W}\right|⟩$
24 pfxid ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{prefix}\left|{W}\right|={W}$
25 23 24 eqtr3d ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{substr}⟨0,\left|{W}\right|⟩={W}$
26 25 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to {W}\mathrm{substr}⟨0,\left|{W}\right|⟩={W}$
27 pfx00 ${⊢}{W}\mathrm{prefix}0=\varnothing$
28 27 a1i ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to {W}\mathrm{prefix}0=\varnothing$
29 26 28 oveq12d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to \left({W}\mathrm{substr}⟨0,\left|{W}\right|⟩\right)\mathrm{++}\left({W}\mathrm{prefix}0\right)={W}\mathrm{++}\varnothing$
30 ccatrid ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{++}\varnothing ={W}$
31 30 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to {W}\mathrm{++}\varnothing ={W}$
32 20 29 31 3eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \varnothing \ne {W}\right)\to {W}\mathrm{cyclShift}0={W}$
33 32 expcom ${⊢}\varnothing \ne {W}\to \left({W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}0={W}\right)$
34 5 33 pm2.61ine ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}0={W}$