Theorem cshwidxm

Description: The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 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	cshwidxm	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> W e. Word V )
2		elfzelz	|- ( N e. ( 1 ... ( # ` W ) ) -> N e. ZZ )
3	2	adantl	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> N e. ZZ )
4		ubmelfzo	|- ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) - N ) e. ( 0 ..^ ( # ` W ) ) )
5	4	adantl	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( # ` W ) - N ) e. ( 0 ..^ ( # ` W ) ) )
6		cshwidxmod	|- ( ( W e. Word V /\ N e. ZZ /\ ( ( # ` W ) - N ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) ) )
7	1 3 5 6	syl3anc	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) ) )
8		elfz1b	|- ( N e. ( 1 ... ( # ` W ) ) <-> ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) )
9		nncn	|- ( N e. NN -> N e. CC )
10		nncn	|- ( ( # ` W ) e. NN -> ( # ` W ) e. CC )
11	9 10	anim12ci	|- ( ( N e. NN /\ ( # ` W ) e. NN ) -> ( ( # ` W ) e. CC /\ N e. CC ) )
12	11	3adant3	|- ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( ( # ` W ) e. CC /\ N e. CC ) )
13	8 12	sylbi	|- ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) e. CC /\ N e. CC ) )
14		npcan	|- ( ( ( # ` W ) e. CC /\ N e. CC ) -> ( ( ( # ` W ) - N ) + N ) = ( # ` W ) )
15	13 14	syl	|- ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( # ` W ) - N ) + N ) = ( # ` W ) )
16	15	oveq1d	|- ( N e. ( 1 ... ( # ` W ) ) -> ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) = ( ( # ` W ) mod ( # ` W ) ) )
17	16	adantl	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) = ( ( # ` W ) mod ( # ` W ) ) )
18		nnrp	|- ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
19		modid0	|- ( ( # ` W ) e. RR+ -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
20	18 19	syl	|- ( ( # ` W ) e. NN -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
21	20	3ad2ant2	|- ( ( N e. NN /\ ( # ` W ) e. NN /\ N <_ ( # ` W ) ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
22	8 21	sylbi	|- ( N e. ( 1 ... ( # ` W ) ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
23	22	adantl	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
24	17 23	eqtrd	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) = 0 )
25	24	fveq2d	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( W ` ( ( ( ( # ` W ) - N ) + N ) mod ( # ` W ) ) ) = ( W ` 0 ) )
26	7 25	eqtrd	|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - N ) ) = ( W ` 0 ) )