This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshw1repsw

Description: If cyclically shifting a word by 1 position results in the word itself, the word is a "repeated symbol word". Remark: also "valid" for an empty word! (Contributed by AV, 8-Nov-2018) (Proof shortened by AV, 10-Nov-2018)

Ref Expression
Assertion cshw1repsw 
|- ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) )

Proof

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 ) ) )