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 WWordVWNWcyclShiftN0=WNmodW

Proof

Step Hyp Ref Expression
1 simp1 WWordVWNWWordV
2 simp3 WWordVWNN
3 lennncl WWordVWW
4 lbfzo0 00..^WW
5 3 4 sylibr WWordVW00..^W
6 5 3adant3 WWordVWN00..^W
7 cshwidxmod WWordVN00..^WWcyclShiftN0=W0+NmodW
8 1 2 6 7 syl3anc WWordVWNWcyclShiftN0=W0+NmodW
9 zcn NN
10 9 addlidd N0+N=N
11 10 3ad2ant3 WWordVWN0+N=N
12 11 fvoveq1d WWordVWNW0+NmodW=WNmodW
13 8 12 eqtrd WWordVWNWcyclShiftN0=WNmodW