Metamath Proof Explorer

Theorem cycpmconjslem1

Description: Lemma for cycpmconjs . (Contributed by Thierry Arnoux, 14-Oct-2023)

Ref Expression
Hypotheses cycpmconjs.c 
|- C = ( M " ( `' # " { P } ) )
cycpmconjs.s 
|- S = ( SymGrp ` D )
cycpmconjs.n 
|- N = ( # ` D )
cycpmconjs.m 
|- M = ( toCyc ` D )
cycpmconjslem1.d 
|- ( ph -> D e. V )
cycpmconjslem1.w 
|- ( ph -> W e. Word D )
cycpmconjslem1.1 
|- ( ph -> W : dom W -1-1-> D )
cycpmconjslem1.2 
|- ( ph -> ( # ` W ) = P )
Assertion cycpmconjslem1 
|- ( ph -> ( ( `' W o. ( M ` W ) ) o. W ) = ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) )

Proof

Step Hyp Ref Expression
1 cycpmconjs.c 
 |-  C = ( M " ( `' # " { P } ) )
2 cycpmconjs.s 
 |-  S = ( SymGrp ` D )
3 cycpmconjs.n 
 |-  N = ( # ` D )
4 cycpmconjs.m 
 |-  M = ( toCyc ` D )
5 cycpmconjslem1.d 
 |-  ( ph -> D e. V )
6 cycpmconjslem1.w 
 |-  ( ph -> W e. Word D )
7 cycpmconjslem1.1 
 |-  ( ph -> W : dom W -1-1-> D )
8 cycpmconjslem1.2 
 |-  ( ph -> ( # ` W ) = P )
9 resco 
 |-  ( ( `' W o. ( M ` W ) ) |` ran W ) = ( `' W o. ( ( M ` W ) |` ran W ) )
