Metamath Proof Explorer

Definition df-csh

Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words w e. Word S or at least functions over half-open ranges of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018) (Revised by Mario Carneiro/Alexander van der Vekens/ Gerard Lang, 17-Nov-2018) (Revised by AV, 4-Nov-2022)

Ref Expression
Assertion df-csh ⊢ cyclShift = w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccsh class cyclShift
1 vw setvar w
2 vf setvar f
3 vl setvar l
4 cn0 class ℕ 0
5 2 cv setvar f
6 cc0 class 0
7 cfzo class ..^
8 3 cv setvar l
9 6 8 7 co class 0 ..^ l
10 5 9 wfn wff f Fn 0 ..^ l
11 10 3 4 wrex wff ∃ l ∈ ℕ 0 f Fn 0 ..^ l
12 11 2 cab class f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l
13 vn setvar n
14 cz class ℤ
15 1 cv setvar w
16 c0 class ∅
17 15 16 wceq wff w = ∅
18 csubstr class substr
19 13 cv setvar n
20 cmo class mod
21 chash class .
22 15 21 cfv class w
23 19 22 20 co class n mod w
24 23 22 cop class n mod w w
25 15 24 18 co class w substr n mod w w
26 cconcat class ++
27 cpfx class prefix
28 15 23 27 co class w prefix n mod w
29 25 28 26 co class w substr n mod w w ++ w prefix n mod w
30 17 16 29 cif class if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w
31 1 13 12 14 30 cmpo class w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w
32 0 31 wceq wff cyclShift = w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w