Metamath Proof Explorer


Theorem cshwidxm1

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

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

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> W e. Word V )
2 elfzoelz
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> N e. ZZ )
3 2 adantl
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> N e. ZZ )
4 ubmelm1fzo
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( # ` W ) - N ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
5 4 adantl
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - N ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
6 cshwidxmod
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( ( ( # ` W ) - N ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) ) )
7 1 3 5 6 syl3anc
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) ) )
8 elfzoel2
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. ZZ )
9 8 zcnd
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. CC )
10 2 zcnd
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> N e. CC )
11 1cnd
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> 1 e. CC )
12 nnpcan
 |-  ( ( ( # ` W ) e. CC /\ N e. CC /\ 1 e. CC ) -> ( ( ( ( # ` W ) - N ) - 1 ) + N ) = ( ( # ` W ) - 1 ) )
13 9 10 11 12 syl3anc
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( ( # ` W ) - N ) - 1 ) + N ) = ( ( # ` W ) - 1 ) )
14 13 oveq1d
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) = ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) )
15 14 adantl
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) = ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) )
16 elfzo0
 |-  ( N e. ( 0 ..^ ( # ` W ) ) <-> ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) )
17 nnre
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR )
18 peano2rem
 |-  ( ( # ` W ) e. RR -> ( ( # ` W ) - 1 ) e. RR )
19 17 18 syl
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. RR )
20 nnrp
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
21 19 20 jca
 |-  ( ( # ` W ) e. NN -> ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) )
22 21 3ad2ant2
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) )
23 16 22 sylbi
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) )
24 nnm1ge0
 |-  ( ( # ` W ) e. NN -> 0 <_ ( ( # ` W ) - 1 ) )
25 24 3ad2ant2
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 0 <_ ( ( # ` W ) - 1 ) )
26 16 25 sylbi
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> 0 <_ ( ( # ` W ) - 1 ) )
27 zre
 |-  ( ( # ` W ) e. ZZ -> ( # ` W ) e. RR )
28 27 ltm1d
 |-  ( ( # ` W ) e. ZZ -> ( ( # ` W ) - 1 ) < ( # ` W ) )
29 8 28 syl
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) - 1 ) < ( # ` W ) )
30 23 26 29 jca32
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) /\ ( 0 <_ ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
31 30 adantl
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) /\ ( 0 <_ ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
32 modid
 |-  ( ( ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) /\ ( 0 <_ ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
33 31 32 syl
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
34 15 33 eqtrd
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
35 34 fveq2d
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
36 7 35 eqtrd
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )