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∈WordV∧N∈ℤ→WcyclShiftNcyclShiftW−N=W

Proof

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