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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cshw1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
2		repswsymballbi	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
3	2	bicomd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
4	3	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
5	1 4	mpbid	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )