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	addid2d	⊢ ( 𝑁 ∈ ℤ → ( 0 + 𝑁 ) = 𝑁 )
11	10	3ad2ant3	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( 0 + 𝑁 ) = 𝑁 )
12	11	fvoveq1d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( 𝑊 ‘ ( ( 0 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
13	8 12	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 0 ) = ( 𝑊 ‘ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )