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 V w u Word d | u : dom u 1-1 d I d ran w w cyclShift 1 w -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctocyc class toCyc
1 vd setvar d
2 cvv class V
3 vw setvar w
4 vu setvar u
5 1 cv setvar d
6 5 cword class Word d
7 4 cv setvar u
8 7 cdm class dom u
9 8 5 7 wf1 wff u : dom u 1-1 d
10 9 4 6 crab class u Word d | u : dom u 1-1 d
11 cid class I
12 3 cv setvar w
13 12 crn class ran w
14 5 13 cdif class d ran w
15 11 14 cres class I d ran w
16 ccsh class cyclShift
17 c1 class 1
18 12 17 16 co class w cyclShift 1
19 12 ccnv class w -1
20 18 19 ccom class w cyclShift 1 w -1
21 15 20 cun class I d ran w w cyclShift 1 w -1
22 3 10 21 cmpt class w u Word d | u : dom u 1-1 d I d ran w w cyclShift 1 w -1
23 1 2 22 cmpt class d V w u Word d | u : dom u 1-1 d I d ran w w cyclShift 1 w -1
24 0 23 wceq wff toCyc = d V w u Word d | u : dom u 1-1 d I d ran w w cyclShift 1 w -1