Metamath Proof Explorer

Theorem cshwidxn

Description: The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) 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 cshwidxn 
|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( N - 1 ) ) )

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 elfz1b 
 |-  ( N e. ( 1 ... ( # ` W ) ) <-> ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) )
5 simp2 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( # ` W ) e. NN )
6 4 5 sylbi 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( # ` W ) e. NN )
7 6 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( # ` W ) e. NN )
8 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
9 7 8 syl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
10 cshwidxmod 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( ( ( # ` W ) - 1 ) + N ) mod ( # ` W ) ) ) )
11 1 3 9 10 syl3anc 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( ( ( # ` W ) - 1 ) + N ) mod ( # ` W ) ) ) )
12 nncn 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. CC )
13 12 adantl 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN ) -> ( # ` W ) e. CC )
14 1cnd 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN ) -> 1 e. CC )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 15 adantr 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN ) -> N e. CC )
17 13 14 16 3jca 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN ) -> ( ( # ` W ) e. CC /\ 1 e. CC /\ N e. CC ) )
18 17 3adant3 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( ( # ` W ) e. CC /\ 1 e. CC /\ N e. CC ) )
19 4 18 sylbi 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) e. CC /\ 1 e. CC /\ N e. CC ) )
20 subadd23 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC /\ N e. CC ) -> ( ( ( # ` W ) - 1 ) + N ) = ( ( # ` W ) + ( N - 1 ) ) )
21 19 20 syl 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) + N ) = ( ( # ` W ) + ( N - 1 ) ) )
22 21 oveq1d 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( ( # ` W ) - 1 ) + N ) mod ( # ` W ) ) = ( ( ( # ` W ) + ( N - 1 ) ) mod ( # ` W ) ) )
23 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
24 23 3ad2ant1 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( N - 1 ) e. NN0 )
25 simp3 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> N <_ ( # ` W ) )
26 nnz 
 |-  ( N e. NN -> N e. ZZ )
27 nnz 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. ZZ )
28 26 27 anim12i 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN ) -> ( N e. ZZ /\ ( # ` W ) e. ZZ ) )
29 28 3adant3 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( N e. ZZ /\ ( # ` W ) e. ZZ ) )
30 zlem1lt 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. ZZ ) -> ( N <_ ( # ` W ) <-> ( N - 1 ) < ( # ` W ) ) )
31 29 30 syl 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( N <_ ( # ` W ) <-> ( N - 1 ) < ( # ` W ) ) )
32 25 31 mpbid 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( N - 1 ) < ( # ` W ) )
33 24 5 32 3jca 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( ( N - 1 ) e. NN0 /\ ( # ` W ) e. NN /\ ( N - 1 ) < ( # ` W ) ) )
34 4 33 sylbi 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( N - 1 ) e. NN0 /\ ( # ` W ) e. NN /\ ( N - 1 ) < ( # ` W ) ) )
35 addmodid 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( # ` W ) e. NN /\ ( N - 1 ) < ( # ` W ) ) -> ( ( ( # ` W ) + ( N - 1 ) ) mod ( # ` W ) ) = ( N - 1 ) )
36 34 35 syl 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( # ` W ) + ( N - 1 ) ) mod ( # ` W ) ) = ( N - 1 ) )
37 22 36 eqtrd 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( ( # ` W ) - 1 ) + N ) mod ( # ` W ) ) = ( N - 1 ) )
38 37 fveq2d 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( W ` ( ( ( ( # ` W ) - 1 ) + N ) mod ( # ` W ) ) ) = ( W ` ( N - 1 ) ) )
39 38 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( W ` ( ( ( ( # ` W ) - 1 ) + N ) mod ( # ` W ) ) ) = ( W ` ( N - 1 ) ) )
40 11 39 eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( N - 1 ) ) )