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

Proof

Step Hyp Ref Expression
1 simpr ⊢W∈WordV∧W∈ℙ→W∈ℙ
2 1 adantr ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W∈ℙ
3 simp1 ⊢L∈ℤ∧LmodW≠0∧WcyclShiftL=W→L∈ℤ
4 3 adantl ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→L∈ℤ
5 simpr2 ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→LmodW≠0
6 2 4 5 3jca ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W∈ℙ∧L∈ℤ∧LmodW≠0
7 6 adantr ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W∈ℙ∧L∈ℤ∧LmodW≠0
8 simpr ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→i∈0..^W
9 modprmn0modprm0 ⊢W∈ℙ∧L∈ℤ∧LmodW≠0→i∈0..^W→∃j∈0..^Wi+j⁢LmodW=0
10 7 8 9 sylc ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→∃j∈0..^Wi+j⁢LmodW=0
11 oveq1 ⊢k=j→k⁢L=j⁢L
12 11 oveq2d ⊢k=j→i+k⁢L=i+j⁢L
13 12 fvoveq1d ⊢k=j→W⁡i+k⁢LmodW=W⁡i+j⁢LmodW
14 13 eqeq2d ⊢k=j→W⁡i=W⁡i+k⁢LmodW↔W⁡i=W⁡i+j⁢LmodW
15 simpl ⊢W∈WordV∧W∈ℙ→W∈WordV
16 15 3 anim12i ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W∈WordV∧L∈ℤ
17 16 adantr ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W∈WordV∧L∈ℤ
18 17 adantl ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W∈WordV∧L∈ℤ
19 simpr3 ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→WcyclShiftL=W
20 19 anim1i ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→WcyclShiftL=W∧i∈0..^W
21 20 adantl ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→WcyclShiftL=W∧i∈0..^W
22 cshweqrep ⊢W∈WordV∧L∈ℤ→WcyclShiftL=W∧i∈0..^W→∀k∈ℕ0W⁡i=W⁡i+k⁢LmodW
23 18 21 22 sylc ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→∀k∈ℕ0W⁡i=W⁡i+k⁢LmodW
24 elfzonn0 ⊢j∈0..^W→j∈ℕ0
25 24 ad2antrr ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→j∈ℕ0
26 14 23 25 rspcdva ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W⁡i=W⁡i+j⁢LmodW
27 fveq2 ⊢i+j⁢LmodW=0→W⁡i+j⁢LmodW=W⁡0
28 27 adantl ⊢j∈0..^W∧i+j⁢LmodW=0→W⁡i+j⁢LmodW=W⁡0
29 28 adantr ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W⁡i+j⁢LmodW=W⁡0
30 26 29 eqtrd ⊢j∈0..^W∧i+j⁢LmodW=0∧W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W⁡i=W⁡0
31 30 ex ⊢j∈0..^W∧i+j⁢LmodW=0→W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W⁡i=W⁡0
32 31 rexlimiva ⊢∃j∈0..^Wi+j⁢LmodW=0→W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W⁡i=W⁡0
33 10 32 mpcom ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W∧i∈0..^W→W⁡i=W⁡0
34 33 ralrimiva ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→∀i∈0..^WW⁡i=W⁡0
35 repswsymballbi ⊢W∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
36 35 ad2antrr ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
37 34 36 mpbird ⊢W∈WordV∧W∈ℙ∧L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W=W⁡0repeatSW
38 37 ex ⊢W∈WordV∧W∈ℙ→L∈ℤ∧LmodW≠0∧WcyclShiftL=W→W=W⁡0repeatSW