Metamath Proof Explorer


Theorem cycpmfv3

Description: Values outside of the orbit are unchanged by a cycle. (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
cycpmfv3.1 φ X D
cycpmfv3.2 φ ¬ X ran W
Assertion cycpmfv3 φ C W X = X

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 cycpmfv3.1 φ X D
6 cycpmfv3.2 φ ¬ X ran W
7 1 2 3 4 tocycfv φ C W = I D ran W W cyclShift 1 W -1
8 7 fveq1d φ C W X = I D ran W W cyclShift 1 W -1 X
9 f1oi I D ran W : D ran W 1-1 onto D ran W
10 f1ofn I D ran W : D ran W 1-1 onto D ran W I D ran W Fn D ran W
11 9 10 mp1i φ I D ran W Fn D ran W
12 1zzd φ 1
13 cshwf W Word D 1 W cyclShift 1 : 0 ..^ W D
14 3 12 13 syl2anc φ W cyclShift 1 : 0 ..^ W D
15 14 ffnd φ W cyclShift 1 Fn 0 ..^ W
16 df-f1 W : dom W 1-1 D W : dom W D Fun W -1
17 4 16 sylib φ W : dom W D Fun W -1
18 17 simprd φ Fun W -1
19 18 funfnd φ W -1 Fn dom W -1
20 df-rn ran W = dom W -1
21 20 fneq2i W -1 Fn ran W W -1 Fn dom W -1
22 19 21 sylibr φ W -1 Fn ran W
23 dfdm4 dom W = ran W -1
24 23 eqimss2i ran W -1 dom W
25 wrdfn W Word D W Fn 0 ..^ W
26 3 25 syl φ W Fn 0 ..^ W
27 26 fndmd φ dom W = 0 ..^ W
28 24 27 sseqtrid φ ran W -1 0 ..^ W
29 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
30 15 22 28 29 syl3anc φ W cyclShift 1 W -1 Fn ran W
31 disjdifr D ran W ran W =
32 31 a1i φ D ran W ran W =
33 5 6 eldifd φ X D ran W
34 fvun1 I D ran W Fn D ran W W cyclShift 1 W -1 Fn ran W D ran W ran W = X D ran W I D ran W W cyclShift 1 W -1 X = I D ran W X
35 11 30 32 33 34 syl112anc φ I D ran W W cyclShift 1 W -1 X = I D ran W X
36 fvresi X D ran W I D ran W X = X
37 33 36 syl φ I D ran W X = X
38 8 35 37 3eqtrd φ C W X = X