Definition df-csh 13386

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

Step	Hyp	Ref	Expression
1		ccsh 13385	. 2 class cyclShift
2		vw	. . 3 setvar 𝑤
3		vn	. . 3 setvar 𝑛
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1474	. . . . . 6 class 𝑓
6		cc0 9815	. . . . . . 7 class 0
7		vl	. . . . . . . 8 setvar 𝑙
8	7	cv 1474	. . . . . . 7 class 𝑙
9		cfzo 12334	. . . . . . 7 class ..^
10	6, 8, 9	co 6549	. . . . . 6 class (0..^𝑙)
11	5, 10	wfn 5799	. . . . 5 wff 𝑓 Fn (0..^𝑙)
12		cn0 11169	. . . . 5 class ℕ0
13	11, 7, 12	wrex 2897	. . . 4 wff ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)
14	13, 4	cab 2596	. . 3 class {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}
15		cz 11254	. . 3 class ℤ
16	2	cv 1474	. . . . 5 class 𝑤
17		c0 3874	. . . . 5 class ∅
18	16, 17	wceq 1475	. . . 4 wff 𝑤 = ∅
19	3	cv 1474	. . . . . . . 8 class 𝑛
20		chash 12979	. . . . . . . . 9 class #
21	16, 20	cfv 5804	. . . . . . . 8 class (#‘𝑤)
22		cmo 12530	. . . . . . . 8 class mod
23	19, 21, 22	co 6549	. . . . . . 7 class (𝑛 mod (#‘𝑤))
24	23, 21	cop 4131	. . . . . 6 class ⟨(𝑛 mod (#‘𝑤)), (#‘𝑤)⟩
25		csubstr 13150	. . . . . 6 class substr
26	16, 24, 25	co 6549	. . . . 5 class (𝑤 substr ⟨(𝑛 mod (#‘𝑤)), (#‘𝑤)⟩)
27	6, 23	cop 4131	. . . . . 6 class ⟨0, (𝑛 mod (#‘𝑤))⟩
28	16, 27, 25	co 6549	. . . . 5 class (𝑤 substr ⟨0, (𝑛 mod (#‘𝑤))⟩)
29		cconcat 13148	. . . . 5 class ++
30	26, 28, 29	co 6549	. . . 4 class ((𝑤 substr ⟨(𝑛 mod (#‘𝑤)), (#‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (#‘𝑤))⟩))
31	18, 17, 30	cif 4036	. . 3 class if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (#‘𝑤)), (#‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (#‘𝑤))⟩)))
32	2, 3, 14, 15, 31	cmpt2 6551	. 2 class (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (#‘𝑤)), (#‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (#‘𝑤))⟩))))
33	1, 32	wceq 1475	1 wff cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (#‘𝑤)), (#‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (#‘𝑤))⟩))))

This definition is referenced by:  cshfn  13387  cshnz  13389  0csh0  13390