Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tocyc Structured version   Visualization version   GIF version

Definition df-tocyc 30912
 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
StepHypRef Expression
1 ctocyc 30911 . 2 class toCyc
2 vd . . 3 setvar 𝑑
3 cvv 3409 . . 3 class V
4 vw . . . 4 setvar 𝑤
5 vu . . . . . . . 8 setvar 𝑢
65cv 1537 . . . . . . 7 class 𝑢
76cdm 5528 . . . . . 6 class dom 𝑢
82cv 1537 . . . . . 6 class 𝑑
97, 8, 6wf1 6337 . . . . 5 wff 𝑢:dom 𝑢1-1𝑑
108cword 13926 . . . . 5 class Word 𝑑
119, 5, 10crab 3074 . . . 4 class {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑}
12 cid 5433 . . . . . 6 class I
134cv 1537 . . . . . . . 8 class 𝑤
1413crn 5529 . . . . . . 7 class ran 𝑤
158, 14cdif 3857 . . . . . 6 class (𝑑 ∖ ran 𝑤)
1612, 15cres 5530 . . . . 5 class ( I ↾ (𝑑 ∖ ran 𝑤))
17 c1 10589 . . . . . . 7 class 1
18 ccsh 14210 . . . . . . 7 class cyclShift
1913, 17, 18co 7156 . . . . . 6 class (𝑤 cyclShift 1)
2013ccnv 5527 . . . . . 6 class 𝑤
2119, 20ccom 5532 . . . . 5 class ((𝑤 cyclShift 1) ∘ 𝑤)
2216, 21cun 3858 . . . 4 class (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤))
234, 11, 22cmpt 5116 . . 3 class (𝑤 ∈ {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤)))
242, 3, 23cmpt 5116 . 2 class (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤))))
251, 24wceq 1538 1 wff toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤))))
 Colors of variables: wff setvar class This definition is referenced by:  tocycval  30913
 Copyright terms: Public domain W3C validator