Step |
Hyp |
Ref |
Expression |
1 |
|
hasheq0 |
|- ( W e. Word V -> ( ( # ` W ) = 0 <-> W = (/) ) ) |
2 |
|
elfzo0 |
|- ( N e. ( 0 ..^ ( # ` W ) ) <-> ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) ) |
3 |
|
elnnne0 |
|- ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) ) |
4 |
|
eqneqall |
|- ( ( # ` W ) = 0 -> ( ( # ` W ) =/= 0 -> ( W e. Word V -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
5 |
4
|
com12 |
|- ( ( # ` W ) =/= 0 -> ( ( # ` W ) = 0 -> ( W e. Word V -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
6 |
5
|
adantl |
|- ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( ( # ` W ) = 0 -> ( W e. Word V -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
7 |
3 6
|
sylbi |
|- ( ( # ` W ) e. NN -> ( ( # ` W ) = 0 -> ( W e. Word V -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
8 |
7
|
3ad2ant2 |
|- ( ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( ( # ` W ) = 0 -> ( W e. Word V -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
9 |
2 8
|
sylbi |
|- ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) = 0 -> ( W e. Word V -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
10 |
9
|
com13 |
|- ( W e. Word V -> ( ( # ` W ) = 0 -> ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
11 |
1 10
|
sylbird |
|- ( W e. Word V -> ( W = (/) -> ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
12 |
11
|
com23 |
|- ( W e. Word V -> ( N e. ( 0 ..^ ( # ` W ) ) -> ( W = (/) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) ) |
13 |
12
|
imp |
|- ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W = (/) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) |
14 |
13
|
com12 |
|- ( W = (/) -> ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) |
15 |
|
simpl |
|- ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> W e. Word V ) |
16 |
15
|
adantl |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> W e. Word V ) |
17 |
|
simpl |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> W =/= (/) ) |
18 |
|
elfzoelz |
|- ( N e. ( 0 ..^ ( # ` W ) ) -> N e. ZZ ) |
19 |
18
|
ad2antll |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> N e. ZZ ) |
20 |
|
cshwidx0mod |
|- ( ( W e. Word V /\ W =/= (/) /\ N e. ZZ ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` ( N mod ( # ` W ) ) ) ) |
21 |
16 17 19 20
|
syl3anc |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` ( N mod ( # ` W ) ) ) ) |
22 |
|
zmodidfzoimp |
|- ( N e. ( 0 ..^ ( # ` W ) ) -> ( N mod ( # ` W ) ) = N ) |
23 |
22
|
ad2antll |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N mod ( # ` W ) ) = N ) |
24 |
23
|
fveq2d |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` ( N mod ( # ` W ) ) ) = ( W ` N ) ) |
25 |
21 24
|
eqtrd |
|- ( ( W =/= (/) /\ ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) |
26 |
25
|
ex |
|- ( W =/= (/) -> ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) ) |
27 |
14 26
|
pm2.61ine |
|- ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) ) |