Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
|- F e. _V |
2 |
|
negneg |
|- ( A e. CC -> -u -u A = A ) |
3 |
2
|
adantr |
|- ( ( A e. CC /\ B e. CC ) -> -u -u A = A ) |
4 |
3
|
oveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift -u A ) shift -u -u A ) = ( ( F shift -u A ) shift A ) ) |
5 |
4
|
fveq1d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift -u -u A ) ` B ) = ( ( ( F shift -u A ) shift A ) ` B ) ) |
6 |
|
negcl |
|- ( A e. CC -> -u A e. CC ) |
7 |
1
|
shftcan1 |
|- ( ( -u A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift -u -u A ) ` B ) = ( F ` B ) ) |
8 |
6 7
|
sylan |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift -u -u A ) ` B ) = ( F ` B ) ) |
9 |
5 8
|
eqtr3d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift A ) ` B ) = ( F ` B ) ) |