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