Metamath Proof Explorer

Theorem cshco

Description: Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018)

Ref Expression
Assertion cshco 
|- ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( F o. ( W cyclShift N ) ) = ( ( F o. W ) cyclShift N ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 1 3ad2ant3 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> F Fn A )
3 cshwfn 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ( W cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) )
4 3 3adant3 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( W cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) )
5 cshwrn 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ran ( W cyclShift N ) C_ A )
6 5 3adant3 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ran ( W cyclShift N ) C_ A )
7 fnco 
 |-  ( ( F Fn A /\ ( W cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) /\ ran ( W cyclShift N ) C_ A ) -> ( F o. ( W cyclShift N ) ) Fn ( 0 ..^ ( # ` W ) ) )
8 2 4 6 7 syl3anc 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( F o. ( W cyclShift N ) ) Fn ( 0 ..^ ( # ` W ) ) )
9 wrdco 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( F o. W ) e. Word B )
10 9 3adant2 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( F o. W ) e. Word B )
11 simp2 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> N e. ZZ )
12 cshwfn 
 |-  ( ( ( F o. W ) e. Word B /\ N e. ZZ ) -> ( ( F o. W ) cyclShift N ) Fn ( 0 ..^ ( # ` ( F o. W ) ) ) )
13 10 11 12 syl2anc 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( ( F o. W ) cyclShift N ) Fn ( 0 ..^ ( # ` ( F o. W ) ) ) )
14 lenco 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
15 14 3adant2 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
16 15 oveq2d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( 0 ..^ ( # ` ( F o. W ) ) ) = ( 0 ..^ ( # ` W ) ) )
17 16 fneq2d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( ( ( F o. W ) cyclShift N ) Fn ( 0 ..^ ( # ` ( F o. W ) ) ) <-> ( ( F o. W ) cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) ) )
18 13 17 mpbid 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( ( F o. W ) cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) )
19 15 adantr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
20 19 oveq2d 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( i + N ) mod ( # ` ( F o. W ) ) ) = ( ( i + N ) mod ( # ` W ) ) )
21 20 fveq2d 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) = ( W ` ( ( i + N ) mod ( # ` W ) ) ) )
22 21 fveq2d 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( F ` ( W ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) ) = ( F ` ( W ` ( ( i + N ) mod ( # ` W ) ) ) ) )
23 wrdfn 
 |-  ( W e. Word A -> W Fn ( 0 ..^ ( # ` W ) ) )
24 23 3ad2ant1 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> W Fn ( 0 ..^ ( # ` W ) ) )
25 24 adantr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> W Fn ( 0 ..^ ( # ` W ) ) )
26 elfzoelz 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> i e. ZZ )
27 zaddcl 
 |-  ( ( i e. ZZ /\ N e. ZZ ) -> ( i + N ) e. ZZ )
28 26 11 27 syl2anr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( i + N ) e. ZZ )
29 elfzo0 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) <-> ( i e. NN0 /\ ( # ` W ) e. NN /\ i < ( # ` W ) ) )
30 29 simp2bi 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. NN )
31 30 adantl 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. NN )
32 zmodfzo 
 |-  ( ( ( i + N ) e. ZZ /\ ( # ` W ) e. NN ) -> ( ( i + N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
33 28 31 32 syl2anc 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( i + N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
34 15 oveq2d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( ( i + N ) mod ( # ` ( F o. W ) ) ) = ( ( i + N ) mod ( # ` W ) ) )
35 34 eleq1d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( ( ( i + N ) mod ( # ` ( F o. W ) ) ) e. ( 0 ..^ ( # ` W ) ) <-> ( ( i + N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) ) )
36 35 adantr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( i + N ) mod ( # ` ( F o. W ) ) ) e. ( 0 ..^ ( # ` W ) ) <-> ( ( i + N ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) ) )
37 33 36 mpbird 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( i + N ) mod ( # ` ( F o. W ) ) ) e. ( 0 ..^ ( # ` W ) ) )
38 fvco2 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ ( ( i + N ) mod ( # ` ( F o. W ) ) ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) = ( F ` ( W ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) ) )
39 25 37 38 syl2anc 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) = ( F ` ( W ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) ) )
40 simpl1 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> W e. Word A )
41 11 adantr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> N e. ZZ )
42 simpr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
43 cshwidxmod 
 |-  ( ( W e. Word A /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` i ) = ( W ` ( ( i + N ) mod ( # ` W ) ) ) )
44 43 fveq2d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( F ` ( ( W cyclShift N ) ` i ) ) = ( F ` ( W ` ( ( i + N ) mod ( # ` W ) ) ) ) )
45 40 41 42 44 syl3anc 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( F ` ( ( W cyclShift N ) ` i ) ) = ( F ` ( W ` ( ( i + N ) mod ( # ` W ) ) ) ) )
46 22 39 45 3eqtr4rd 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( F ` ( ( W cyclShift N ) ` i ) ) = ( ( F o. W ) ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) )
47 fvco2 
 |-  ( ( ( W cyclShift N ) Fn ( 0 ..^ ( # ` W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. ( W cyclShift N ) ) ` i ) = ( F ` ( ( W cyclShift N ) ` i ) ) )
48 4 47 sylan 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. ( W cyclShift N ) ) ` i ) = ( F ` ( ( W cyclShift N ) ` i ) ) )
49 10 adantr 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( F o. W ) e. Word B )
50 15 eqcomd 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( # ` W ) = ( # ` ( F o. W ) ) )
51 50 oveq2d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( # ` ( F o. W ) ) ) )
52 51 eleq2d 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( # ` ( F o. W ) ) ) ) )
53 52 biimpa 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` ( F o. W ) ) ) )
54 cshwidxmod 
 |-  ( ( ( F o. W ) e. Word B /\ N e. ZZ /\ i e. ( 0 ..^ ( # ` ( F o. W ) ) ) ) -> ( ( ( F o. W ) cyclShift N ) ` i ) = ( ( F o. W ) ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) )
55 49 41 53 54 syl3anc 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( F o. W ) cyclShift N ) ` i ) = ( ( F o. W ) ` ( ( i + N ) mod ( # ` ( F o. W ) ) ) ) )
56 46 48 55 3eqtr4d 
 |-  ( ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. ( W cyclShift N ) ) ` i ) = ( ( ( F o. W ) cyclShift N ) ` i ) )
57 8 18 56 eqfnfvd 
 |-  ( ( W e. Word A /\ N e. ZZ /\ F : A --> B ) -> ( F o. ( W cyclShift N ) ) = ( ( F o. W ) cyclShift N ) )