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 incom 
 |-  ( ran W i^i ( D \ ran W ) ) = ( ( D \ ran W ) i^i ran W )
31 disjdif 
 |-  ( ran W i^i ( D \ ran W ) ) = (/)
32 30 31 eqtr3i 
 |-  ( ( D \ ran W ) i^i ran W ) = (/)
33 32 a1i 
 |-  ( ph -> ( ( D \ ran W ) i^i ran W ) = (/) )
34 fnfvelrn 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` N ) e. ran W )
35 25 5 34 syl2anc 
 |-  ( ph -> ( W ` N ) e. ran W )
36 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 ) ) )
37 10 29 33 35 36 syl112anc 
 |-  ( ph -> ( ( ( _I |` ( D \ ran W ) ) u. ( ( W cyclShift 1 ) o. `' W ) ) ` ( W ` N ) ) = ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) )
38 7 37 eqtrd 
 |-  ( ph -> ( ( C ` W ) ` ( W ` N ) ) = ( ( ( W cyclShift 1 ) o. `' W ) ` ( W ` N ) ) )