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 𝑁 ) )