Definition df-tocyc 31276

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 31275	. 2 class toCyc
2		vd	. . 3 setvar 𝑑
3		cvv 3422	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5		vu	. . . . . . . 8 setvar 𝑢
6	5	cv 1538	. . . . . . 7 class 𝑢
7	6	cdm 5580	. . . . . 6 class dom 𝑢
8	2	cv 1538	. . . . . 6 class 𝑑
9	7, 8, 6	wf1 6415	. . . . 5 wff 𝑢:dom 𝑢–1-1→𝑑
10	8	cword 14145	. . . . 5 class Word 𝑑
11	9, 5, 10	crab 3067	. . . 4 class {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑}
12		cid 5479	. . . . . 6 class I
13	4	cv 1538	. . . . . . . 8 class 𝑤
14	13	crn 5581	. . . . . . 7 class ran 𝑤
15	8, 14	cdif 3880	. . . . . 6 class (𝑑 ∖ ran 𝑤)
16	12, 15	cres 5582	. . . . 5 class ( I ↾ (𝑑 ∖ ran 𝑤))
17		c1 10803	. . . . . . 7 class 1
18		ccsh 14429	. . . . . . 7 class cyclShift
19	13, 17, 18	co 7255	. . . . . 6 class (𝑤 cyclShift 1)
20	13	ccnv 5579	. . . . . 6 class ◡𝑤
21	19, 20	ccom 5584	. . . . 5 class ((𝑤 cyclShift 1) ∘ ◡𝑤)
22	16, 21	cun 3881	. . . 4 class (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))
23	4, 11, 22	cmpt 5153	. . 3 class (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))
24	2, 3, 23	cmpt 5153	. 2 class (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))
25	1, 24	wceq 1539	1 wff toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))

This definition is referenced by:  tocycval  31277