Definition df-csh 14142

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 14141	. 2 class cyclShift
2		vw	. . 3 setvar 𝑤
3		vn	. . 3 setvar 𝑛
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1537	. . . . . 6 class 𝑓
6		cc0 10526	. . . . . . 7 class 0
7		vl	. . . . . . . 8 setvar 𝑙
8	7	cv 1537	. . . . . . 7 class 𝑙
9		cfzo 13028	. . . . . . 7 class ..^
10	6, 8, 9	co 7135	. . . . . 6 class (0..^𝑙)
11	5, 10	wfn 6319	. . . . 5 wff 𝑓 Fn (0..^𝑙)
12		cn0 11885	. . . . 5 class ℕ0
13	11, 7, 12	wrex 3107	. . . 4 wff ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)
14	13, 4	cab 2776	. . 3 class {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}
15		cz 11969	. . 3 class ℤ
16	2	cv 1537	. . . . 5 class 𝑤
17		c0 4243	. . . . 5 class ∅
18	16, 17	wceq 1538	. . . 4 wff 𝑤 = ∅
19	3	cv 1537	. . . . . . . 8 class 𝑛
20		chash 13686	. . . . . . . . 9 class ♯
21	16, 20	cfv 6324	. . . . . . . 8 class (♯‘𝑤)
22		cmo 13232	. . . . . . . 8 class mod
23	19, 21, 22	co 7135	. . . . . . 7 class (𝑛 mod (♯‘𝑤))
24	23, 21	cop 4531	. . . . . 6 class ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩
25		csubstr 13993	. . . . . 6 class substr
26	16, 24, 25	co 7135	. . . . 5 class (𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩)
27		cpfx 14023	. . . . . 6 class prefix
28	16, 23, 27	co 7135	. . . . 5 class (𝑤 prefix (𝑛 mod (♯‘𝑤)))
29		cconcat 13913	. . . . 5 class ++
30	26, 28, 29	co 7135	. . . 4 class ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))
31	18, 17, 30	cif 4425	. . 3 class if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤)))))
32	2, 3, 14, 15, 31	cmpo 7137	. 2 class (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))
33	1, 32	wceq 1538	1 wff cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))

This definition is referenced by:  cshfn  14143  cshnz  14145  0csh0  14146