# Metamath Proof Explorer

## Theorem shftcan2

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

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 negneg ${⊢}{A}\in ℂ\to -\left(-{A}\right)={A}$
3 2 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to -\left(-{A}\right)={A}$
4 3 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}\left(-\left(-{A}\right)\right)=\left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}{A}$
5 4 fveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}\left(-\left(-{A}\right)\right)\right)\left({B}\right)=\left(\left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}{A}\right)\left({B}\right)$
6 negcl ${⊢}{A}\in ℂ\to -{A}\in ℂ$
7 1 shftcan1 ${⊢}\left(-{A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}\left(-\left(-{A}\right)\right)\right)\left({B}\right)={F}\left({B}\right)$
8 6 7 sylan ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}\left(-\left(-{A}\right)\right)\right)\left({B}\right)={F}\left({B}\right)$
9 5 8 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({F}\mathrm{shift}\left(-{A}\right)\right)\mathrm{shift}{A}\right)\left({B}\right)={F}\left({B}\right)$