# Metamath Proof Explorer

## Theorem shftcan1

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

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 negcl ${⊢}{A}\in ℂ\to -{A}\in ℂ$
3 1 2shfti ${⊢}\left({A}\in ℂ\wedge -{A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\mathrm{shift}\left(-{A}\right)={F}\mathrm{shift}\left({A}+\left(-{A}\right)\right)$
4 2 3 mpdan ${⊢}{A}\in ℂ\to \left({F}\mathrm{shift}{A}\right)\mathrm{shift}\left(-{A}\right)={F}\mathrm{shift}\left({A}+\left(-{A}\right)\right)$
5 negid ${⊢}{A}\in ℂ\to {A}+\left(-{A}\right)=0$
6 5 oveq2d ${⊢}{A}\in ℂ\to {F}\mathrm{shift}\left({A}+\left(-{A}\right)\right)={F}\mathrm{shift}0$
7 4 6 eqtrd ${⊢}{A}\in ℂ\to \left({F}\mathrm{shift}{A}\right)\mathrm{shift}\left(-{A}\right)={F}\mathrm{shift}0$
8 7 fveq1d ${⊢}{A}\in ℂ\to \left(\left({F}\mathrm{shift}{A}\right)\mathrm{shift}\left(-{A}\right)\right)\left({B}\right)=\left({F}\mathrm{shift}0\right)\left({B}\right)$
9 1 shftidt ${⊢}{B}\in ℂ\to \left({F}\mathrm{shift}0\right)\left({B}\right)={F}\left({B}\right)$
10 8 9 sylan9eq ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({F}\mathrm{shift}{A}\right)\mathrm{shift}\left(-{A}\right)\right)\left({B}\right)={F}\left({B}\right)$