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 ⊢W∈WordV∧W∈ℙ∧L∈ℤ→WcyclShiftL=W→LmodW=0∨W=W⁡0repeatSW

Proof

Step Hyp Ref Expression
1 orc ⊢LmodW=0→LmodW=0∨W=W⁡0repeatSW
2 1 2a1d ⊢LmodW=0→W∈WordV∧W∈ℙ∧L∈ℤ→WcyclShiftL=W→LmodW=0∨W=W⁡0repeatSW
3 3simpa ⊢W∈WordV∧W∈ℙ∧L∈ℤ→W∈WordV∧W∈ℙ
4 3 ad2antlr ⊢LmodW≠0∧W∈WordV∧W∈ℙ∧L∈ℤ∧WcyclShiftL=W→W∈WordV∧W∈ℙ
5 simplr3 ⊢LmodW≠0∧W∈WordV∧W∈ℙ∧L∈ℤ∧WcyclShiftL=W→L∈ℤ
6 simpll ⊢LmodW≠0∧W∈WordV∧W∈ℙ∧L∈ℤ∧WcyclShiftL=W→LmodW≠0
7 simpr ⊢LmodW≠0∧W∈WordV∧W∈ℙ∧L∈ℤ∧WcyclShiftL=W→WcyclShiftL=W
8 cshwsidrepsw ⊢W∈WordV∧W∈ℙ→L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W=W⁡0repeatSW
9 8 imp ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W=W⁡0repeatSW
10 4 5 6 7 9 syl13anc ⊢LmodW≠0∧W∈WordV∧W∈ℙ∧L∈ℤ∧WcyclShiftL=W→W=W⁡0repeatSW
11 10 olcd ⊢LmodW≠0∧W∈WordV∧W∈ℙ∧L∈ℤ∧WcyclShiftL=W→LmodW=0∨W=W⁡0repeatSW
12 11 exp31 ⊢LmodW≠0→W∈WordV∧W∈ℙ∧L∈ℤ→WcyclShiftL=W→LmodW=0∨W=W⁡0repeatSW
13 2 12 pm2.61ine ⊢W∈WordV∧W∈ℙ∧L∈ℤ→WcyclShiftL=W→LmodW=0∨W=W⁡0repeatSW