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 e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( # ` W ) e. Prime )
2 1 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( # ` W ) e. Prime )
3 simp1 
 |-  ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> L e. ZZ )
4 3 adantl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> L e. ZZ )
5 simpr2 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( L mod ( # ` W ) ) =/= 0 )
6 2 4 5 3jca 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( ( # ` W ) e. Prime /\ L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 ) )
7 6 adantr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) e. Prime /\ L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 ) )
8 simpr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
9 modprmn0modprm0 
 |-  ( ( ( # ` W ) e. Prime /\ L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 ) -> ( i e. ( 0 ..^ ( # ` W ) ) -> E. j e. ( 0 ..^ ( # ` W ) ) ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) )
10 7 8 9 sylc 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> E. j e. ( 0 ..^ ( # ` W ) ) ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 )
11 oveq1 
 |-  ( k = j -> ( k x. L ) = ( j x. L ) )
12 11 oveq2d 
 |-  ( k = j -> ( i + ( k x. L ) ) = ( i + ( j x. L ) ) )
13 12 fvoveq1d 
 |-  ( k = j -> ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) )
14 13 eqeq2d 
 |-  ( k = j -> ( ( W ` i ) = ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) <-> ( W ` i ) = ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) ) )
15 simpl 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> W e. Word V )
16 15 3 anim12i 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( W e. Word V /\ L e. ZZ ) )
17 16 adantr 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W e. Word V /\ L e. ZZ ) )
18 17 adantl 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W e. Word V /\ L e. ZZ ) )
19 simpr3 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( W cyclShift L ) = W )
20 19 anim1i 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift L ) = W /\ i e. ( 0 ..^ ( # ` W ) ) ) )
21 20 adantl 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( W cyclShift L ) = W /\ i e. ( 0 ..^ ( # ` W ) ) ) )
22 cshweqrep 
 |-  ( ( W e. Word V /\ L e. ZZ ) -> ( ( ( W cyclShift L ) = W /\ i e. ( 0 ..^ ( # ` W ) ) ) -> A. k e. NN0 ( W ` i ) = ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) ) )
23 18 21 22 sylc 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> A. k e. NN0 ( W ` i ) = ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) )
24 elfzonn0 
 |-  ( j e. ( 0 ..^ ( # ` W ) ) -> j e. NN0 )
25 24 ad2antrr 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> j e. NN0 )
26 14 23 25 rspcdva 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` i ) = ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) )
27 fveq2 
 |-  ( ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 -> ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )
28 27 adantl 
 |-  ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) -> ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )
29 28 adantr 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )
30 26 29 eqtrd 
 |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` i ) = ( W ` 0 ) )
31 30 ex 
 |-  ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) -> ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) ) )
32 31 rexlimiva 
 |-  ( E. j e. ( 0 ..^ ( # ` W ) ) ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 -> ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) ) )
33 10 32 mpcom 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) )
34 33 ralrimiva 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
35 repswsymballbi 
 |-  ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
36 35 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
37 34 36 mpbird 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) )
38 37 ex 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )