Metamath Proof Explorer

Theorem shftval2

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

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

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
3 2 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - B ) e. CC )
4 addcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A + C ) e. CC )
5 1 shftval 
 |-  ( ( ( A - B ) e. CC /\ ( A + C ) e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + C ) ) = ( F ` ( ( A + C ) - ( A - B ) ) ) )
6 3 4 5 3imp3i2an 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + C ) ) = ( F ` ( ( A + C ) - ( A - B ) ) ) )
7 pnncan 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A + C ) - ( A - B ) ) = ( C + B ) )
8 7 3com23 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) - ( A - B ) ) = ( C + B ) )
9 addcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) )
10 9 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) )
11 8 10 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) - ( A - B ) ) = ( B + C ) )
12 11 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( F ` ( ( A + C ) - ( A - B ) ) ) = ( F ` ( B + C ) ) )
13 6 12 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + C ) ) = ( F ` ( B + C ) ) )