Metamath Proof Explorer


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 )