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 ) ) )