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 ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ N ∈ ℤ → W cyclShift N ⁡ 0 = W ⁡ N mod W

Proof

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