# Metamath Proof Explorer

## Theorem cshwsidrepsw

Description: If cyclically shifting a word of length being a prime number by a number of positions which is not divisible by the prime number results in the word itself, the word is a "repeated symbol word". (Contributed by AV, 18-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to \left|{W}\right|\in ℙ$
2 1 adantr ${⊢}\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 \left|{W}\right|\in ℙ$
3 simp1 ${⊢}\left({L}\in ℤ\wedge {L}\mathrm{mod}\left|{W}\right|\ne 0\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {L}\in ℤ$
4 3 adantl ${⊢}\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 {L}\in ℤ$
5 simpr2 ${⊢}\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 {L}\mathrm{mod}\left|{W}\right|\ne 0$
6 2 4 5 3jca ${⊢}\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 \left(\left|{W}\right|\in ℙ\wedge {L}\in ℤ\wedge {L}\mathrm{mod}\left|{W}\right|\ne 0\right)$
7 6 adantr ${⊢}\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left(\left|{W}\right|\in ℙ\wedge {L}\in ℤ\wedge {L}\mathrm{mod}\left|{W}\right|\ne 0\right)$
8 simpr ${⊢}\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to {i}\in \left(0..^\left|{W}\right|\right)$
9 modprmn0modprm0 ${⊢}\left(\left|{W}\right|\in ℙ\wedge {L}\in ℤ\wedge {L}\mathrm{mod}\left|{W}\right|\ne 0\right)\to \left({i}\in \left(0..^\left|{W}\right|\right)\to \exists {j}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)$
10 7 8 9 sylc ${⊢}\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \exists {j}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0$
11 oveq1 ${⊢}{k}={j}\to {k}{L}={j}{L}$
12 11 oveq2d ${⊢}{k}={j}\to {i}+{k}{L}={i}+{j}{L}$
13 12 fvoveq1d ${⊢}{k}={j}\to {W}\left(\left({i}+{k}{L}\right)\mathrm{mod}\left|{W}\right|\right)={W}\left(\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|\right)$
14 13 eqeq2d ${⊢}{k}={j}\to \left({W}\left({i}\right)={W}\left(\left({i}+{k}{L}\right)\mathrm{mod}\left|{W}\right|\right)↔{W}\left({i}\right)={W}\left(\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|\right)\right)$
15 simpl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to {W}\in \mathrm{Word}{V}$
16 15 3 anim12i ${⊢}\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 \left({W}\in \mathrm{Word}{V}\wedge {L}\in ℤ\right)$
17 16 adantr ${⊢}\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left({W}\in \mathrm{Word}{V}\wedge {L}\in ℤ\right)$
18 17 adantl ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to \left({W}\in \mathrm{Word}{V}\wedge {L}\in ℤ\right)$
19 simpr3 ${⊢}\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}\mathrm{cyclShift}{L}={W}$
20 19 anim1i ${⊢}\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{L}={W}\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)$
21 20 adantl ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to \left({W}\mathrm{cyclShift}{L}={W}\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)$
22 cshweqrep ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {L}\in ℤ\right)\to \left(\left({W}\mathrm{cyclShift}{L}={W}\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(\left({i}+{k}{L}\right)\mathrm{mod}\left|{W}\right|\right)\right)$
23 18 21 22 sylc ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(\left({i}+{k}{L}\right)\mathrm{mod}\left|{W}\right|\right)$
24 elfzonn0 ${⊢}{j}\in \left(0..^\left|{W}\right|\right)\to {j}\in {ℕ}_{0}$
25 24 ad2antrr ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to {j}\in {ℕ}_{0}$
26 14 23 25 rspcdva ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to {W}\left({i}\right)={W}\left(\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|\right)$
27 fveq2 ${⊢}\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\to {W}\left(\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|\right)={W}\left(0\right)$
28 27 adantl ${⊢}\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\to {W}\left(\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|\right)={W}\left(0\right)$
29 28 adantr ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to {W}\left(\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|\right)={W}\left(0\right)$
30 26 29 eqtrd ${⊢}\left(\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\wedge \left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\right)\to {W}\left({i}\right)={W}\left(0\right)$
31 30 ex ${⊢}\left({j}\in \left(0..^\left|{W}\right|\right)\wedge \left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\right)\to \left(\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to {W}\left({i}\right)={W}\left(0\right)\right)$
32 31 rexlimiva ${⊢}\exists {j}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({i}+{j}{L}\right)\mathrm{mod}\left|{W}\right|=0\to \left(\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to {W}\left({i}\right)={W}\left(0\right)\right)$
33 10 32 mpcom ${⊢}\left(\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)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to {W}\left({i}\right)={W}\left(0\right)$
34 33 ralrimiva ${⊢}\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 \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
35 repswsymballbi ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
36 35 ad2antrr ${⊢}\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 \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
37 34 36 mpbird ${⊢}\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|$
38 37 ex ${⊢}\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)$