Theorem shftval

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

	Ref	Expression
Hypothesis	shftfval.1	$$⊢F\in \mathrm{V}$$
Assertion	shftval	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(F\mathrm{shift}A\right)\left(B\right)=F\left(B-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	$$⊢F\in \mathrm{V}$$
2	1	shftfib	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(F\mathrm{shift}A\right)\left[\left\{B\right\}\right]=F\left[\left\{B-A\right\}\right]$$
3	2	eleq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(x\in \left(F\mathrm{shift}A\right)\left[\left\{B\right\}\right]\leftrightarrow x\in F\left[\left\{B-A\right\}\right]\right)$$
4	3	iotabidv	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\iota x|x\in \left(F\mathrm{shift}A\right)\left[\left\{B\right\}\right]\right)=\left(\iota x|x\in F\left[\left\{B-A\right\}\right]\right)$$
5		dffv3	$$⊢\left(F\mathrm{shift}A\right)\left(B\right)=\left(\iota x|x\in \left(F\mathrm{shift}A\right)\left[\left\{B\right\}\right]\right)$$
6		dffv3	$$⊢F\left(B-A\right)=\left(\iota x|x\in F\left[\left\{B-A\right\}\right]\right)$$
7	4 5 6	3eqtr4g	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(F\mathrm{shift}A\right)\left(B\right)=F\left(B-A\right)$$