Metamath Proof Explorer

Theorem cshword

Description: Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018) (Revised by AV, 12-Oct-2022)

Ref Expression
Assertion cshword 
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iswrd 
 |-  ( W e. Word V <-> E. l e. NN0 W : ( 0 ..^ l ) --> V )
2 ffn 
 |-  ( W : ( 0 ..^ l ) --> V -> W Fn ( 0 ..^ l ) )
3 2 reximi 
 |-  ( E. l e. NN0 W : ( 0 ..^ l ) --> V -> E. l e. NN0 W Fn ( 0 ..^ l ) )
4 1 3 sylbi 
 |-  ( W e. Word V -> E. l e. NN0 W Fn ( 0 ..^ l ) )
5 fneq1 
 |-  ( w = W -> ( w Fn ( 0 ..^ l ) <-> W Fn ( 0 ..^ l ) ) )
6 5 rexbidv 
 |-  ( w = W -> ( E. l e. NN0 w Fn ( 0 ..^ l ) <-> E. l e. NN0 W Fn ( 0 ..^ l ) ) )
7 6 elabg 
 |-  ( W e. Word V -> ( W e. { w | E. l e. NN0 w Fn ( 0 ..^ l ) } <-> E. l e. NN0 W Fn ( 0 ..^ l ) ) )
8 4 7 mpbird 
 |-  ( W e. Word V -> W e. { w | E. l e. NN0 w Fn ( 0 ..^ l ) } )
9 cshfn 
 |-  ( ( W e. { w | E. l e. NN0 w Fn ( 0 ..^ l ) } /\ N e. ZZ ) -> ( W cyclShift N ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )
10 8 9 sylan 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )
11 iftrue 
 |-  ( W = (/) -> if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = (/) )
12 11 adantr 
 |-  ( ( W = (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = (/) )
13 oveq1 
 |-  ( W = (/) -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) = ( (/) substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) )
14 swrd0 
 |-  ( (/) substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) = (/)
15 13 14 eqtrdi 
 |-  ( W = (/) -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) = (/) )
16 oveq1 
 |-  ( W = (/) -> ( W prefix ( N mod ( # ` W ) ) ) = ( (/) prefix ( N mod ( # ` W ) ) ) )
17 pfx0 
 |-  ( (/) prefix ( N mod ( # ` W ) ) ) = (/)
18 16 17 eqtrdi 
 |-  ( W = (/) -> ( W prefix ( N mod ( # ` W ) ) ) = (/) )
19 15 18 oveq12d 
 |-  ( W = (/) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) = ( (/) ++ (/) ) )
20 19 adantr 
 |-  ( ( W = (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) = ( (/) ++ (/) ) )
21 ccatidid 
 |-  ( (/) ++ (/) ) = (/)
22 20 21 eqtr2di 
 |-  ( ( W = (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> (/) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
23 12 22 eqtrd 
 |-  ( ( W = (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
24 iffalse 
 |-  ( -. W = (/) -> if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
25 24 adantr 
 |-  ( ( -. W = (/) /\ ( W e. Word V /\ N e. ZZ ) ) -> if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
26 23 25 pm2.61ian 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
27 10 26 eqtrd 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )