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 ) )
10 9 adantr 
 |-  ( ( 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 ) ) ) ) )
28 27 adantl 
 |-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
29 21 26 28 3eqtr4rd 
 |-  ( ( W =/= (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
30 29 ex 
 |-  ( W =/= (/) -> ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) ) )
31 7 30 pm2.61ine 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )