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 ) ) )