Metamath Proof Explorer


Theorem cshwidxmodr

Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021)

Ref Expression
Assertion cshwidxmodr
|- ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( I - N ) mod ( # ` W ) ) ) = ( W ` I ) )

Proof

Step Hyp Ref Expression
1 elfzo0
 |-  ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) )
2 nn0z
 |-  ( I e. NN0 -> I e. ZZ )
3 2 3ad2ant1
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) -> I e. ZZ )
4 zsubcl
 |-  ( ( I e. ZZ /\ N e. ZZ ) -> ( I - N ) e. ZZ )
5 3 4 sylan
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) /\ N e. ZZ ) -> ( I - N ) e. ZZ )
6 simpl2
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) /\ N e. ZZ ) -> ( # ` W ) e. NN )
7 5 6 jca
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) /\ N e. ZZ ) -> ( ( I - N ) e. ZZ /\ ( # ` W ) e. NN ) )
8 7 ex
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) -> ( N e. ZZ -> ( ( I - N ) e. ZZ /\ ( # ` W ) e. NN ) ) )
9 1 8 sylbi
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( N e. ZZ -> ( ( I - N ) e. ZZ /\ ( # ` W ) e. NN ) ) )
10 9 impcom
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I - N ) e. ZZ /\ ( # ` W ) e. NN ) )
11 10 3adant1
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I - N ) e. ZZ /\ ( # ` W ) e. NN ) )
12 zmodfzo
 |-  ( ( ( I - N ) e. ZZ /\ ( # ` W ) e. NN ) -> ( ( I - N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
13 11 12 syl
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I - N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
14 cshwidxmod
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( ( I - N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( I - N ) mod ( # ` W ) ) ) = ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) )
15 13 14 syld3an3
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( I - N ) mod ( # ` W ) ) ) = ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) )
16 elfzoelz
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. ZZ )
17 16 adantl
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I e. ZZ )
18 17 4 sylan
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( I - N ) e. ZZ )
19 18 zred
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( I - N ) e. RR )
20 zre
 |-  ( N e. ZZ -> N e. RR )
21 20 adantl
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> N e. RR )
22 nnrp
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
23 22 ad3antlr
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( # ` W ) e. RR+ )
24 modaddmod
 |-  ( ( ( I - N ) e. RR /\ N e. RR /\ ( # ` W ) e. RR+ ) -> ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) = ( ( ( I - N ) + N ) mod ( # ` W ) ) )
25 19 21 23 24 syl3anc
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) = ( ( ( I - N ) + N ) mod ( # ` W ) ) )
26 nn0cn
 |-  ( I e. NN0 -> I e. CC )
27 26 ad2antrr
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I e. CC )
28 zcn
 |-  ( N e. ZZ -> N e. CC )
29 npcan
 |-  ( ( I e. CC /\ N e. CC ) -> ( ( I - N ) + N ) = I )
30 27 28 29 syl2an
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( ( I - N ) + N ) = I )
31 30 oveq1d
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( ( ( I - N ) + N ) mod ( # ` W ) ) = ( I mod ( # ` W ) ) )
32 zmodidfzoimp
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( I mod ( # ` W ) ) = I )
33 32 ad2antlr
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( I mod ( # ` W ) ) = I )
34 25 31 33 3eqtrd
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) = I )
35 34 fveq2d
 |-  ( ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) /\ N e. ZZ ) -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) )
36 35 ex
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( N e. ZZ -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) ) )
37 36 ex
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN ) -> ( I e. ( 0 ..^ ( # ` W ) ) -> ( N e. ZZ -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) ) ) )
38 37 3adant3
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) -> ( I e. ( 0 ..^ ( # ` W ) ) -> ( N e. ZZ -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) ) ) )
39 1 38 sylbi
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( I e. ( 0 ..^ ( # ` W ) ) -> ( N e. ZZ -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) ) ) )
40 39 pm2.43i
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( N e. ZZ -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) ) )
41 40 impcom
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) )
42 41 3adant1
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( ( I - N ) mod ( # ` W ) ) + N ) mod ( # ` W ) ) ) = ( W ` I ) )
43 15 42 eqtrd
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( I - N ) mod ( # ` W ) ) ) = ( W ` I ) )