Definition df-csh 14153

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.) (Revised by AV, 4-Nov-2022.)

Assertion

Ref	Expression
df-csh	⊢ cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))

Distinct variable group:   𝑓,𝑙,𝑛,𝑤

Detailed syntax breakdown of Definition df-csh

Step	Hyp	Ref	Expression
1		ccsh 14152	. 2 class cyclShift
2		vw	. . 3 setvar 𝑤
3		vn	. . 3 setvar 𝑛
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1536	. . . . . 6 class 𝑓
6		cc0 10539	. . . . . . 7 class 0
7		vl	. . . . . . . 8 setvar 𝑙
8	7	cv 1536	. . . . . . 7 class 𝑙
9		cfzo 13036	. . . . . . 7 class ..^
10	6, 8, 9	co 7158	. . . . . 6 class (0..^𝑙)
11	5, 10	wfn 6352	. . . . 5 wff 𝑓 Fn (0..^𝑙)
12		cn0 11900	. . . . 5 class ℕ0
13	11, 7, 12	wrex 3141	. . . 4 wff ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)
14	13, 4	cab 2801	. . 3 class {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}
15		cz 11984	. . 3 class ℤ
16	2	cv 1536	. . . . 5 class 𝑤
17		c0 4293	. . . . 5 class ∅
18	16, 17	wceq 1537	. . . 4 wff 𝑤 = ∅
19	3	cv 1536	. . . . . . . 8 class 𝑛
20		chash 13693	. . . . . . . . 9 class ♯
21	16, 20	cfv 6357	. . . . . . . 8 class (♯‘𝑤)
22		cmo 13240	. . . . . . . 8 class mod
23	19, 21, 22	co 7158	. . . . . . 7 class (𝑛 mod (♯‘𝑤))
24	23, 21	cop 4575	. . . . . 6 class ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩
25		csubstr 14004	. . . . . 6 class substr
26	16, 24, 25	co 7158	. . . . 5 class (𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩)
27		cpfx 14034	. . . . . 6 class prefix
28	16, 23, 27	co 7158	. . . . 5 class (𝑤 prefix (𝑛 mod (♯‘𝑤)))
29		cconcat 13924	. . . . 5 class ++
30	26, 28, 29	co 7158	. . . 4 class ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))
31	18, 17, 30	cif 4469	. . 3 class if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤)))))
32	2, 3, 14, 15, 31	cmpo 7160	. 2 class (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))
33	1, 32	wceq 1537	1 wff cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))

This definition is referenced by:  cshfn  14154  cshnz  14156  0csh0  14157