Metamath Proof Explorer

Theorem tocycfvres2

Description: A cyclic permutation is the identity outside of its orbit. (Contributed by Thierry Arnoux, 15-Oct-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 )
Assertion tocycfvres2 
|- ( ph -> ( ( C ` W ) |` ( D \ ran W ) ) = ( _I |` ( D \ ran W ) ) )

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 1 2 3 4 tocycfv 
 |-  ( ph -> ( C ` W ) = ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) )
6 5 reseq1d 
 |-  ( ph -> ( ( C ` W ) |` ( D \ ran W ) ) = ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) |` ( D \ ran W ) ) )
7 fnresi 
 |-  ( _I |` ( D \ ran W ) ) Fn ( D \ ran W )
8 7 a1i 
 |-  ( ph -> ( _I |` ( D \ ran W ) ) Fn ( D \ ran W ) )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 cshwfn 
 |-  ( ( W e. Word D /\ 1 e. ZZ ) -> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) )
11 3 9 10 syl2anc 
 |-  ( ph -> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) )
12 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
13 f1ocnv 
 |-  ( W : dom W -1-1-onto-> ran W -> `' W : ran W -1-1-onto-> dom W )
14 f1ofn 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W Fn ran W )
15 4 12 13 14 4syl 
 |-  ( ph -> `' W Fn ran W )
16 dfdm4 
 |-  dom W = ran `' W
17 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
18 3 17 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
19 ssidd 
 |-  ( ph -> ( 0 ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) )
20 18 19 eqsstrd 
 |-  ( ph -> dom W C_ ( 0 ..^ ( # ` W ) ) )
21 16 20 eqsstrrid 
 |-  ( ph -> ran `' W C_ ( 0 ..^ ( # ` W ) ) )
22 fnco 
 |-  ( ( ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) /\ `' W Fn ran W /\ ran `' W C_ ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift 1 ) o. `' W ) Fn ran W )
23 11 15 21 22 syl3anc 
 |-  ( ph -> ( ( W cyclShift 1 ) o. `' W ) Fn ran W )
24 disjdifr 
 |-  ( ( D \ ran W ) i^i ran W ) = (/)
25 24 a1i 
 |-  ( ph -> ( ( D \ ran W ) i^i ran W ) = (/) )
26 fnunres1 
 |-  ( ( ( _I |` ( D \ ran W ) ) Fn ( D \ ran W ) /\ ( ( W cyclShift 1 ) o. `' W ) Fn ran W /\ ( ( D \ ran W ) i^i ran W ) = (/) ) -> ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) |` ( D \ ran W ) ) = ( _I |` ( D \ ran W ) ) )
27 8 23 25 26 syl3anc 
 |-  ( ph -> ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) |` ( D \ ran W ) ) = ( _I |` ( D \ ran W ) ) )
28 6 27 eqtrd 
 |-  ( ph -> ( ( C ` W ) |` ( D \ ran W ) ) = ( _I |` ( D \ ran W ) ) )