Definition df-csh 13913

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 13911	. 2 class cyclShift
2		vw	. . 3 setvar 𝑤
3		vn	. . 3 setvar 𝑛
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1655	. . . . . 6 class 𝑓
6		cc0 10259	. . . . . . 7 class 0
7		vl	. . . . . . . 8 setvar 𝑙
8	7	cv 1655	. . . . . . 7 class 𝑙
9		cfzo 12767	. . . . . . 7 class ..^
10	6, 8, 9	co 6910	. . . . . 6 class (0..^𝑙)
11	5, 10	wfn 6122	. . . . 5 wff 𝑓 Fn (0..^𝑙)
12		cn0 11625	. . . . 5 class ℕ0
13	11, 7, 12	wrex 3118	. . . 4 wff ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)
14	13, 4	cab 2811	. . 3 class {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}
15		cz 11711	. . 3 class ℤ
16	2	cv 1655	. . . . 5 class 𝑤
17		c0 4146	. . . . 5 class ∅
18	16, 17	wceq 1656	. . . 4 wff 𝑤 = ∅
19	3	cv 1655	. . . . . . . 8 class 𝑛
20		chash 13417	. . . . . . . . 9 class ♯
21	16, 20	cfv 6127	. . . . . . . 8 class (♯‘𝑤)
22		cmo 12970	. . . . . . . 8 class mod
23	19, 21, 22	co 6910	. . . . . . 7 class (𝑛 mod (♯‘𝑤))
24	23, 21	cop 4405	. . . . . 6 class ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩
25		csubstr 13707	. . . . . 6 class substr
26	16, 24, 25	co 6910	. . . . 5 class (𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩)
27		cpfx 13756	. . . . . 6 class prefix
28	16, 23, 27	co 6910	. . . . 5 class (𝑤 prefix (𝑛 mod (♯‘𝑤)))
29		cconcat 13637	. . . . 5 class ++
30	26, 28, 29	co 6910	. . . 4 class ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))
31	18, 17, 30	cif 4308	. . 3 class if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤)))))
32	2, 3, 14, 15, 31	cmpt2 6912	. 2 class (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))
33	1, 32	wceq 1656	1 wff cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))

This definition is referenced by:  cshfn  13915  cshnz  13918  0csh0  13920