Theorem 3cshw

Description: Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by AV, 6-Jun-2018) (Revised by AV, 1-Nov-2018)

	Ref	Expression
Assertion	3cshw	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2cshwid	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = 𝑊 )
2	1	3adant2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = 𝑊 )
3	2	eqcomd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑊 = ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )
4	3	oveq1d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) cyclShift 𝑁 ) )
5		cshwcl	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 )
6	5	3ad2ant1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 )
7		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
8	7	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
9		zsubcl	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ )
10	8 9	sylan	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ )
11	10	3adant2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ )
12		simp2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑁 ∈ ℤ )
13		2cshwcom	⊢ ( ( ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) cyclShift 𝑁 ) = ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )
14	6 11 12 13	syl3anc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) cyclShift 𝑁 ) = ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )
15	4 14	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )