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 ∈ V
Assertion shftcan1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A shift − A ⁡ B = F ⁡ B

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
3 1 2shfti ⊢ A ∈ ℂ ∧ − A ∈ ℂ → F shift A shift − A = F shift A + − A
4 2 3 mpdan ⊢ A ∈ ℂ → F shift A shift − A = F shift A + − A
5 negid ⊢ A ∈ ℂ → A + − A = 0
6 5 oveq2d ⊢ A ∈ ℂ → F shift A + − A = F shift 0
7 4 6 eqtrd ⊢ A ∈ ℂ → F shift A shift − A = F shift 0
8 7 fveq1d ⊢ A ∈ ℂ → F shift A shift − A ⁡ B = F shift 0 ⁡ B
9 1 shftidt ⊢ B ∈ ℂ → F shift 0 ⁡ B = F ⁡ B
10 8 9 sylan9eq ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A shift − A ⁡ B = F ⁡ B