This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )