Metamath Proof Explorer

Theorem cshwlen

Description: The length of a cyclically shifted word is the same as the length of the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 27-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 0csh0 
 |-  ( (/) cyclShift N ) = (/)
2 oveq1 
 |-  ( W = (/) -> ( W cyclShift N ) = ( (/) cyclShift N ) )
3 id 
 |-  ( W = (/) -> W = (/) )
4 1 2 3 3eqtr4a 
 |-  ( W = (/) -> ( W cyclShift N ) = W )
5 4 fveq2d 
 |-  ( W = (/) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
6 5 a1d 
 |-  ( W = (/) -> ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) ) )
7 cshword 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
8 7 fveq2d 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )
9 8 adantr 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ W =/= (/) ) -> ( # ` ( W cyclShift N ) ) = ( # ` ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )
10 swrdcl 
 |-  ( W e. Word V -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V )
11 pfxcl 
 |-  ( W e. Word V -> ( W prefix ( N mod ( # ` W ) ) ) e. Word V )
12 ccatlen 
 |-  ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V /\ ( W prefix ( N mod ( # ` W ) ) ) e. Word V ) -> ( # ` ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) )
13 10 11 12 syl2anc 
 |-  ( W e. Word V -> ( # ` ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) )
14 13 ad2antrr 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ W =/= (/) ) -> ( # ` ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) )
15 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
16 pm3.21 
 |-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( W e. Word V -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) ) )
17 16 ex 
 |-  ( ( # ` W ) e. NN -> ( N e. ZZ -> ( W e. Word V -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) ) ) )
18 15 17 syl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( N e. ZZ -> ( W e. Word V -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) ) ) )
19 18 ex 
 |-  ( W e. Word V -> ( W =/= (/) -> ( N e. ZZ -> ( W e. Word V -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) ) ) ) )
20 19 com24 
 |-  ( W e. Word V -> ( W e. Word V -> ( N e. ZZ -> ( W =/= (/) -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) ) ) ) )
21 20 pm2.43i 
 |-  ( W e. Word V -> ( N e. ZZ -> ( W =/= (/) -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) ) ) )
22 21 imp31 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ W =/= (/) ) -> ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) )
23 simpl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> W e. Word V )
24 zmodfzp1 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
25 24 ancoms 
 |-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
26 25 adantl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
27 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
28 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
29 27 28 sylib 
 |-  ( W e. Word V -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
30 29 adantr 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
31 swrdlen 
 |-  ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( N mod ( # ` W ) ) ) )
32 23 26 30 31 syl3anc 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( N mod ( # ` W ) ) ) )
33 pfxlen 
 |-  ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) = ( N mod ( # ` W ) ) )
34 25 33 sylan2 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) = ( N mod ( # ` W ) ) )
35 32 34 oveq12d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) )
36 27 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
37 zmodcl 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. NN0 )
38 37 nn0cnd 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. CC )
39 38 ancoms 
 |-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( N mod ( # ` W ) ) e. CC )
40 npcan 
 |-  ( ( ( # ` W ) e. CC /\ ( N mod ( # ` W ) ) e. CC ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) )
41 36 39 40 syl2an 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) )
42 35 41 eqtrd 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ N e. ZZ ) ) -> ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( # ` W ) )
43 22 42 syl 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ W =/= (/) ) -> ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( # ` W ) )
44 9 14 43 3eqtrd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ W =/= (/) ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
45 44 expcom 
 |-  ( W =/= (/) -> ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) ) )
46 6 45 pm2.61ine 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )