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 = ( 𝑑 ∈ V ↦ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctocyc	⊢ toCyc
1		vd	⊢ 𝑑
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		vu	⊢ 𝑢
5	1	cv	⊢ 𝑑
6	5	cword	⊢ Word 𝑑
7	4	cv	⊢ 𝑢
8	7	cdm	⊢ dom 𝑢
9	8 5 7	wf1	⊢ 𝑢 : dom 𝑢 –1-1→ 𝑑
10	9 4 6	crab	⊢ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 }
11		cid	⊢ I
12	3	cv	⊢ 𝑤
13	12	crn	⊢ ran 𝑤
14	5 13	cdif	⊢ ( 𝑑 ∖ ran 𝑤 )
15	11 14	cres	⊢ ( I ↾ ( 𝑑 ∖ ran 𝑤 ) )
16		ccsh	⊢ cyclShift
17		c1	⊢ 1
18	12 17 16	co	⊢ ( 𝑤 cyclShift 1 )
19	12	ccnv	⊢ ◡ 𝑤
20	18 19	ccom	⊢ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 )
21	15 20	cun	⊢ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) )
22	3 10 21	cmpt	⊢ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) )
23	1 2 22	cmpt	⊢ ( 𝑑 ∈ V ↦ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )
24	0 23	wceq	⊢ toCyc = ( 𝑑 ∈ V ↦ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )