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

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 negneg ⊢ A ∈ ℂ → − − A = A
3 2 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → − − A = A
4 3 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift − A shift − − A = F shift − A shift A
5 4 fveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift − A shift − − A ⁡ B = F shift − A shift A ⁡ B
6 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
7 1 shftcan1 ⊢ − A ∈ ℂ ∧ B ∈ ℂ → F shift − A shift − − A ⁡ B = F ⁡ B
8 6 7 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift − A shift − − A ⁡ B = F ⁡ B
9 5 8 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift − A shift A ⁡ B = F ⁡ B