Metamath Proof Explorer


Theorem cycpmconjslem1

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

Ref Expression
Hypotheses cycpmconjs.c C = M . -1 P
cycpmconjs.s S = SymGrp D
cycpmconjs.n N = D
cycpmconjs.m M = toCyc D
cycpmconjslem1.d φ D V
cycpmconjslem1.w φ W Word D
cycpmconjslem1.1 φ W : dom W 1-1 D
cycpmconjslem1.2 φ W = P
Assertion cycpmconjslem1 φ W -1 M W W = I 0 ..^ P cyclShift 1

Proof

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