# Metamath Proof Explorer

## Theorem cshwmodn

Description: Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

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

### Proof

Step Hyp Ref Expression
1 0csh0
|-  ( (/) cyclShift N ) = (/)
2 oveq1
|-  ( W = (/) -> ( W cyclShift N ) = ( (/) cyclShift N ) )
3 oveq1
|-  ( W = (/) -> ( W cyclShift ( N mod ( # ` W ) ) ) = ( (/) cyclShift ( N mod ( # ` W ) ) ) )
4 0csh0
|-  ( (/) cyclShift ( N mod ( # ` W ) ) ) = (/)
5 3 4 eqtrdi
|-  ( W = (/) -> ( W cyclShift ( N mod ( # ` W ) ) ) = (/) )
6 1 2 5 3eqtr4a
|-  ( W = (/) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
7 6 a1d
|-  ( W = (/) -> ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) ) )
8 lennncl
|-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
9 8 ex
|-  ( W e. Word V -> ( W =/= (/) -> ( # ` W ) e. NN ) )
|-  ( ( W e. Word V /\ N e. ZZ ) -> ( W =/= (/) -> ( # ` W ) e. NN ) )
11 10 impcom
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( # ` W ) e. NN )
12 simprr
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> N e. ZZ )
13 zre
|-  ( N e. ZZ -> N e. RR )
14 nnrp
|-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
15 modabs2
|-  ( ( N e. RR /\ ( # ` W ) e. RR+ ) -> ( ( N mod ( # ` W ) ) mod ( # ` W ) ) = ( N mod ( # ` W ) ) )
16 13 14 15 syl2anr
|-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( ( N mod ( # ` W ) ) mod ( # ` W ) ) = ( N mod ( # ` W ) ) )
17 16 opeq1d
|-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> <. ( ( N mod ( # ` W ) ) mod ( # ` W ) ) , ( # ` W ) >. = <. ( N mod ( # ` W ) ) , ( # ` W ) >. )
18 17 oveq2d
|-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( W substr <. ( ( N mod ( # ` W ) ) mod ( # ` W ) ) , ( # ` W ) >. ) = ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) )
19 16 oveq2d
|-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( W prefix ( ( N mod ( # ` W ) ) mod ( # ` W ) ) ) = ( W prefix ( N mod ( # ` W ) ) ) )
20 18 19 oveq12d
|-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( ( W substr <. ( ( N mod ( # ` W ) ) mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( ( N mod ( # ` W ) ) mod ( # ` W ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
21 11 12 20 syl2anc
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( ( W substr <. ( ( N mod ( # ` W ) ) mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( ( N mod ( # ` W ) ) mod ( # ` W ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
22 simprl
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> W e. Word V )
23 12 11 zmodcld
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( N mod ( # ` W ) ) e. NN0 )
24 23 nn0zd
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( N mod ( # ` W ) ) e. ZZ )
25 cshword
|-  ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ZZ ) -> ( W cyclShift ( N mod ( # ` W ) ) ) = ( ( W substr <. ( ( N mod ( # ` W ) ) mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( ( N mod ( # ` W ) ) mod ( # ` W ) ) ) ) )
26 22 24 25 syl2anc
|-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift ( N mod ( # ` W ) ) ) = ( ( W substr <. ( ( N mod ( # ` W ) ) mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( ( N mod ( # ` W ) ) mod ( # ` W ) ) ) ) )
27 cshword
|-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )