Metamath Proof Explorer

Theorem 2cshwid

Description: Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion 2cshwid ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N cyclShift W − N = W

Proof

Step Hyp Ref Expression
1 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
2 1 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
3 zsubcl ⊢ W ∈ ℤ ∧ N ∈ ℤ → W − N ∈ ℤ
4 2 3 sylan ⊢ W ∈ Word V ∧ N ∈ ℤ → W − N ∈ ℤ
5 2cshw ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W − N ∈ ℤ → W cyclShift N cyclShift W − N = W cyclShift N + W - N
6 4 5 mpd3an3 ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N cyclShift W − N = W cyclShift N + W - N
7 zcn ⊢ N ∈ ℤ → N ∈ ℂ
8 1 nn0cnd ⊢ W ∈ Word V → W ∈ ℂ
9 pncan3 ⊢ N ∈ ℂ ∧ W ∈ ℂ → N + W - N = W
10 7 8 9 syl2anr ⊢ W ∈ Word V ∧ N ∈ ℤ → N + W - N = W
11 10 oveq2d ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N + W - N = W cyclShift W
12 cshwn ⊢ W ∈ Word V → W cyclShift W = W
13 12 adantr ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift W = W
14 6 11 13 3eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N cyclShift W − N = W