Metamath Proof Explorer

Theorem cycpmfv3

Description: Values outside of the orbit are unchanged by a cycle. (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 )
cycpmfv3.1 
|- ( ph -> X e. D )
cycpmfv3.2 
|- ( ph -> -. X e. ran W )
Assertion cycpmfv3 
|- ( ph -> ( ( C ` W ) ` X ) = X )

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 cycpmfv3.1 
 |-  ( ph -> X e. D )
6 cycpmfv3.2 
 |-  ( ph -> -. X e. ran W )
7 1 2 3 4 tocycfv 
 |-  ( ph -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
8 7 fveq1d 
 |-  ( ph -> ( ( C ` W ) ` X ) = ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ` X ) )
9 f1oi 
 |-  ( _I |` ( D \ ran W ) ) : ( D \ ran W ) -1-1-onto-> ( D \ ran W )
10 f1ofn 
 |-  ( ( _I |` ( D \ ran W ) ) : ( D \ ran W ) -1-1-onto-> ( D \ ran W ) -> ( _I |` ( D \ ran W ) ) Fn ( D \ ran W ) )
11 9 10 mp1i 
 |-  ( ph -> ( _I |` ( D \ ran W ) ) Fn ( D \ ran W ) )
12 1zzd 
 |-  ( ph -> 1 e. ZZ )
13 cshwf 
 |-  ( ( W e. Word D /\ 1 e. ZZ ) -> ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) --> D )
14 3 12 13 syl2anc 
 |-  ( ph -> ( W cyclShift 1 ) : ( 0 ..^ ( # ` W ) ) --> D )
15 14 ffnd 
 |-  ( ph -> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) )
16 df-f1 
 |-  ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) )
17 4 16 sylib 
 |-  ( ph -> ( W : dom W --> D /\ Fun `' W ) )
18 17 simprd 
 |-  ( ph -> Fun `' W )
19 18 funfnd 
 |-  ( ph -> `' W Fn dom `' W )
20 df-rn 
 |-  ran W = dom `' W
21 20 fneq2i 
 |-  ( `' W Fn ran W <-> `' W Fn dom `' W )
22 19 21 sylibr 
 |-  ( ph -> `' W Fn ran W )
23 dfdm4 
 |-  dom W = ran `' W
24 23 eqimss2i 
 |-  ran `' W C_ dom W
25 wrdfn 
 |-  ( W e. Word D -> W Fn ( 0 ..^ ( # ` W ) ) )
26 3 25 syl 
 |-  ( ph -> W Fn ( 0 ..^ ( # ` W ) ) )
27 26 fndmd 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
28 24 27 sseqtrid 
 |-  ( ph -> ran `' W C_ ( 0 ..^ ( # ` W ) ) )
29 fnco 
 |-  ( ( ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) /\ `' W Fn ran W /\ ran `' W C_ ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift 1 ) o. `' W ) Fn ran W )
30 15 22 28 29 syl3anc 
 |-  ( ph -> ( ( W cyclShift 1 ) o. `' W ) Fn ran W )
31 disjdifr 
 |-  ( ( D \ ran W ) i^i ran W ) = (/)
32 31 a1i 
 |-  ( ph -> ( ( D \ ran W ) i^i ran W ) = (/) )
33 5 6 eldifd 
 |-  ( ph -> X e. ( D \ ran W ) )
34 fvun1 
 |-  ( ( ( _I |` ( D \ ran W ) ) Fn ( D \ ran W ) /\ ( ( W cyclShift 1 ) o. `' W ) Fn ran W /\ ( ( ( D \ ran W ) i^i ran W ) = (/) /\ X e. ( D \ ran W ) ) ) -> ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ` X ) = ( ( _I |` ( D \ ran W ) ) ` X ) )
35 11 30 32 33 34 syl112anc 
 |-  ( ph -> ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ` X ) = ( ( _I |` ( D \ ran W ) ) ` X ) )
36 fvresi 
 |-  ( X e. ( D \ ran W ) -> ( ( _I |` ( D \ ran W ) ) ` X ) = X )
37 33 36 syl 
 |-  ( ph -> ( ( _I |` ( D \ ran W ) ) ` X ) = X )
38 8 35 37 3eqtrd 
 |-  ( ph -> ( ( C ` W ) ` X ) = X )