Definition df-tocyc 30768

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 30767	. 2 class toCyc
2		vd	. . 3 setvar 𝑑
3		cvv 3491	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5		vu	. . . . . . . 8 setvar 𝑢
6	5	cv 1535	. . . . . . 7 class 𝑢
7	6	cdm 5548	. . . . . 6 class dom 𝑢
8	2	cv 1535	. . . . . 6 class 𝑑
9	7, 8, 6	wf1 6345	. . . . 5 wff 𝑢:dom 𝑢–1-1→𝑑
10	8	cword 13858	. . . . 5 class Word 𝑑
11	9, 5, 10	crab 3141	. . . 4 class {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑}
12		cid 5452	. . . . . 6 class I
13	4	cv 1535	. . . . . . . 8 class 𝑤
14	13	crn 5549	. . . . . . 7 class ran 𝑤
15	8, 14	cdif 3926	. . . . . 6 class (𝑑 ∖ ran 𝑤)
16	12, 15	cres 5550	. . . . 5 class ( I ↾ (𝑑 ∖ ran 𝑤))
17		c1 10531	. . . . . . 7 class 1
18		ccsh 14143	. . . . . . 7 class cyclShift
19	13, 17, 18	co 7149	. . . . . 6 class (𝑤 cyclShift 1)
20	13	ccnv 5547	. . . . . 6 class ◡𝑤
21	19, 20	ccom 5552	. . . . 5 class ((𝑤 cyclShift 1) ∘ ◡𝑤)
22	16, 21	cun 3927	. . . 4 class (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))
23	4, 11, 22	cmpt 5139	. . 3 class (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))
24	2, 3, 23	cmpt 5139	. 2 class (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))
25	1, 24	wceq 1536	1 wff toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))

This definition is referenced by:  tocycval  30769