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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( 𝑊 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
2 elfzelz ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
3 2 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
4 ubmelfzo ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 4 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
7 1 3 5 6 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
8 elfz1b ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) )
9 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
10 nncn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℂ )
11 9 10 anim12ci ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
12 11 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
13 8 12 sylbi ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
14 npcan ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) = ( ♯ ‘ 𝑊 ) )
15 13 14 syl ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) = ( ♯ ‘ 𝑊 ) )
16 15 oveq1d ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) )
17 16 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) )
18 nnrp ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
19 modid0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
20 18 19 syl ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
21 20 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
22 8 21 sylbi ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
23 22 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
24 17 23 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = 0 )
25 24 fveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 𝑁 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) )
26 7 25 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 𝑁 ) ) = ( 𝑊 ‘ 0 ) )