Metamath Proof Explorer

Theorem shftval2

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

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

Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 subcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}\in ℂ$
3 2 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}-{B}\in ℂ$
4 addcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{C}\in ℂ$
5 1 shftval ${⊢}\left({A}-{B}\in ℂ\wedge {A}+{C}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}+{C}\right)={F}\left({A}+{C}-\left({A}-{B}\right)\right)$
6 3 4 5 3imp3i2an ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}+{C}\right)={F}\left({A}+{C}-\left({A}-{B}\right)\right)$
7 pnncan ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{C}-\left({A}-{B}\right)={C}+{B}$
8 7 3com23 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{C}-\left({A}-{B}\right)={C}+{B}$
9 addcom ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}+{C}={C}+{B}$
10 9 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}+{C}={C}+{B}$
11 8 10 eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{C}-\left({A}-{B}\right)={B}+{C}$
12 11 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {F}\left({A}+{C}-\left({A}-{B}\right)\right)={F}\left({B}+{C}\right)$
13 6 12 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}+{C}\right)={F}\left({B}+{C}\right)$