Theorem shftcan1

Description: Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	|- F e. _V
2		negcl	|- ( A e. CC -> -u A e. CC )
3	1	2shfti	|- ( ( A e. CC /\ -u A e. CC ) -> ( ( F shift A ) shift -u A ) = ( F shift ( A + -u A ) ) )
4	2 3	mpdan	|- ( A e. CC -> ( ( F shift A ) shift -u A ) = ( F shift ( A + -u A ) ) )
5		negid	|- ( A e. CC -> ( A + -u A ) = 0 )
6	5	oveq2d	|- ( A e. CC -> ( F shift ( A + -u A ) ) = ( F shift 0 ) )
7	4 6	eqtrd	|- ( A e. CC -> ( ( F shift A ) shift -u A ) = ( F shift 0 ) )
8	7	fveq1d	|- ( A e. CC -> ( ( ( F shift A ) shift -u A ) ` B ) = ( ( F shift 0 ) ` B ) )
9	1	shftidt	|- ( B e. CC -> ( ( F shift 0 ) ` B ) = ( F ` B ) )
10	8 9	sylan9eq	|- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift A ) shift -u A ) ` B ) = ( F ` B ) )