MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-csh Structured version   Unicode version

Definition df-csh 12816
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
StepHypRef Expression
1 ccsh 12815 . 2  class cyclShift
2 vw . . 3  setvar  w
3 vn . . 3  setvar  n
4 vf . . . . . . 7  setvar  f
54cv 1404 . . . . . 6  class  f
6 cc0 9522 . . . . . . 7  class  0
7 vl . . . . . . . 8  setvar  l
87cv 1404 . . . . . . 7  class  l
9 cfzo 11854 . . . . . . 7  class ..^
106, 8, 9co 6278 . . . . . 6  class  ( 0..^ l )
115, 10wfn 5564 . . . . 5  wff  f  Fn  ( 0..^ l )
12 cn0 10836 . . . . 5  class  NN0
1311, 7, 12wrex 2755 . . . 4  wff  E. l  e.  NN0  f  Fn  (
0..^ l )
1413, 4cab 2387 . . 3  class  { f  |  E. l  e. 
NN0  f  Fn  (
0..^ l ) }
15 cz 10905 . . 3  class  ZZ
162cv 1404 . . . . 5  class  w
17 c0 3738 . . . . 5  class  (/)
1816, 17wceq 1405 . . . 4  wff  w  =  (/)
193cv 1404 . . . . . . . 8  class  n
20 chash 12452 . . . . . . . . 9  class  #
2116, 20cfv 5569 . . . . . . . 8  class  ( # `  w )
22 cmo 12034 . . . . . . . 8  class  mod
2319, 21, 22co 6278 . . . . . . 7  class  ( n  mod  ( # `  w
) )
2423, 21cop 3978 . . . . . 6  class  <. (
n  mod  ( # `  w
) ) ,  (
# `  w ) >.
25 csubstr 12587 . . . . . 6  class substr
2616, 24, 25co 6278 . . . . 5  class  ( w substr  <. ( n  mod  ( # `
 w ) ) ,  ( # `  w
) >. )
276, 23cop 3978 . . . . . 6  class  <. 0 ,  ( n  mod  ( # `  w ) ) >.
2816, 27, 25co 6278 . . . . 5  class  ( w substr  <. 0 ,  ( n  mod  ( # `  w
) ) >. )
29 cconcat 12585 . . . . 5  class ++
3026, 28, 29co 6278 . . . 4  class  ( ( w substr  <. ( n  mod  ( # `  w ) ) ,  ( # `  w ) >. ) ++  ( w substr  <. 0 ,  ( n  mod  ( # `
 w ) )
>. ) )
3118, 17, 30cif 3885 . . 3  class  if ( w  =  (/) ,  (/) ,  ( ( w substr  <. (
n  mod  ( # `  w
) ) ,  (
# `  w ) >. ) ++  ( w substr  <. 0 ,  ( n  mod  ( # `  w ) ) >. ) ) )
322, 3, 14, 15, 31cmpt2 6280 . 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 ) ) >. ) ) ) )
331, 32wceq 1405 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
) ) >. )
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  cshfn  12817  cshnz  12819  0csh0  12820
  Copyright terms: Public domain W3C validator