10 9 coeq1i 
 |-  ( ( ( `' W o. ( M ` W ) ) |` ran W ) o. W ) = ( ( `' W o. ( ( M ` W ) |` ran W ) ) o. W )
11 ssid 
 |-  ran W C_ ran W
12 cores 
 |-  ( ran W C_ ran W -> ( ( ( `' W o. ( M ` W ) ) |` ran W ) o. W ) = ( ( `' W o. ( M ` W ) ) o. W ) )
13 11 12 ax-mp 
 |-  ( ( ( `' W o. ( M ` W ) ) |` ran W ) o. W ) = ( ( `' W o. ( M ` W ) ) o. W )
14 coass 
 |-  ( ( `' W o. ( ( M ` W ) |` ran W ) ) o. W ) = ( `' W o. ( ( ( M ` W ) |` ran W ) o. W ) )
15 10 13 14 3eqtr3i 
 |-  ( ( `' W o. ( M ` W ) ) o. W ) = ( `' W o. ( ( ( M ` W ) |` ran W ) o. W ) )
16 4 5 6 7 tocycfvres1 
 |-  ( ph -> ( ( M ` W ) |` ran W ) = ( ( W cyclShift 1 ) o. `' W ) )
17 16 coeq1d 
 |-  ( ph -> ( ( ( M ` W ) |` ran W ) o. W ) = ( ( ( W cyclShift 1 ) o. `' W ) o. W ) )
18 coass 
 |-  ( ( ( W cyclShift 1 ) o. `' W ) o. W ) = ( ( W cyclShift 1 ) o. ( `' W o. W ) )
19 f1f1orn 
 |-  ( W : dom W -1-1-> D -> W : dom W -1-1-onto-> ran W )
20 f1ococnv1 
 |-  ( W : dom W -1-1-onto-> ran W -> ( `' W o. W ) = ( _I |` dom W ) )
21 7 19 20 3syl 
 |-  ( ph -> ( `' W o. W ) = ( _I |` dom W ) )
22 21 coeq2d 
 |-  ( ph -> ( ( W cyclShift 1 ) o. ( `' W o. W ) ) = ( ( W cyclShift 1 ) o. ( _I |` dom W ) ) )
23 coires1 
 |-  ( ( W cyclShift 1 ) o. ( _I |` dom W ) ) = ( ( W cyclShift 1 ) |` dom W )
24 22 23 eqtr2di 
 |-  ( ph -> ( ( W cyclShift 1 ) |` dom W ) = ( ( W cyclShift 1 ) o. ( `' W o. W ) ) )
25 18 24 eqtr4id 
 |-  ( ph -> ( ( ( W cyclShift 1 ) o. `' W ) o. W ) = ( ( W cyclShift 1 ) |` dom W ) )
26 1zzd 
 |-  ( ph -> 1 e. ZZ )
27 cshwfn 
 |-  ( ( W e. Word D /\ 1 e. ZZ ) -> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) )
28 6 26 27 syl2anc 
 |-  ( ph -> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) )
29 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
30 6 29 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
31 30 fneq2d 
 |-  ( ph -> ( ( W cyclShift 1 ) Fn dom W <-> ( W cyclShift 1 ) Fn ( 0 ..^ ( # ` W ) ) ) )
32 28 31 mpbird 
 |-  ( ph -> ( W cyclShift 1 ) Fn dom W )
33 fnresdm 
 |-  ( ( W cyclShift 1 ) Fn dom W -> ( ( W cyclShift 1 ) |` dom W ) = ( W cyclShift 1 ) )
34 32 33 syl 
 |-  ( ph -> ( ( W cyclShift 1 ) |` dom W ) = ( W cyclShift 1 ) )
35 17 25 34 3eqtrd 
 |-  ( ph -> ( ( ( M ` W ) |` ran W ) o. W ) = ( W cyclShift 1 ) )
36 35 coeq2d 
 |-  ( ph -> ( `' W o. ( ( ( M ` W ) |` ran W ) o. W ) ) = ( `' W o. ( W cyclShift 1 ) ) )
37 15 36 eqtrid 
 |-  ( ph -> ( ( `' W o. ( M ` W ) ) o. W ) = ( `' W o. ( W cyclShift 1 ) ) )
38 wrdfn 
 |-  ( W e. Word D -> W Fn ( 0 ..^ ( # ` W ) ) )
39 6 38 syl 
 |-  ( ph -> W Fn ( 0 ..^ ( # ` W ) ) )
40 df-f 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> ran W <-> ( W Fn ( 0 ..^ ( # ` W ) ) /\ ran W C_ ran W ) )
41 39 11 40 sylanblrc 
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> ran W )
42 iswrdi 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> ran W -> W e. Word ran W )
43 41 42 syl 
 |-  ( ph -> W e. Word ran W )
44 f1ocnv 
 |-  ( W : dom W -1-1-onto-> ran W -> `' W : ran W -1-1-onto-> dom W )
45 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
46 7 19 44 45 4syl 
 |-  ( ph -> `' W : ran W --> dom W )
47 cshco 
 |-  ( ( W e. Word ran W /\ 1 e. ZZ /\ `' W : ran W --> dom W ) -> ( `' W o. ( W cyclShift 1 ) ) = ( ( `' W o. W ) cyclShift 1 ) )
48 43 26 46 47 syl3anc 
 |-  ( ph -> ( `' W o. ( W cyclShift 1 ) ) = ( ( `' W o. W ) cyclShift 1 ) )
49 8 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ P ) )
50 30 49 eqtrd 
 |-  ( ph -> dom W = ( 0 ..^ P ) )
51 50 reseq2d 
 |-  ( ph -> ( _I |` dom W ) = ( _I |` ( 0 ..^ P ) ) )
52 21 51 eqtrd 
 |-  ( ph -> ( `' W o. W ) = ( _I |` ( 0 ..^ P ) ) )
53 52 oveq1d 
 |-  ( ph -> ( ( `' W o. W ) cyclShift 1 ) = ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) )
54 37 48 53 3eqtrd 
 |-  ( ph -> ( ( `' W o. ( M ` W ) ) o. W ) = ( ( _I |` ( 0 ..^ P ) ) cyclShift 1 ) )