Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( w = W -> ( w = (/) <-> W = (/) ) ) |
2 |
1
|
adantr |
|- ( ( w = W /\ n = N ) -> ( w = (/) <-> W = (/) ) ) |
3 |
|
simpl |
|- ( ( w = W /\ n = N ) -> w = W ) |
4 |
|
simpr |
|- ( ( w = W /\ n = N ) -> n = N ) |
5 |
|
fveq2 |
|- ( w = W -> ( # ` w ) = ( # ` W ) ) |
6 |
5
|
adantr |
|- ( ( w = W /\ n = N ) -> ( # ` w ) = ( # ` W ) ) |
7 |
4 6
|
oveq12d |
|- ( ( w = W /\ n = N ) -> ( n mod ( # ` w ) ) = ( N mod ( # ` W ) ) ) |
8 |
7 6
|
opeq12d |
|- ( ( w = W /\ n = N ) -> <. ( n mod ( # ` w ) ) , ( # ` w ) >. = <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) |
9 |
3 8
|
oveq12d |
|- ( ( w = W /\ n = N ) -> ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) = ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) |
10 |
3 7
|
oveq12d |
|- ( ( w = W /\ n = N ) -> ( w prefix ( n mod ( # ` w ) ) ) = ( W prefix ( N mod ( # ` W ) ) ) ) |
11 |
9 10
|
oveq12d |
|- ( ( w = W /\ n = N ) -> ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) |
12 |
2 11
|
ifbieq2d |
|- ( ( w = W /\ n = N ) -> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) ) |
13 |
|
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 ) ) ) ) ) ) |
14 |
|
0ex |
|- (/) e. _V |
15 |
|
ovex |
|- ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. _V |
16 |
14 15
|
ifex |
|- if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) e. _V |
17 |
12 13 16
|
ovmpoa |
|- ( ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) -> ( W cyclShift N ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) ) |