Definition df-tocyc 33127

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.)

Assertion

Ref	Expression
df-tocyc	⊢ toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))

Distinct variable group:   𝑤,𝑑,𝑢

Detailed syntax breakdown of Definition df-tocyc

Step	Hyp	Ref	Expression
1		ctocyc 33126	. 2 class toCyc
2		vd	. . 3 setvar 𝑑
3		cvv 3480	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5		vu	. . . . . . . 8 setvar 𝑢
6	5	cv 1539	. . . . . . 7 class 𝑢
7	6	cdm 5685	. . . . . 6 class dom 𝑢
8	2	cv 1539	. . . . . 6 class 𝑑
9	7, 8, 6	wf1 6558	. . . . 5 wff 𝑢:dom 𝑢–1-1→𝑑
10	8	cword 14552	. . . . 5 class Word 𝑑
11	9, 5, 10	crab 3436	. . . 4 class {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑}
12		cid 5577	. . . . . 6 class I
13	4	cv 1539	. . . . . . . 8 class 𝑤
14	13	crn 5686	. . . . . . 7 class ran 𝑤
15	8, 14	cdif 3948	. . . . . 6 class (𝑑 ∖ ran 𝑤)
16	12, 15	cres 5687	. . . . 5 class ( I ↾ (𝑑 ∖ ran 𝑤))
17		c1 11156	. . . . . . 7 class 1
18		ccsh 14826	. . . . . . 7 class cyclShift
19	13, 17, 18	co 7431	. . . . . 6 class (𝑤 cyclShift 1)
20	13	ccnv 5684	. . . . . 6 class ◡𝑤
21	19, 20	ccom 5689	. . . . 5 class ((𝑤 cyclShift 1) ∘ ◡𝑤)
22	16, 21	cun 3949	. . . 4 class (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))
23	4, 11, 22	cmpt 5225	. . 3 class (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))
24	2, 3, 23	cmpt 5225	. 2 class (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))
25	1, 24	wceq 1540	1 wff toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))

This definition is referenced by:  tocycval  33128