Metamath Proof Explorer

Theorem cshfn

Description: Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018) (Revised by AV, 17-Nov-2018) (Revised by AV, 4-Nov-2022)

Ref Expression
Assertion cshfn 
|- ( ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) -> ( W cyclShift N ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( w = W -> ( w = (/) <-> W = (/) ) )
2 1 adantr 
 |-  ( ( w = W /\ n = N ) -> ( w = (/) <-> W = (/) ) )
3 simpl 
 |-  ( ( w = W /\ n = N ) -> w = W )
4 simpr 
 |-  ( ( w = W /\ n = N ) -> n = N )
5 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
6 5 adantr 
 |-  ( ( w = W /\ n = N ) -> ( # ` w ) = ( # ` W ) )
7 4 6 oveq12d 
 |-  ( ( w = W /\ n = N ) -> ( n mod ( # ` w ) ) = ( N mod ( # ` W ) ) )
8 7 6 opeq12d 
 |-  ( ( w = W /\ n = N ) -> <. ( n mod ( # ` w ) ) , ( # ` w ) >. = <. ( N mod ( # ` W ) ) , ( # ` W ) >. )
9 3 8 oveq12d 
 |-  ( ( w = W /\ n = N ) -> ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) = ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) )
10 3 7 oveq12d 
 |-  ( ( w = W /\ n = N ) -> ( w prefix ( n mod ( # ` w ) ) ) = ( W prefix ( N mod ( # ` W ) ) ) )
11 9 10 oveq12d 
 |-  ( ( w = W /\ n = N ) -> ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
12 2 11 ifbieq2d 
 |-  ( ( w = W /\ n = N ) -> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )
13 df-csh 
 |-  cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )
14 0ex 
 |-  (/) e. _V
15 ovex 
 |-  ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) e. _V
16 14 15 ifex 
 |-  if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) e. _V
17 12 13 16 ovmpoa 
 |-  ( ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) -> ( W cyclShift N ) = if ( W = (/) , (/) , ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ) )