This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccsh 
 |-  cyclShift
1 vw 
 |-  w
2 vf 
 |-  f
3 vl 
 |-  l
4 cn0 
 |-  NN0
5 2 cv 
 |-  f
6 cc0 
 |-  0
7 cfzo 
 |-  ..^
8 3 cv 
 |-  l
9 6 8 7 co 
 |-  ( 0 ..^ l )
10 5 9 wfn 
 |-  f Fn ( 0 ..^ l )
11 10 3 4 wrex 
 |-  E. l e. NN0 f Fn ( 0 ..^ l )
12 11 2 cab 
 |-  { f | E. l e. NN0 f Fn ( 0 ..^ l ) }
13 vn 
 |-  n
14 cz 
 |-  ZZ
15 1 cv 
 |-  w
16 c0 
 |-  (/)
17 15 16 wceq 
 |-  w = (/)
18 csubstr 
 |-  substr
19 13 cv 
 |-  n
20 cmo 
 |-  mod
21 chash 
 |-  #
22 15 21 cfv 
 |-  ( # ` w )
23 19 22 20 co 
 |-  ( n mod ( # ` w ) )
24 23 22 cop 
 |-  <. ( n mod ( # ` w ) ) , ( # ` w ) >.
25 15 24 18 co 
 |-  ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. )
26 cconcat 
 |-  ++
27 cpfx 
 |-  prefix
28 15 23 27 co 
 |-  ( w prefix ( n mod ( # ` w ) ) )
29 25 28 26 co 
 |-  ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) )
30 17 16 29 cif 
 |-  if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) )
31 1 13 12 14 30 cmpo 
 |-  ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )
32 0 31 wceq 
 |-  cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )