Metamath Proof Explorer

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]↔{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)$