Metamath Proof Explorer

Theorem cycpmfv2

Description: Value of a cycle function for the last element of the orbit. (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 )
cycpmfv2.1 
|- ( ph -> 0 < ( # ` W ) )
cycpmfv2.2 
|- ( ph -> N = ( ( # ` W ) - 1 ) )
Assertion cycpmfv2 
|- ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( W ` 0 ) )

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 cycpmfv2.1 
 |-  ( ph -> 0 < ( # ` W ) )
6 cycpmfv2.2 
 |-  ( ph -> N = ( ( # ` W ) - 1 ) )
7 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
8 3 7 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
9 elnnnn0b 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ 0 < ( # ` W ) ) )
10 8 5 9 sylanbrc 
 |-  ( ph -> ( # ` W ) e. NN )
11 elfz1end 
 |-  ( ( # ` W ) e. NN <-> ( # ` W ) e. ( 1 ... ( # ` W ) ) )
12 10 11 sylib 
 |-  ( ph -> ( # ` W ) e. ( 1 ... ( # ` W ) ) )
13 fz1fzo0m1 
 |-  ( ( # ` W ) e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
14 12 13 syl 
 |-  ( ph -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
15 6 14 eqeltrd 
 |-  ( ph -> N e. ( 0 ..^ ( # ` W ) ) )
16 1 2 3 4 15 cycpmfvlem 
 |-  ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) )
17 df-f1 
 |-  ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) )
18 4 17 sylib 
 |-  ( ph -> ( W : dom W --> D /\ Fun `' W ) )
19 18 simprd 
 |-  ( ph -> Fun `' W )
20 wrdfn 
 |-  ( W e. Word D -> W Fn ( 0 ..^ ( # ` W ) ) )
21 3 20 syl 
 |-  ( ph -> W Fn ( 0 ..^ ( # ` W ) ) )
22 fnfvelrn 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` N ) e. ran W )
23 21 15 22 syl2anc 
 |-  ( ph -> ( W ` N ) e. ran W )
24 df-rn 
 |-  ran W = dom `' W
25 23 24 eleqtrdi 
 |-  ( ph -> ( W ` N ) e. dom `' W )
26 fvco 
 |-  ( ( Fun `' W /\ ( W ` N ) e. dom `' W ) -> ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) = ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) )
27 19 25 26 syl2anc 
 |-  ( ph -> ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) = ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) )
28 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
29 4 28 syl 
 |-  ( ph -> W : dom W -1-1-onto-> ran W )
30 21 fndmd 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
31 15 30 eleqtrrd 
 |-  ( ph -> N e. dom W )
32 f1ocnvfv1 
 |-  ( ( W : dom W -1-1-onto-> ran W /\ N e. dom W ) -> ( `' W ` ( W ` N ) ) = N )
33 29 31 32 syl2anc 
 |-  ( ph -> ( `' W ` ( W ` N ) ) = N )
34 33 fveq2d 
 |-  ( ph -> ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) = ( ( W cyclShift 1 ) ` N ) )
35 1zzd 
 |-  ( ph -> 1 e. ZZ )
36 cshwidxmod 
 |-  ( ( W e. Word D /\ 1 e. ZZ /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift 1 ) ` N ) = ( W ` ( ( N + 1 ) mod ( # ` W ) ) ) )
37 3 35 15 36 syl3anc 
 |-  ( ph -> ( ( W cyclShift 1 ) ` N ) = ( W ` ( ( N + 1 ) mod ( # ` W ) ) ) )
38 fzossfz 
 |-  ( 0 ..^ ( # ` W ) ) C_ ( 0 ... ( # ` W ) )
39 fzssz 
 |-  ( 0 ... ( # ` W ) ) C_ ZZ
40 38 39 sstri 
 |-  ( 0 ..^ ( # ` W ) ) C_ ZZ
41 40 15 sselid 
 |-  ( ph -> N e. ZZ )
42 41 zred 
 |-  ( ph -> N e. RR )
43 10 nnrpd 
 |-  ( ph -> ( # ` W ) e. RR+ )
44 6 oveq1d 
 |-  ( ph -> ( N mod ( # ` W ) ) = ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) )
45 zmodidfzoimp 
 |-  ( ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
46 14 45 syl 
 |-  ( ph -> ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
47 44 46 eqtrd 
 |-  ( ph -> ( N mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
48 modm1p1mod0 
 |-  ( ( N e. RR /\ ( # ` W ) e. RR+ ) -> ( ( N mod ( # ` W ) ) = ( ( # ` W ) - 1 ) -> ( ( N + 1 ) mod ( # ` W ) ) = 0 ) )
49 48 imp 
 |-  ( ( ( N e. RR /\ ( # ` W ) e. RR+ ) /\ ( N mod ( # ` W ) ) = ( ( # ` W ) - 1 ) ) -> ( ( N + 1 ) mod ( # ` W ) ) = 0 )
50 42 43 47 49 syl21anc 
 |-  ( ph -> ( ( N + 1 ) mod ( # ` W ) ) = 0 )
51 50 fveq2d 
 |-  ( ph -> ( W ` ( ( N + 1 ) mod ( # ` W ) ) ) = ( W ` 0 ) )
52 34 37 51 3eqtrd 
 |-  ( ph -> ( ( W cyclShift 1 ) ` ( `' W ` ( W ` N ) ) ) = ( W ` 0 ) )
53 16 27 52 3eqtrd 
 |-  ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( W ` 0 ) )