This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshwidx0mod

Description: The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidx0mod ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → 𝑊 ∈ Word 𝑉 )
2 simp3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
3 lennncl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
4 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
5 3 4 sylibr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 5 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
8 1 2 6 7 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
9 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
10 9 addlidd ⊢ ( 𝑁 ∈ ℤ → ( 0 + 𝑁 ) = 𝑁 )
11 10 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( 0 + 𝑁 ) = 𝑁 )
12 11 fvoveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( 𝑊 ‘ ( ( 0 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
13 8 12 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )