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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift 𝑀 ) = ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
2 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
3 addcom ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
4 1 2 3 syl2anr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
5 4 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
6 5 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) = ( 𝑊 cyclShift ( 𝑁 + 𝑀 ) ) )
7 2cshw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) )
8 7 3com23 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) )
9 2cshw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift 𝑀 ) = ( 𝑊 cyclShift ( 𝑁 + 𝑀 ) ) )
10 6 8 9 3eqtr4rd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift 𝑀 ) = ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) )