# Metamath Proof Explorer

## Theorem cshwsidrepswmod0

Description: If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 (modulo the length of the word) or the word must be a "repeated symbol word". (Contributed by AV, 18-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Assertion cshwsidrepswmod0 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$

### Proof

Step Hyp Ref Expression
1 orc ${⊢}{L}\mathrm{mod}\left|{W}\right|=0\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
2 1 2a1d ${⊢}{L}\mathrm{mod}\left|{W}\right|=0\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)\right)$
3 3simpa ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)$
4 3 ad2antlr ${⊢}\left(\left({L}\mathrm{mod}\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)$
5 simplr3 ${⊢}\left(\left({L}\mathrm{mod}\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {L}\in ℤ$
6 simpll ${⊢}\left(\left({L}\mathrm{mod}\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {L}\mathrm{mod}\left|{W}\right|\ne 0$
7 simpr ${⊢}\left(\left({L}\mathrm{mod}\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {W}\mathrm{cyclShift}{L}={W}$
8 cshwsidrepsw ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to \left(\left({L}\in ℤ\wedge {L}\mathrm{mod}\left|{W}\right|\ne 0\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
9 8 imp ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge \left({L}\in ℤ\wedge {L}\mathrm{mod}\left|{W}\right|\ne 0\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|$
10 4 5 6 7 9 syl13anc ${⊢}\left(\left({L}\mathrm{mod}\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|$
11 10 olcd ${⊢}\left(\left({L}\mathrm{mod}\left|{W}\right|\ne 0\wedge \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
12 11 exp31 ${⊢}{L}\mathrm{mod}\left|{W}\right|\ne 0\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)\right)$
13 2 12 pm2.61ine ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$