Theorem shftval4

Description: Value of a sequence shifted by -u A . (Contributed by NM, 18-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	|- F e. _V
2		negcl	|- ( A e. CC -> -u A e. CC )
3	1	shftval	|- ( ( -u A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( B - -u A ) ) )
4	2 3	sylan	|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( B - -u A ) ) )
5		subneg	|- ( ( B e. CC /\ A e. CC ) -> ( B - -u A ) = ( B + A ) )
6	5	ancoms	|- ( ( A e. CC /\ B e. CC ) -> ( B - -u A ) = ( B + A ) )
7		addcom	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
8	6 7	eqtr4d	|- ( ( A e. CC /\ B e. CC ) -> ( B - -u A ) = ( A + B ) )
9	8	fveq2d	|- ( ( A e. CC /\ B e. CC ) -> ( F ` ( B - -u A ) ) = ( F ` ( A + B ) ) )
10	4 9	eqtrd	|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( A + B ) ) )