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∈WordV∧WcyclShift1=W→W=W⁡0repeatSW

Proof

Step Hyp Ref Expression
1 cshw1 ⊢W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0
2 repswsymballbi ⊢W∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
3 2 bicomd ⊢W∈WordV→∀i∈0..^WW⁡i=W⁡0↔W=W⁡0repeatSW
4 3 adantr ⊢W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0↔W=W⁡0repeatSW
5 1 4 mpbid ⊢W∈WordV∧WcyclShift1=W→W=W⁡0repeatSW