Metamath Proof Explorer

Theorem cshwidxm

Description: The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 of the original word. (Contributed by AV, 18-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidxm ⊢W∈WordV∧N∈1…W→WcyclShiftN⁡W−N=W⁡0

Proof

Step Hyp Ref Expression
1 simpl ⊢W∈WordV∧N∈1…W→W∈WordV
2 elfzelz ⊢N∈1…W→N∈ℤ
3 2 adantl ⊢W∈WordV∧N∈1…W→N∈ℤ
4 ubmelfzo ⊢N∈1…W→W−N∈0..^W
5 4 adantl ⊢W∈WordV∧N∈1…W→W−N∈0..^W
6 cshwidxmod ⊢W∈WordV∧N∈ℤ∧W−N∈0..^W→WcyclShiftN⁡W−N=W⁡W-N+NmodW
7 1 3 5 6 syl3anc ⊢W∈WordV∧N∈1…W→WcyclShiftN⁡W−N=W⁡W-N+NmodW
8 elfz1b ⊢N∈1…W↔N∈ℕ∧W∈ℕ∧N≤W
9 nncn ⊢N∈ℕ→N∈ℂ
10 nncn ⊢W∈ℕ→W∈ℂ
11 9 10 anim12ci ⊢N∈ℕ∧W∈ℕ→W∈ℂ∧N∈ℂ
12 11 3adant3 ⊢N∈ℕ∧W∈ℕ∧N≤W→W∈ℂ∧N∈ℂ
13 8 12 sylbi ⊢N∈1…W→W∈ℂ∧N∈ℂ
14 npcan ⊢W∈ℂ∧N∈ℂ→W-N+N=W
15 13 14 syl ⊢N∈1…W→W-N+N=W
16 15 oveq1d ⊢N∈1…W→W-N+NmodW=WmodW
17 16 adantl ⊢W∈WordV∧N∈1…W→W-N+NmodW=WmodW
18 nnrp ⊢W∈ℕ→W∈ℝ+
19 modid0 ⊢W∈ℝ+→WmodW=0
20 18 19 syl ⊢W∈ℕ→WmodW=0
21 20 3ad2ant2 ⊢N∈ℕ∧W∈ℕ∧N≤W→WmodW=0
22 8 21 sylbi ⊢N∈1…W→WmodW=0
23 22 adantl ⊢W∈WordV∧N∈1…W→WmodW=0
24 17 23 eqtrd ⊢W∈WordV∧N∈1…W→W-N+NmodW=0
25 24 fveq2d ⊢W∈WordV∧N∈1…W→W⁡W-N+NmodW=W⁡0
26 7 25 eqtrd ⊢W∈WordV∧N∈1…W→WcyclShiftN⁡W−N=W⁡0