Metamath Proof Explorer


Definition df-tocyc

Description: Define a convenience permutation cycle builder. Given a list of elements to be cycled, in the form of a word, this function produces the corresponding permutation cycle. See definition in Lang p. 30. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Assertion df-tocyc toCyc=dVwuWordd|u:domu1-1dIdranwwcyclShift1w-1

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctocyc classtoCyc
1 vd setvard
2 cvv classV
3 vw setvarw
4 vu setvaru
5 1 cv setvard
6 5 cword classWordd
7 4 cv setvaru
8 7 cdm classdomu
9 8 5 7 wf1 wffu:domu1-1d
10 9 4 6 crab classuWordd|u:domu1-1d
11 cid classI
12 3 cv setvarw
13 12 crn classranw
14 5 13 cdif classdranw
15 11 14 cres classIdranw
16 ccsh classcyclShift
17 c1 class1
18 12 17 16 co classwcyclShift1
19 12 ccnv classw-1
20 18 19 ccom classwcyclShift1w-1
21 15 20 cun classIdranwwcyclShift1w-1
22 3 10 21 cmpt classwuWordd|u:domu1-1dIdranwwcyclShift1w-1
23 1 2 22 cmpt classdVwuWordd|u:domu1-1dIdranwwcyclShift1w-1
24 0 23 wceq wfftoCyc=dVwuWordd|u:domu1-1dIdranwwcyclShift1w-1