Definition df-csh 13535

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.)

Assertion

Ref	Expression
df-csh	|- cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w substr <. 0 , ( n mod ( # ` w ) ) >. ) ) ) )

Distinct variable group:   f, l, n, w

Detailed syntax breakdown of Definition df-csh

Step	Hyp	Ref	Expression
1		ccsh 13534	. 2 class cyclShift
2		vw	. . 3 setvar w
3		vn	. . 3 setvar n
4		vf	. . . . . . 7 setvar f
5	4	cv 1482	. . . . . 6 class f
6		cc0 9936	. . . . . . 7 class 0
7		vl	. . . . . . . 8 setvar l
8	7	cv 1482	. . . . . . 7 class l
9		cfzo 12465	. . . . . . 7 class ..^
10	6, 8, 9	co 6650	. . . . . 6 class ( 0..^ l )
11	5, 10	wfn 5883	. . . . 5 wff f Fn ( 0..^ l )
12		cn0 11292	. . . . 5 class NN0
13	11, 7, 12	wrex 2913	. . . 4 wff E. l e. NN0 f Fn ( 0..^ l )
14	13, 4	cab 2608	. . 3 class { f | E. l e. NN0 f Fn ( 0..^ l ) }
15		cz 11377	. . 3 class ZZ
16	2	cv 1482	. . . . 5 class w
17		c0 3915	. . . . 5 class (/)
18	16, 17	wceq 1483	. . . 4 wff w = (/)
19	3	cv 1482	. . . . . . . 8 class n
20		chash 13117	. . . . . . . . 9 class #
21	16, 20	cfv 5888	. . . . . . . 8 class ( # ` w )
22		cmo 12668	. . . . . . . 8 class mod
23	19, 21, 22	co 6650	. . . . . . 7 class ( n mod ( # ` w ) )
24	23, 21	cop 4183	. . . . . 6 class <. ( n mod ( # ` w ) ) , ( # ` w ) >.
25		csubstr 13295	. . . . . 6 class substr
26	16, 24, 25	co 6650	. . . . 5 class ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. )
27	6, 23	cop 4183	. . . . . 6 class <. 0 , ( n mod ( # ` w ) ) >.
28	16, 27, 25	co 6650	. . . . 5 class ( w substr <. 0 , ( n mod ( # ` w ) ) >. )
29		cconcat 13293	. . . . 5 class ++
30	26, 28, 29	co 6650	. . . 4 class ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w substr <. 0 , ( n mod ( # ` w ) ) >. ) )
31	18, 17, 30	cif 4086	. . 3 class if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w substr <. 0 , ( n mod ( # ` w ) ) >. ) ) )
32	2, 3, 14, 15, 31	cmpt2 6652	. 2 class ( w e. { f | E. l e. NN0 f Fn ( 0..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w substr <. 0 , ( n mod ( # ` w ) ) >. ) ) ) )
33	1, 32	wceq 1483	1 wff cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w substr <. 0 , ( n mod ( # ` w ) ) >. ) ) ) )

This definition is referenced by:  cshfn  13536  cshnz  13538  0csh0  13539