Metamath Proof Explorer

Theorem cshwidxm1

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

Ref Expression
Assertion cshwidxm1 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
2 elfzoelz ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
3 2 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
4 ubmelm1fzo ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 4 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
7 1 3 5 6 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
8 elfzoel2 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
9 8 zcnd ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
10 2 zcnd ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℂ )
11 1cnd ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 1 ∈ ℂ )
12 nnpcan ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
13 9 10 11 12 syl3anc ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
14 13 oveq1d ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) )
15 14 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) )
16 elfzo0 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) )
17 nnre ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ )
18 peano2rem ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ )
19 17 18 syl ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ )
20 nnrp ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
21 19 20 jca ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) )
22 21 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) )
23 16 22 sylbi ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) )
24 nnm1ge0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 0 ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
25 24 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 0 ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
26 16 25 sylbi ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 0 ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
27 zre ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( ♯ ‘ 𝑊 ) ∈ ℝ )
28 27 ltm1d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) )
29 8 28 syl ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) )
30 23 26 29 jca32 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) ) ) )
31 30 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) ) ) )
32 modid ⊢ ( ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
33 31 32 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
34 15 33 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
35 34 fveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
36 7 35 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )