Definition df-cshOLD 13943

Description: Obsolete version of df-csh 13942 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by Mario Carneiro/ Alexander van der Vekens/Gerard Lang, 17-Nov-2018.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   𝑓,𝑙,𝑛,𝑤

Detailed syntax breakdown of Definition df-cshOLD

Step	Hyp	Ref	Expression
1		ccshOLD 13941	. 2 class cyclShiftOLD
2		vw	. . 3 setvar 𝑤
3		vn	. . 3 setvar 𝑛
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1600	. . . . . 6 class 𝑓
6		cc0 10274	. . . . . . 7 class 0
7		vl	. . . . . . . 8 setvar 𝑙
8	7	cv 1600	. . . . . . 7 class 𝑙
9		cfzo 12789	. . . . . . 7 class ..^
10	6, 8, 9	co 6924	. . . . . 6 class (0..^𝑙)
11	5, 10	wfn 6132	. . . . 5 wff 𝑓 Fn (0..^𝑙)
12		cn0 11647	. . . . 5 class ℕ0
13	11, 7, 12	wrex 3091	. . . 4 wff ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)
14	13, 4	cab 2763	. . 3 class {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}
15		cz 11733	. . 3 class ℤ
16	2	cv 1600	. . . . 5 class 𝑤
17		c0 4141	. . . . 5 class ∅
18	16, 17	wceq 1601	. . . 4 wff 𝑤 = ∅
19	3	cv 1600	. . . . . . . 8 class 𝑛
20		chash 13441	. . . . . . . . 9 class ♯
21	16, 20	cfv 6137	. . . . . . . 8 class (♯‘𝑤)
22		cmo 12992	. . . . . . . 8 class mod
23	19, 21, 22	co 6924	. . . . . . 7 class (𝑛 mod (♯‘𝑤))
24	23, 21	cop 4404	. . . . . 6 class ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩
25		csubstr 13736	. . . . . 6 class substr
26	16, 24, 25	co 6924	. . . . 5 class (𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩)
27	6, 23	cop 4404	. . . . . 6 class ⟨0, (𝑛 mod (♯‘𝑤))⟩
28	16, 27, 25	co 6924	. . . . 5 class (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩)
29		cconcat 13666	. . . . 5 class ++
30	26, 28, 29	co 6924	. . . 4 class ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))
31	18, 17, 30	cif 4307	. . 3 class if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩)))
32	2, 3, 14, 15, 31	cmpt2 6926	. 2 class (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))))
33	1, 32	wceq 1601	1 wff cyclShiftOLD = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 substr ⟨0, (𝑛 mod (♯‘𝑤))⟩))))

This definition is referenced by:  cshfnOLD  13945  cshnzOLD  13948  0csh0OLD  13950