This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshwidxm

Description: The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 of the original word. (Contributed by AV, 18-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidxm 
|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> W e. Word V )
2 elfzelz 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> N e. ZZ )
3 2 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> N e. ZZ )
4 ubmelfzo 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) - N ) e. ( 0 ..^ ( # ` W ) ) )
5 4 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( # ` W ) - N ) e. ( 0 ..^ ( # ` W ) ) )
6 cshwidxmod 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( ( # ` W ) - N ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) ) )
7 1 3 5 6 syl3anc 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) ) )
8 elfz1b 
 |-  ( N e. ( 1 ... ( # ` W ) ) <-> ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) )
9 nncn 
 |-  ( N e. NN -> N e. CC )
10 nncn 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. CC )
11 9 10 anim12ci 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN ) -> ( ( # ` W ) e. CC /\ N e. CC ) )
12 11 3adant3 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( ( # ` W ) e. CC /\ N e. CC ) )
13 8 12 sylbi 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) e. CC /\ N e. CC ) )
14 npcan 
 |-  ( ( ( # ` W ) e. CC /\ N e. CC ) -> ( ( ( # ` W ) - N ) + N ) = ( # ` W ) )
15 13 14 syl 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( # ` W ) - N ) + N ) = ( # ` W ) )
16 15 oveq1d 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) = ( ( # ` W ) mod ( # ` W ) ) )
17 16 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) = ( ( # ` W ) mod ( # ` W ) ) )
18 nnrp 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
19 modid0 
 |-  ( ( # ` W ) e. RR+ -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
20 18 19 syl 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
21 20 3ad2ant2 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
22 8 21 sylbi 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
23 22 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
24 17 23 eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) = 0 )
25 24 fveq2d 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( W ` ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) ) = ( W ` 0 ) )
26 7 25 eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` 0 ) )