Metamath Proof Explorer

Theorem cycpmfvlem

Description: Lemma for cycpmfv1 and cycpmfv2 . (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 )
cycpmfvlem.1 
|- ( ph -> N e. ( 0 ..^ ( # ` W ) ) )
Assertion cycpmfvlem 
|- ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) )

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