Theorem cshwcl

Description: A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 27-Oct-2018)

	Ref	Expression
Assertion	cshwcl	|- ( W e. Word V -> ( W cyclShift N ) e. Word V )

Proof

Step	Hyp	Ref	Expression
1		cshword	|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
2		swrdcl	|- ( W e. Word V -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V )
3		pfxcl	|- ( W e. Word V -> ( W prefix ( N mod ( # ` W ) ) ) e. Word V )
4		ccatcl	|- ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V /\ ( W prefix ( N mod ( # ` W ) ) ) e. Word V ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. Word V )
5	2 3 4	syl2anc	|- ( W e. Word V -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. Word V )
6	5	adantr	|- ( ( W e. Word V /\ N e. ZZ ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. Word V )
7	1 6	eqeltrd	|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) e. Word V )
8	7	expcom	|- ( N e. ZZ -> ( W e. Word V -> ( W cyclShift N ) e. Word V ) )
9		cshnz	|- ( -. N e. ZZ -> ( W cyclShift N ) = (/) )
10		wrd0	|- (/) e. Word V
11	9 10	eqeltrdi	|- ( -. N e. ZZ -> ( W cyclShift N ) e. Word V )
12	11	a1d	|- ( -. N e. ZZ -> ( W e. Word V -> ( W cyclShift N ) e. Word V ) )
13	8 12	pm2.61i	|- ( W e. Word V -> ( W cyclShift N ) e. Word V )