Metamath Proof Explorer


Theorem tocycfvres2

Description: A cyclic permutation is the identity outside of its orbit. (Contributed by Thierry Arnoux, 15-Oct-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
Assertion tocycfvres2 φ C W D ran W = I D ran W

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 1 2 3 4 tocycfv φ C W = I D ran W W cyclShift 1 W -1
6 5 reseq1d φ C W D ran W = I D ran W W cyclShift 1 W -1 D ran W
7 fnresi I D ran W Fn D ran W
8 7 a1i φ I D ran W Fn D ran W
9 1zzd φ 1
10 cshwfn W Word D 1 W cyclShift 1 Fn 0 ..^ W
11 3 9 10 syl2anc φ W cyclShift 1 Fn 0 ..^ W
12 f1f1orn W : dom W 1-1 D W : dom W 1-1 onto ran W
13 f1ocnv W : dom W 1-1 onto ran W W -1 : ran W 1-1 onto dom W
14 f1ofn W -1 : ran W 1-1 onto dom W W -1 Fn ran W
15 4 12 13 14 4syl φ W -1 Fn ran W
16 dfdm4 dom W = ran W -1
17 wrddm W Word D dom W = 0 ..^ W
18 3 17 syl φ dom W = 0 ..^ W
19 ssidd φ 0 ..^ W 0 ..^ W
20 18 19 eqsstrd φ dom W 0 ..^ W
21 16 20 eqsstrrid φ ran W -1 0 ..^ W
22 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
23 11 15 21 22 syl3anc φ W cyclShift 1 W -1 Fn ran W
24 disjdifr D ran W ran W =
25 24 a1i φ D ran W ran W =
26 fnunres1 I D ran W Fn D ran W W cyclShift 1 W -1 Fn ran W D ran W ran W = I D ran W W cyclShift 1 W -1 D ran W = I D ran W
27 8 23 25 26 syl3anc φ I D ran W W cyclShift 1 W -1 D ran W = I D ran W
28 6 27 eqtrd φ C W D ran W = I D ran W