Step |
Hyp |
Ref |
Expression |
1 |
|
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 ) ) ) ) ) ) |
2 |
|
0ex |
|- (/) e. _V |
3 |
|
ovex |
|- ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) e. _V |
4 |
2 3
|
ifex |
|- if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) e. _V |
5 |
1 4
|
dmmpo |
|- dom cyclShift = ( { f | E. l e. NN0 f Fn ( 0 ..^ l ) } X. ZZ ) |
6 |
|
id |
|- ( -. N e. ZZ -> -. N e. ZZ ) |
7 |
6
|
intnand |
|- ( -. N e. ZZ -> -. ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) ) |
8 |
|
ndmovg |
|- ( ( dom cyclShift = ( { f | E. l e. NN0 f Fn ( 0 ..^ l ) } X. ZZ ) /\ -. ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) ) -> ( W cyclShift N ) = (/) ) |
9 |
5 7 8
|
sylancr |
|- ( -. N e. ZZ -> ( W cyclShift N ) = (/) ) |