# Metamath Proof Explorer

## Theorem 2shfti

Description: Composite shift operations. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

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

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 1 shftfval ${⊢}{A}\in ℂ\to {F}\mathrm{shift}{A}=\left\{⟨{z},{w}⟩|\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)\right\}$
3 2 breqd ${⊢}{A}\in ℂ\to \left(\left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}↔\left({x}-{B}\right)\left\{⟨{z},{w}⟩|\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)\right\}{y}\right)$
4 ovex ${⊢}{x}-{B}\in \mathrm{V}$
5 vex ${⊢}{y}\in \mathrm{V}$
6 eleq1 ${⊢}{z}={x}-{B}\to \left({z}\in ℂ↔{x}-{B}\in ℂ\right)$
7 oveq1 ${⊢}{z}={x}-{B}\to {z}-{A}={x}-{B}-{A}$
8 7 breq1d ${⊢}{z}={x}-{B}\to \left(\left({z}-{A}\right){F}{w}↔\left({x}-{B}-{A}\right){F}{w}\right)$
9 6 8 anbi12d ${⊢}{z}={x}-{B}\to \left(\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{w}\right)\right)$
10 breq2 ${⊢}{w}={y}\to \left(\left({x}-{B}-{A}\right){F}{w}↔\left({x}-{B}-{A}\right){F}{y}\right)$
11 10 anbi2d ${⊢}{w}={y}\to \left(\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{w}\right)↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)\right)$
12 eqid ${⊢}\left\{⟨{z},{w}⟩|\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)\right\}=\left\{⟨{z},{w}⟩|\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)\right\}$
13 4 5 9 11 12 brab ${⊢}\left({x}-{B}\right)\left\{⟨{z},{w}⟩|\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)\right\}{y}↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)$
14 3 13 syl6bb ${⊢}{A}\in ℂ\to \left(\left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)\right)$
15 14 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {x}\in ℂ\right)\to \left(\left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)\right)$
16 subcl ${⊢}\left({x}\in ℂ\wedge {B}\in ℂ\right)\to {x}-{B}\in ℂ$
17 16 biantrurd ${⊢}\left({x}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({x}-{B}-{A}\right){F}{y}↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)\right)$
18 17 ancoms ${⊢}\left({B}\in ℂ\wedge {x}\in ℂ\right)\to \left(\left({x}-{B}-{A}\right){F}{y}↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)\right)$
19 18 adantll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {x}\in ℂ\right)\to \left(\left({x}-{B}-{A}\right){F}{y}↔\left({x}-{B}\in ℂ\wedge \left({x}-{B}-{A}\right){F}{y}\right)\right)$
20 sub32 ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℂ\right)\to {x}-{A}-{B}={x}-{B}-{A}$
21 subsub4 ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℂ\right)\to {x}-{A}-{B}={x}-\left({A}+{B}\right)$
22 20 21 eqtr3d ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℂ\right)\to {x}-{B}-{A}={x}-\left({A}+{B}\right)$
23 22 3expb ${⊢}\left({x}\in ℂ\wedge \left({A}\in ℂ\wedge {B}\in ℂ\right)\right)\to {x}-{B}-{A}={x}-\left({A}+{B}\right)$
24 23 ancoms ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {x}\in ℂ\right)\to {x}-{B}-{A}={x}-\left({A}+{B}\right)$
25 24 breq1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {x}\in ℂ\right)\to \left(\left({x}-{B}-{A}\right){F}{y}↔\left({x}-\left({A}+{B}\right)\right){F}{y}\right)$
26 15 19 25 3bitr2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {x}\in ℂ\right)\to \left(\left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}↔\left({x}-\left({A}+{B}\right)\right){F}{y}\right)$
27 26 pm5.32da ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({x}\in ℂ\wedge \left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}\right)↔\left({x}\in ℂ\wedge \left({x}-\left({A}+{B}\right)\right){F}{y}\right)\right)$
28 27 opabbidv ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-\left({A}+{B}\right)\right){F}{y}\right)\right\}$
29 ovex ${⊢}{F}\mathrm{shift}{A}\in \mathrm{V}$
30 29 shftfval ${⊢}{B}\in ℂ\to \left({F}\mathrm{shift}{A}\right)\mathrm{shift}{B}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}\right)\right\}$
31 30 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\mathrm{shift}{B}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{B}\right)\left({F}\mathrm{shift}{A}\right){y}\right)\right\}$
32 addcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}\in ℂ$
33 1 shftfval ${⊢}{A}+{B}\in ℂ\to {F}\mathrm{shift}\left({A}+{B}\right)=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-\left({A}+{B}\right)\right){F}{y}\right)\right\}$
34 32 33 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {F}\mathrm{shift}\left({A}+{B}\right)=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-\left({A}+{B}\right)\right){F}{y}\right)\right\}$
35 28 31 34 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\mathrm{shift}{B}={F}\mathrm{shift}\left({A}+{B}\right)$