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 ∈ Word V ∧ W cyclShift 1 = W → W = W ⁡ 0 repeatS W

Proof

Step Hyp Ref Expression
1 cshw1 ⊢ W ∈ Word V ∧ W cyclShift 1 = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
2 repswsymballbi ⊢ W ∈ Word V → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
3 2 bicomd ⊢ W ∈ Word V → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 ↔ W = W ⁡ 0 repeatS W
4 3 adantr ⊢ W ∈ Word V ∧ W cyclShift 1 = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 ↔ W = W ⁡ 0 repeatS W
5 1 4 mpbid ⊢ W ∈ Word V ∧ W cyclShift 1 = W → W = W ⁡ 0 repeatS W