Theorem shftvalg

Description: Value of a sequence shifted by A . (Contributed by Scott Fenton, 16-Dec-2017)

	Ref	Expression
Assertion	shftvalg	$$⊢\left(F\in V\wedge 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		oveq1	$$⊢f=F\to f\mathrm{shift}A=F\mathrm{shift}A$$
2	1	fveq1d	$$⊢f=F\to \left(f\mathrm{shift}A\right)\left(B\right)=\left(F\mathrm{shift}A\right)\left(B\right)$$
3		fveq1	$$⊢f=F\to f\left(B-A\right)=F\left(B-A\right)$$
4	2 3	eqeq12d	$$⊢f=F\to \left(\left(f\mathrm{shift}A\right)\left(B\right)=f\left(B-A\right)\leftrightarrow \left(F\mathrm{shift}A\right)\left(B\right)=F\left(B-A\right)\right)$$
5	4	imbi2d	$$⊢f=F\to \left(\left(\left(A\in ℂ\wedge B\in ℂ\right)\to \left(f\mathrm{shift}A\right)\left(B\right)=f\left(B-A\right)\right)\leftrightarrow \left(\left(A\in ℂ\wedge B\in ℂ\right)\to \left(F\mathrm{shift}A\right)\left(B\right)=F\left(B-A\right)\right)\right)$$
6		vex	$$⊢f\in \mathrm{V}$$
7	6	shftval	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(f\mathrm{shift}A\right)\left(B\right)=f\left(B-A\right)$$
8	5 7	vtoclg	$$⊢F\in V\to \left(\left(A\in ℂ\wedge B\in ℂ\right)\to \left(F\mathrm{shift}A\right)\left(B\right)=F\left(B-A\right)\right)$$
9	8	3impib	$$⊢\left(F\in V\wedge A\in ℂ\wedge B\in ℂ\right)\to \left(F\mathrm{shift}A\right)\left(B\right)=F\left(B-A\right)$$