Users' Mathboxes 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 32005
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 32004 . 2 class toCyc
2 vd . . 3 setvar 𝑑
3 cvv 3444 . . 3 class V
4 vw . . . 4 setvar 𝑤
5 vu . . . . . . . 8 setvar 𝑢
65cv 1541 . . . . . . 7 class 𝑢
76cdm 5634 . . . . . 6 class dom 𝑢
82cv 1541 . . . . . 6 class 𝑑
97, 8, 6wf1 6494 . . . . 5 wff 𝑢:dom 𝑢1-1𝑑
108cword 14408 . . . . 5 class Word 𝑑
119, 5, 10crab 3406 . . . 4 class {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑}
12 cid 5531 . . . . . 6 class I
134cv 1541 . . . . . . . 8 class 𝑤
1413crn 5635 . . . . . . 7 class ran 𝑤
158, 14cdif 3908 . . . . . 6 class (𝑑 ∖ ran 𝑤)
1612, 15cres 5636 . . . . 5 class ( I ↾ (𝑑 ∖ ran 𝑤))
17 c1 11057 . . . . . . 7 class 1
18 ccsh 14682 . . . . . . 7 class cyclShift
1913, 17, 18co 7358 . . . . . 6 class (𝑤 cyclShift 1)
2013ccnv 5633 . . . . . 6 class 𝑤
2119, 20ccom 5638 . . . . 5 class ((𝑤 cyclShift 1) ∘ 𝑤)
2216, 21cun 3909 . . . 4 class (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤))
234, 11, 22cmpt 5189 . . 3 class (𝑤 ∈ {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤)))
242, 3, 23cmpt 5189 . 2 class (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤))))
251, 24wceq 1542 1 wff toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑𝑢:dom 𝑢1-1𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ 𝑤))))
Colors of variables: wff setvar class
This definition is referenced by:  tocycval  32006
  Copyright terms: Public domain W3C validator