Step |
Hyp |
Ref |
Expression |
1 |
|
cshw1 |
|- ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) |
2 |
|
repswsymballbi |
|- ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) |
3 |
2
|
bicomd |
|- ( W e. Word V -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) |
4 |
3
|
adantr |
|- ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) |
5 |
1 4
|
mpbid |
|- ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) |