Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
|- F e. _V |
2 |
|
simpr |
|- ( ( B e. CC /\ A e. CC ) -> A e. CC ) |
3 |
|
addcl |
|- ( ( B e. CC /\ A e. CC ) -> ( B + A ) e. CC ) |
4 |
1
|
shftval |
|- ( ( A e. CC /\ ( B + A ) e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` ( ( B + A ) - A ) ) ) |
5 |
2 3 4
|
syl2anc |
|- ( ( B e. CC /\ A e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` ( ( B + A ) - A ) ) ) |
6 |
|
pncan |
|- ( ( B e. CC /\ A e. CC ) -> ( ( B + A ) - A ) = B ) |
7 |
6
|
fveq2d |
|- ( ( B e. CC /\ A e. CC ) -> ( F ` ( ( B + A ) - A ) ) = ( F ` B ) ) |
8 |
5 7
|
eqtrd |
|- ( ( B e. CC /\ A e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` B ) ) |
9 |
8
|
ancoms |
|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` B ) ) |