Step |
Hyp |
Ref |
Expression |
1 |
|
cshword |
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) |
2 |
|
swrdcl |
|- ( W e. Word V -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V ) |
3 |
|
pfxcl |
|- ( W e. Word V -> ( W prefix ( N mod ( # ` W ) ) ) e. Word V ) |
4 |
|
ccatcl |
|- ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V /\ ( W prefix ( N mod ( # ` W ) ) ) e. Word V ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. Word V ) |
5 |
2 3 4
|
syl2anc |
|- ( W e. Word V -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. Word V ) |
6 |
5
|
adantr |
|- ( ( W e. Word V /\ N e. ZZ ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. Word V ) |
7 |
1 6
|
eqeltrd |
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) e. Word V ) |
8 |
7
|
expcom |
|- ( N e. ZZ -> ( W e. Word V -> ( W cyclShift N ) e. Word V ) ) |
9 |
|
cshnz |
|- ( -. N e. ZZ -> ( W cyclShift N ) = (/) ) |
10 |
|
wrd0 |
|- (/) e. Word V |
11 |
9 10
|
eqeltrdi |
|- ( -. N e. ZZ -> ( W cyclShift N ) e. Word V ) |
12 |
11
|
a1d |
|- ( -. N e. ZZ -> ( W e. Word V -> ( W cyclShift N ) e. Word V ) ) |
13 |
8 12
|
pm2.61i |
|- ( W e. Word V -> ( W cyclShift N ) e. Word V ) |