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

Metamath Proof Explorer

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 ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )