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

Metamath Proof Explorer

Theorem 2cshwcom

Description: Cyclically shifting a word two times is commutative. (Contributed by AV, 21-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by Mario Carneiro/AV, 1-Nov-2018)

Ref Expression
Assertion 2cshwcom ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N cyclShift M = W cyclShift M cyclShift N

Proof

Step Hyp Ref Expression
1 zcn ⊢ M ∈ ℤ → M ∈ ℂ
2 zcn ⊢ N ∈ ℤ → N ∈ ℂ
3 addcom ⊢ M ∈ ℂ ∧ N ∈ ℂ → M + N = N + M
4 1 2 3 syl2anr ⊢ N ∈ ℤ ∧ M ∈ ℤ → M + N = N + M
5 4 3adant1 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → M + N = N + M
6 5 oveq2d ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift M + N = W cyclShift N + M
7 2cshw ⊢ W ∈ Word V ∧ M ∈ ℤ ∧ N ∈ ℤ → W cyclShift M cyclShift N = W cyclShift M + N
8 7 3com23 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift M cyclShift N = W cyclShift M + N
9 2cshw ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N cyclShift M = W cyclShift N + M
10 6 8 9 3eqtr4rd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N cyclShift M = W cyclShift M cyclShift N