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\in \mathrm{V}$$
Assertion	shftcan1	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left(F\mathrm{shift}A\right)\mathrm{shift}\left(-A\right)\right)\left(B\right)=F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	$$⊢F\in \mathrm{V}$$
2		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
3	1	2shfti	$$⊢\left(A\in ℂ\wedge -A\in ℂ\right)\to \left(F\mathrm{shift}A\right)\mathrm{shift}\left(-A\right)=F\mathrm{shift}\left(A+\left(-A\right)\right)$$
4	2 3	mpdan	$$⊢A\in ℂ\to \left(F\mathrm{shift}A\right)\mathrm{shift}\left(-A\right)=F\mathrm{shift}\left(A+\left(-A\right)\right)$$
5		negid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$
6	5	oveq2d	$$⊢A\in ℂ\to F\mathrm{shift}\left(A+\left(-A\right)\right)=F\mathrm{shift}0$$
7	4 6	eqtrd	$$⊢A\in ℂ\to \left(F\mathrm{shift}A\right)\mathrm{shift}\left(-A\right)=F\mathrm{shift}0$$
8	7	fveq1d	$$⊢A\in ℂ\to \left(\left(F\mathrm{shift}A\right)\mathrm{shift}\left(-A\right)\right)\left(B\right)=\left(F\mathrm{shift}0\right)\left(B\right)$$
9	1	shftidt	$$⊢B\in ℂ\to \left(F\mathrm{shift}0\right)\left(B\right)=F\left(B\right)$$
10	8 9	sylan9eq	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left(F\mathrm{shift}A\right)\mathrm{shift}\left(-A\right)\right)\left(B\right)=F\left(B\right)$$