Metamath Proof Explorer


Theorem cycpmconjslem1

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

Ref Expression
Hypotheses cycpmconjs.c C=M.-1P
cycpmconjs.s S=SymGrpD
cycpmconjs.n N=D
cycpmconjs.m M=toCycD
cycpmconjslem1.d φDV
cycpmconjslem1.w φWWordD
cycpmconjslem1.1 φW:domW1-1D
cycpmconjslem1.2 φW=P
Assertion cycpmconjslem1 φW-1MWW=I0..^PcyclShift1

Proof

Step Hyp Ref Expression
1 cycpmconjs.c C=M.-1P
2 cycpmconjs.s S=SymGrpD
3 cycpmconjs.n N=D
4 cycpmconjs.m M=toCycD
5 cycpmconjslem1.d φDV
6 cycpmconjslem1.w φWWordD
7 cycpmconjslem1.1 φW:domW1-1D
8 cycpmconjslem1.2 φW=P
9 resco W-1MWranW=W-1MWranW
10 9 coeq1i W-1MWranWW=W-1MWranWW
11 ssid ranWranW
12 cores ranWranWW-1MWranWW=W-1MWW
13 11 12 ax-mp W-1MWranWW=W-1MWW
14 coass W-1MWranWW=W-1MWranWW
15 10 13 14 3eqtr3i W-1MWW=W-1MWranWW
16 4 5 6 7 tocycfvres1 φMWranW=WcyclShift1W-1
17 16 coeq1d φMWranWW=WcyclShift1W-1W
18 coass WcyclShift1W-1W=WcyclShift1W-1W
19 f1f1orn W:domW1-1DW:domW1-1 ontoranW
20 f1ococnv1 W:domW1-1 ontoranWW-1W=IdomW
21 7 19 20 3syl φW-1W=IdomW
22 21 coeq2d φWcyclShift1W-1W=WcyclShift1IdomW
23 coires1 WcyclShift1IdomW=WcyclShift1domW
24 22 23 eqtr2di φWcyclShift1domW=WcyclShift1W-1W
25 18 24 eqtr4id φWcyclShift1W-1W=WcyclShift1domW
26 1zzd φ1
27 cshwfn WWordD1WcyclShift1Fn0..^W
28 6 26 27 syl2anc φWcyclShift1Fn0..^W
29 wrddm WWordDdomW=0..^W
30 6 29 syl φdomW=0..^W
31 30 fneq2d φWcyclShift1FndomWWcyclShift1Fn0..^W
32 28 31 mpbird φWcyclShift1FndomW
33 fnresdm WcyclShift1FndomWWcyclShift1domW=WcyclShift1
34 32 33 syl φWcyclShift1domW=WcyclShift1
35 17 25 34 3eqtrd φMWranWW=WcyclShift1
36 35 coeq2d φW-1MWranWW=W-1WcyclShift1
37 15 36 eqtrid φW-1MWW=W-1WcyclShift1
38 wrdfn WWordDWFn0..^W
39 6 38 syl φWFn0..^W
40 df-f W:0..^WranWWFn0..^WranWranW
41 39 11 40 sylanblrc φW:0..^WranW
42 iswrdi W:0..^WranWWWordranW
43 41 42 syl φWWordranW
44 f1ocnv W:domW1-1 ontoranWW-1:ranW1-1 ontodomW
45 7 19 44 3syl φW-1:ranW1-1 ontodomW
46 f1of W-1:ranW1-1 ontodomWW-1:ranWdomW
47 45 46 syl φW-1:ranWdomW
48 cshco WWordranW1W-1:ranWdomWW-1WcyclShift1=W-1WcyclShift1
49 43 26 47 48 syl3anc φW-1WcyclShift1=W-1WcyclShift1
50 8 oveq2d φ0..^W=0..^P
51 30 50 eqtrd φdomW=0..^P
52 51 reseq2d φIdomW=I0..^P
53 21 52 eqtrd φW-1W=I0..^P
54 53 oveq1d φW-1WcyclShift1=I0..^PcyclShift1
55 37 49 54 3eqtrd φW-1MWW=I0..^PcyclShift1