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 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W cyclShift M cyclShift N cyclShift W − M

Proof

Step Hyp Ref Expression
1 2cshwid ⊢ W ∈ Word V ∧ M ∈ ℤ → W cyclShift M cyclShift W − M = W
2 1 3adant2 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift M cyclShift W − M = W
3 2 eqcomd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W = W cyclShift M cyclShift W − M
4 3 oveq1d ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W cyclShift M cyclShift W − M cyclShift N
5 cshwcl ⊢ W ∈ Word V → W cyclShift M ∈ Word V
6 5 3ad2ant1 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift M ∈ Word V
7 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
8 7 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
9 zsubcl ⊢ W ∈ ℤ ∧ M ∈ ℤ → W − M ∈ ℤ
10 8 9 sylan ⊢ W ∈ Word V ∧ M ∈ ℤ → W − M ∈ ℤ
11 10 3adant2 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W − M ∈ ℤ
12 simp2 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → N ∈ ℤ
13 2cshwcom ⊢ W cyclShift M ∈ Word V ∧ W − M ∈ ℤ ∧ N ∈ ℤ → W cyclShift M cyclShift W − M cyclShift N = W cyclShift M cyclShift N cyclShift W − M
14 6 11 12 13 syl3anc ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift M cyclShift W − M cyclShift N = W cyclShift M cyclShift N cyclShift W − M
15 4 14 eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W cyclShift M cyclShift N cyclShift W − M