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 |
1
|
a1i |
|- ( N e. ZZ -> 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 ) ) ) ) ) ) ) |
3 |
|
iftrue |
|- ( w = (/) -> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) = (/) ) |
4 |
3
|
ad2antrl |
|- ( ( N e. ZZ /\ ( w = (/) /\ n = N ) ) -> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) = (/) ) |
5 |
|
0nn0 |
|- 0 e. NN0 |
6 |
|
f0 |
|- (/) : (/) --> _V |
7 |
|
ffn |
|- ( (/) : (/) --> _V -> (/) Fn (/) ) |
8 |
|
fzo0 |
|- ( 0 ..^ 0 ) = (/) |
9 |
8
|
eqcomi |
|- (/) = ( 0 ..^ 0 ) |
10 |
9
|
fneq2i |
|- ( (/) Fn (/) <-> (/) Fn ( 0 ..^ 0 ) ) |
11 |
7 10
|
sylib |
|- ( (/) : (/) --> _V -> (/) Fn ( 0 ..^ 0 ) ) |
12 |
6 11
|
ax-mp |
|- (/) Fn ( 0 ..^ 0 ) |
13 |
|
id |
|- ( 0 e. NN0 -> 0 e. NN0 ) |
14 |
|
oveq2 |
|- ( l = 0 -> ( 0 ..^ l ) = ( 0 ..^ 0 ) ) |
15 |
14
|
fneq2d |
|- ( l = 0 -> ( (/) Fn ( 0 ..^ l ) <-> (/) Fn ( 0 ..^ 0 ) ) ) |
16 |
15
|
adantl |
|- ( ( 0 e. NN0 /\ l = 0 ) -> ( (/) Fn ( 0 ..^ l ) <-> (/) Fn ( 0 ..^ 0 ) ) ) |
17 |
13 16
|
rspcedv |
|- ( 0 e. NN0 -> ( (/) Fn ( 0 ..^ 0 ) -> E. l e. NN0 (/) Fn ( 0 ..^ l ) ) ) |
18 |
5 12 17
|
mp2 |
|- E. l e. NN0 (/) Fn ( 0 ..^ l ) |
19 |
|
0ex |
|- (/) e. _V |
20 |
|
fneq1 |
|- ( f = (/) -> ( f Fn ( 0 ..^ l ) <-> (/) Fn ( 0 ..^ l ) ) ) |
21 |
20
|
rexbidv |
|- ( f = (/) -> ( E. l e. NN0 f Fn ( 0 ..^ l ) <-> E. l e. NN0 (/) Fn ( 0 ..^ l ) ) ) |
22 |
19 21
|
elab |
|- ( (/) e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } <-> E. l e. NN0 (/) Fn ( 0 ..^ l ) ) |
23 |
18 22
|
mpbir |
|- (/) e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } |
24 |
23
|
a1i |
|- ( N e. ZZ -> (/) e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } ) |
25 |
|
id |
|- ( N e. ZZ -> N e. ZZ ) |
26 |
19
|
a1i |
|- ( N e. ZZ -> (/) e. _V ) |
27 |
2 4 24 25 26
|
ovmpod |
|- ( N e. ZZ -> ( (/) cyclShift N ) = (/) ) |
28 |
|
cshnz |
|- ( -. N e. ZZ -> ( (/) cyclShift N ) = (/) ) |
29 |
27 28
|
pm2.61i |
|- ( (/) cyclShift N ) = (/) |