MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-csh Structured version   Visualization version   GIF version

Definition df-csh 13735
Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words 𝑤 ∈ Word 𝑆 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.)
Assertion
Ref Expression
df-csh cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))))
Distinct variable group:   𝑓,𝑙,𝑛,𝑤

Detailed syntax breakdown of Definition df-csh
StepHypRef Expression
1 ccsh 13734 . 2 class cyclShift
2 vw . . 3 setvar 𝑤
3 vn . . 3 setvar 𝑛
4 vf . . . . . . 7 setvar 𝑓
54cv 1631 . . . . . 6 class 𝑓
6 cc0 10128 . . . . . . 7 class 0
7 vl . . . . . . . 8 setvar 𝑙
87cv 1631 . . . . . . 7 class 𝑙
9 cfzo 12659 . . . . . . 7 class ..^
106, 8, 9co 6813 . . . . . 6 class (0..^𝑙)
115, 10wfn 6044 . . . . 5 wff 𝑓 Fn (0..^𝑙)
12 cn0 11484 . . . . 5 class 0
1311, 7, 12wrex 3051 . . . 4 wff 𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)
1413, 4cab 2746 . . 3 class {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}
15 cz 11569 . . 3 class
162cv 1631 . . . . 5 class 𝑤
17 c0 4058 . . . . 5 class
1816, 17wceq 1632 . . . 4 wff 𝑤 = ∅
193cv 1631 . . . . . . . 8 class 𝑛
20 chash 13311 . . . . . . . . 9 class
2116, 20cfv 6049 . . . . . . . 8 class (♯‘𝑤)
22 cmo 12862 . . . . . . . 8 class mod
2319, 21, 22co 6813 . . . . . . 7 class (𝑛 mod (♯‘𝑤))
2423, 21cop 4327 . . . . . 6 class ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩
25 csubstr 13481 . . . . . 6 class substr
2616, 24, 25co 6813 . . . . 5 class (𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩)
276, 23cop 4327 . . . . . 6 class ⟨0, (𝑛 mod (♯‘𝑤))⟩
2816, 27, 25co 6813 . . . . 5 class (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩)
29 cconcat 13479 . . . . 5 class ++
3026, 28, 29co 6813 . . . 4 class ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))
3118, 17, 30cif 4230 . . 3 class if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩)))
322, 3, 14, 15, 31cmpt2 6815 . 2 class (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))))
331, 32wceq 1632 1 wff cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))))
Colors of variables: wff setvar class
This definition is referenced by:  cshfn  13736  cshnz  13738  0csh0  13739
  Copyright terms: Public domain W3C validator