Metamath Proof Explorer

Theorem cshwrnid

Description: Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Assertion cshwrnid 
|- ( ( W e. Word V /\ N e. ZZ ) -> ran ( W cyclShift N ) = ran W )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> i e. ZZ )
2 1 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ZZ )
3 simp2 
 |-  ( ( W e. Word V /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> N e. ZZ )
4 2 3 zsubcld 
 |-  ( ( W e. Word V /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( i - N ) e. ZZ )
5 elfzo0 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) <-> ( i e. NN0 /\ ( # ` W ) e. NN /\ i < ( # ` W ) ) )
6 5 simp2bi 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. NN )
7 6 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. NN )
8 zmodfzo 
 |-  ( ( ( i - N ) e. ZZ /\ ( # ` W ) e. NN ) -> ( ( i - N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
9 4 7 8 syl2anc 
 |-  ( ( W e. Word V /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( i - N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
10 9 3expa 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( i - N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
11 elfzoelz 
 |-  ( j e. ( 0 ..^ ( # ` W ) ) -> j e. ZZ )
12 11 adantl 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> j e. ZZ )
13 simplr 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> N e. ZZ )
14 12 13 zaddcld 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( j + N ) e. ZZ )
15 elfzo0 
 |-  ( j e. ( 0 ..^ ( # ` W ) ) <-> ( j e. NN0 /\ ( # ` W ) e. NN /\ j < ( # ` W ) ) )
16 15 simp2bi 
 |-  ( j e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. NN )
17 16 adantl 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. NN )
18 zmodfzo 
 |-  ( ( ( j + N ) e. ZZ /\ ( # ` W ) e. NN ) -> ( ( j + N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
19 14 17 18 syl2anc 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( ( j + N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
20 simpr 
 |-  ( ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) /\ i = ( ( j + N ) mod ( # ` W ) ) ) -> i = ( ( j + N ) mod ( # ` W ) ) )
21 20 oveq1d 
 |-  ( ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) /\ i = ( ( j + N ) mod ( # ` W ) ) ) -> ( i - N ) = ( ( ( j + N ) mod ( # ` W ) ) - N ) )
22 21 oveq1d 
 |-  ( ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) /\ i = ( ( j + N ) mod ( # ` W ) ) ) -> ( ( i - N ) mod ( # ` W ) ) = ( ( ( ( j + N ) mod ( # ` W ) ) - N ) mod ( # ` W ) ) )
23 22 eqeq2d 
 |-  ( ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) /\ i = ( ( j + N ) mod ( # ` W ) ) ) -> ( j = ( ( i - N ) mod ( # ` W ) ) <-> j = ( ( ( ( j + N ) mod ( # ` W ) ) - N ) mod ( # ` W ) ) ) )
24 12 zred 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> j e. RR )
25 13 zred 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> N e. RR )
26 24 25 readdcld 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( j + N ) e. RR )
27 17 nnrpd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. RR+ )
28 modsubmod 
 |-  ( ( ( j + N ) e. RR /\ N e. RR /\ ( # ` W ) e. RR+ ) -> ( ( ( ( j + N ) mod ( # ` W ) ) - N ) mod ( # ` W ) ) = ( ( ( j + N ) - N ) mod ( # ` W ) ) )
29 26 25 27 28 syl3anc 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( j + N ) mod ( # ` W ) ) - N ) mod ( # ` W ) ) = ( ( ( j + N ) - N ) mod ( # ` W ) ) )
30 12 zcnd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> j e. CC )
31 13 zcnd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> N e. CC )
32 30 31 pncand 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( ( j + N ) - N ) = j )
33 32 oveq1d 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( j + N ) - N ) mod ( # ` W ) ) = ( j mod ( # ` W ) ) )
34 zmodidfzoimp 
 |-  ( j e. ( 0 ..^ ( # ` W ) ) -> ( j mod ( # ` W ) ) = j )
35 34 adantl 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( j mod ( # ` W ) ) = j )
36 29 33 35 3eqtrrd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> j = ( ( ( ( j + N ) mod ( # ` W ) ) - N ) mod ( # ` W ) ) )
37 19 23 36 rspcedvd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ j e. ( 0 ..^ ( # ` W ) ) ) -> E. i e. ( 0 ..^ ( # ` W ) ) j = ( ( i - N ) mod ( # ` W ) ) )
38 simp3 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> j = ( ( i - N ) mod ( # ` W ) ) )
39 38 fveq2d 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> ( ( W cyclShift N ) ` j ) = ( ( W cyclShift N ) ` ( ( i - N ) mod ( # ` W ) ) ) )
40 simp1l 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> W e. Word V )
41 simp1r 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> N e. ZZ )
42 simp2 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
43 cshwidxmodr 
 |-  ( ( W e. Word V /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( i - N ) mod ( # ` W ) ) ) = ( W ` i ) )
44 40 41 42 43 syl3anc 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( i - N ) mod ( # ` W ) ) ) = ( W ` i ) )
45 39 44 eqtrd 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> ( ( W cyclShift N ) ` j ) = ( W ` i ) )
46 45 eqeq2d 
 |-  ( ( ( W e. Word V /\ N e. ZZ ) /\ i e. ( 0 ..^ ( # ` W ) ) /\ j = ( ( i - N ) mod ( # ` W ) ) ) -> ( c = ( ( W cyclShift N ) ` j ) <-> c = ( W ` i ) ) )
47 10 37 46 rexxfrd2 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( E. j e. ( 0 ..^ ( # ` W ) ) c = ( ( W cyclShift N ) ` j ) <-> E. i e. ( 0 ..^ ( # ` W ) ) c = ( W ` i ) ) )
48 47 abbidv 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> { c | E. j e. ( 0 ..^ ( # ` W ) ) c = ( ( W cyclShift N ) ` j ) } = { c | E. i e. ( 0 ..^ ( # ` W ) ) c = ( W ` i ) } )
49 cshwfn 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) )
50 fnrnfv 
 |-  ( ( W cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) -> ran ( W cyclShift N ) = { c | E. j e. ( 0 ..^ ( # ` W ) ) c = ( ( W cyclShift N ) ` j ) } )
51 49 50 syl 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ran ( W cyclShift N ) = { c | E. j e. ( 0 ..^ ( # ` W ) ) c = ( ( W cyclShift N ) ` j ) } )
52 wrdfn 
 |-  ( W e. Word V -> W Fn ( 0 ..^ ( # ` W ) ) )
53 52 adantr 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> W Fn ( 0 ..^ ( # ` W ) ) )
54 fnrnfv 
 |-  ( W Fn ( 0 ..^ ( # ` W ) ) -> ran W = { c | E. i e. ( 0 ..^ ( # ` W ) ) c = ( W ` i ) } )
55 53 54 syl 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ran W = { c | E. i e. ( 0 ..^ ( # ` W ) ) c = ( W ` i ) } )
56 48 51 55 3eqtr4d 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ran ( W cyclShift N ) = ran W )