Metamath Proof Explorer

Theorem cycpmfv1

Description: Value of a cycle function for any element but the last. (Contributed by Thierry Arnoux, 22-Sep-2023)

Ref Expression
Hypotheses tocycval.1 
|- C = ( toCyc ` D )
tocycfv.d 
|- ( ph -> D e. V )
tocycfv.w 
|- ( ph -> W e. Word D )
tocycfv.1 
|- ( ph -> W : dom W -1-1-> D )
cycpmfv1.1 
|- ( ph -> N e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
Assertion cycpmfv1 
|- ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( W ` ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 
 |-  C = ( toCyc ` D )
2 tocycfv.d 
 |-  ( ph -> D e. V )
3 tocycfv.w 
 |-  ( ph -> W e. Word D )
4 tocycfv.1 
 |-  ( ph -> W : dom W -1-1-> D )
5 cycpmfv1.1 
 |-  ( ph -> N e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
6 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
7 3 6 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
8 7 nn0zd 
 |-  ( ph -> ( # ` W ) e. ZZ )
9 fzossrbm1 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( ( # ` W ) - 1 ) ) C_ ( 0 ..^ ( # ` W ) ) )
10 8 9 syl 
 |-  ( ph -> ( 0 ..^ ( ( # ` W ) - 1 ) ) C_ ( 0 ..^ ( # ` W ) ) )
11 10 5 sseldd 
 |-  ( ph -> N e. ( 0 ..^ ( # ` W ) ) )
12 1 2 3 4 11 cycpmfvlem 
 |-  ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) )
13 df-f1 
 |-  ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) )
14 4 13 sylib 
 |-  ( ph -> ( W : dom W --> D /\ Fun `' W ) )
15 14 simprd 
 |-  ( ph -> Fun `' W )
16 wrdfn 
 |-  ( W e. Word D -> W Fn ( 0 ..^ ( # ` W ) ) )
17 3 16 syl 
 |-  ( ph -> W Fn ( 0 ..^ ( # ` W ) ) )
18 fnfvelrn 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` N ) e. ran W )
19 17 11 18 syl2anc 
 |-  ( ph -> ( W ` N ) e. ran W )
20 df-rn 
 |-  ran W = dom `' W
21 19 20 eleqtrdi 
 |-  ( ph -> ( W ` N ) e. dom `' W )
22 fvco 
 |-  ( ( Fun `' W /\ ( W ` N ) e. dom `' W ) -> ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) = ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) )
23 15 21 22 syl2anc 
 |-  ( ph -> ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) = ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) )
24 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
25 4 24 syl 
 |-  ( ph -> W : dom W -1-1-onto-> ran W )
26 17 fndmd 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
27 11 26 eleqtrrd 
 |-  ( ph -> N e. dom W )
28 f1ocnvfv1 
 |-  ( ( W : dom W -1-1-onto-> ran W /\ N e. dom W ) -> ( `' W ` ( W ` N ) ) = N )
29 25 27 28 syl2anc 
 |-  ( ph -> ( `' W ` ( W ` N ) ) = N )
30 29 fveq2d 
 |-  ( ph -> ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) = ( ( W cyclShift 1 ) ` N ) )
31 1zzd 
 |-  ( ph -> 1 e. ZZ )
32 cshwidxmod 
 |-  ( ( W e. Word D /\ 1 e. ZZ /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift 1 ) ` N ) = ( W ` ( ( N + 1 ) mod ( # ` W ) ) ) )
33 3 31 11 32 syl3anc 
 |-  ( ph -> ( ( W cyclShift 1 ) ` N ) = ( W ` ( ( N + 1 ) mod ( # ` W ) ) ) )
34 fzo0ss1 
 |-  ( 1 ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) )
35 fzoaddel2 
 |-  ( ( N e. ( 0 ..^ ( ( # ` W ) - 1 ) ) /\ ( # ` W ) e. ZZ /\ 1 e. ZZ ) -> ( N + 1 ) e. ( 1 ..^ ( # ` W ) ) )
36 5 8 31 35 syl3anc 
 |-  ( ph -> ( N + 1 ) e. ( 1 ..^ ( # ` W ) ) )
37 34 36 sselid 
 |-  ( ph -> ( N + 1 ) e. ( 0 ..^ ( # ` W ) ) )
38 zmodidfzoimp 
 |-  ( ( N + 1 ) e. ( 0 ..^ ( # ` W ) ) -> ( ( N + 1 ) mod ( # ` W ) ) = ( N + 1 ) )
39 37 38 syl 
 |-  ( ph -> ( ( N + 1 ) mod ( # ` W ) ) = ( N + 1 ) )
40 39 fveq2d 
 |-  ( ph -> ( W ` ( ( N + 1 ) mod ( # ` W ) ) ) = ( W ` ( N + 1 ) ) )
41 30 33 40 3eqtrd 
 |-  ( ph -> ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) = ( W ` ( N + 1 ) ) )
42 12 23 41 3eqtrd 
 |-  ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( W ` ( N + 1 ) ) )