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

Metamath Proof Explorer

Theorem shftval

Description: Value of a sequence shifted by A . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 4-Nov-2013)

Ref Expression
Hypothesis shftfval.1 
|- F e. _V
Assertion shftval 
|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 1 shftfib 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
3 2 eleq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( x e. ( ( F shift A ) " { B } ) <-> x e. ( F " { ( B - A ) } ) ) )
4 3 iotabidv 
 |-  ( ( A e. CC /\ B e. CC ) -> ( iota x x e. ( ( F shift A ) " { B } ) ) = ( iota x x e. ( F " { ( B - A ) } ) ) )
5 dffv3 
 |-  ( ( F shift A ) ` B ) = ( iota x x e. ( ( F shift A ) " { B } ) )
6 dffv3 
 |-  ( F ` ( B - A ) ) = ( iota x x e. ( F " { ( B - A ) } ) )
7 4 5 6 3eqtr4g 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )