Metamath Proof Explorer

Theorem cshwidxn

Description: The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) 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 cshwidxn ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
2 elfzelz ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
3 2 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
4 elfz1b ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) )
5 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
6 4 5 sylbi ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
7 6 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
8 fzo0end ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 7 8 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
11 1 3 9 10 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
12 nncn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℂ )
13 12 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
14 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → 1 ∈ ℂ )
15 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → 𝑁 ∈ ℂ )
17 13 14 16 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
18 17 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
19 4 18 sylbi ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
20 subadd23 ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) = ( ( ♯ ‘ 𝑊 ) + ( 𝑁 − 1 ) ) )
21 19 20 syl ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) = ( ( ♯ ‘ 𝑊 ) + ( 𝑁 − 1 ) ) )
22 21 oveq1d ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( ♯ ‘ 𝑊 ) + ( 𝑁 − 1 ) ) mod ( ♯ ‘ 𝑊 ) ) )
23 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
24 23 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
25 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑁 ≤ ( ♯ ‘ 𝑊 ) )
26 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
27 nnz ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℤ )
28 26 27 anim12i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) )
29 28 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) )
30 zlem1lt ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 − 1 ) < ( ♯ ‘ 𝑊 ) ) )
31 29 30 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 − 1 ) < ( ♯ ‘ 𝑊 ) ) )
32 25 31 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑁 − 1 ) < ( ♯ ‘ 𝑊 ) )
33 24 5 32 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 − 1 ) < ( ♯ ‘ 𝑊 ) ) )
34 4 33 sylbi ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 − 1 ) < ( ♯ ‘ 𝑊 ) ) )
35 addmodid ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 − 1 ) < ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) + ( 𝑁 − 1 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 − 1 ) )
36 34 35 syl ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) + ( 𝑁 − 1 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 − 1 ) )
37 22 36 eqtrd ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑁 − 1 ) )
38 37 fveq2d ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
39 38 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
40 11 39 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )