Metamath Proof Explorer

Theorem shftvalg

Description: Value of a sequence shifted by A . (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Assertion shftvalg 
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( f = F -> ( f shift A ) = ( F shift A ) )
2 1 fveq1d 
 |-  ( f = F -> ( ( f shift A ) ` B ) = ( ( F shift A ) ` B ) )
3 fveq1 
 |-  ( f = F -> ( f ` ( B - A ) ) = ( F ` ( B - A ) ) )
4 2 3 eqeq12d 
 |-  ( f = F -> ( ( ( f shift A ) ` B ) = ( f ` ( B - A ) ) <-> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) ) )
5 4 imbi2d 
 |-  ( f = F -> ( ( ( A e. CC /\ B e. CC ) -> ( ( f shift A ) ` B ) = ( f ` ( B - A ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) ) ) )
6 vex 
 |-  f e. _V
7 6 shftval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( f shift A ) ` B ) = ( f ` ( B - A ) ) )
8 5 7 vtoclg 
 |-  ( F e. V -> ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) ) )
9 8 3impib 
 |-  ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )