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 ) )