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 φ D V
tocycfv.w φ W Word D
tocycfv.1 φ W : dom W 1-1 D
cycpmfvlem.1 φ N 0 ..^ W
Assertion cycpmfvlem φ C W W N = W cyclShift 1 W -1 W N

Proof

Step Hyp Ref Expression
1 tocycval.1 C = toCyc D
2 tocycfv.d φ D V
3 tocycfv.w φ W Word D
4 tocycfv.1 φ W : dom W 1-1 D
5 cycpmfvlem.1 φ N 0 ..^ W
6 1 2 3 4 tocycfv φ C W = I D ran W W cyclShift 1 W -1
7 6 fveq1d φ C W W N = I D ran W W cyclShift 1 W -1 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 φ I D ran W Fn D ran W
11 1zzd φ 1
12 cshwf W Word D 1 W cyclShift 1 : 0 ..^ W D
13 3 11 12 syl2anc φ W cyclShift 1 : 0 ..^ W D
14 13 ffnd φ W cyclShift 1 Fn 0 ..^ W
15 df-f1 W : dom W 1-1 D W : dom W D Fun W -1
16 4 15 sylib φ W : dom W D Fun W -1
17 16 simprd φ Fun W -1
18 17 funfnd φ W -1 Fn dom W -1
19 df-rn ran W = dom W -1
20 19 fneq2i W -1 Fn ran W W -1 Fn dom W -1
21 18 20 sylibr φ W -1 Fn ran W
22 dfdm4 dom W = ran W -1
23 22 eqimss2i ran W -1 dom W
24 wrdfn W Word D W Fn 0 ..^ W
25 3 24 syl φ W Fn 0 ..^ W
26 25 fndmd φ dom W = 0 ..^ W
27 23 26 sseqtrid φ ran W -1 0 ..^ W
28 fnco W cyclShift 1 Fn 0 ..^ W W -1 Fn ran W ran W -1 0 ..^ W W cyclShift 1 W -1 Fn ran W
29 14 21 27 28 syl3anc φ W cyclShift 1 W -1 Fn ran W
30 disjdifr D ran W ran W =
31 30 a1i φ D ran W ran W =
32 fnfvelrn W Fn 0 ..^ W N 0 ..^ W W N ran W
33 25 5 32 syl2anc φ W N ran W
34 fvun2 I D ran W Fn D ran W W cyclShift 1 W -1 Fn ran W D ran W ran W = W N ran W I D ran W W cyclShift 1 W -1 W N = W cyclShift 1 W -1 W N
35 10 29 31 33 34 syl112anc φ I D ran W W cyclShift 1 W -1 W N = W cyclShift 1 W -1 W N
36 7 35 eqtrd φ C W W N = W cyclShift 1 W -1 W N