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 = ( d e. _V |-> ( w e. { u e. Word d | u : dom u -1-1-> d } |-> ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctocyc 
 |-  toCyc
1 vd 
 |-  d
2 cvv 
 |-  _V
3 vw 
 |-  w
4 vu 
 |-  u
5 1 cv 
 |-  d
6 5 cword 
 |-  Word d
7 4 cv 
 |-  u
8 7 cdm 
 |-  dom u
9 8 5 7 wf1 
 |-  u : dom u -1-1-> d
10 9 4 6 crab 
 |-  { u e. Word d | u : dom u -1-1-> d }
11 cid 
 |-  _I
12 3 cv 
 |-  w
13 12 crn 
 |-  ran w
14 5 13 cdif 
 |-  ( d \ ran w )
15 11 14 cres 
 |-  ( _I |` ( d \ ran w ) )
16 ccsh 
 |-  cyclShift
17 c1 
 |-  1
18 12 17 16 co 
 |-  ( w cyclShift 1 )
19 12 ccnv 
 |-  `' w
20 18 19 ccom 
 |-  ( ( w cyclShift 1 ) o. `' w )
21 15 20 cun 
 |-  ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) )
22 3 10 21 cmpt 
 |-  ( w e. { u e. Word d | u : dom u -1-1-> d } |-> ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) )
23 1 2 22 cmpt 
 |-  ( d e. _V |-> ( w e. { u e. Word d | u : dom u -1-1-> d } |-> ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )
24 0 23 wceq 
 |-  toCyc = ( d e. _V |-> ( w e. { u e. Word d | u : dom u -1-1-> d } |-> ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )