Definition df-csh

Description: Perform a cyclical shift for an arbitrary class. Meaningful only for words w e. Word S 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsh	⊢ cyclShift
1		vw	⊢ 𝑤
2		vf	⊢ 𝑓
3		vl	⊢ 𝑙
4		cn0	⊢ ℕ0
5	2	cv	⊢ 𝑓
6		cc0	⊢ 0
7		cfzo	⊢ ..^
8	3	cv	⊢ 𝑙
9	6 8 7	co	⊢ ( 0 ..^ 𝑙 )
10	5 9	wfn	⊢ 𝑓 Fn ( 0 ..^ 𝑙 )
11	10 3 4	wrex	⊢ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 )
12	11 2	cab	⊢ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) }
13		vn	⊢ 𝑛
14		cz	⊢ ℤ
15	1	cv	⊢ 𝑤
16		c0	⊢ ∅
17	15 16	wceq	⊢ 𝑤 = ∅
18		csubstr	⊢ substr
19	13	cv	⊢ 𝑛
20		cmo	⊢ mod
21		chash	⊢ ♯
22	15 21	cfv	⊢ ( ♯ ‘ 𝑤 )
23	19 22 20	co	⊢ ( 𝑛 mod ( ♯ ‘ 𝑤 ) )
24	23 22	cop	⊢ ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩
25	15 24 18	co	⊢ ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ )
26		cconcat	⊢ ++
27		cpfx	⊢ prefix
28	15 23 27	co	⊢ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) )
29	25 28 26	co	⊢ ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) )
30	17 16 29	cif	⊢ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) )
31	1 13 12 14 30	cmpo	⊢ ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )
32	0 31	wceq	⊢ cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )