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∈V
Assertion 2shfti ⊢A∈ℂ∧B∈ℂ→FshiftAshiftB=FshiftA+B

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢F∈V
2 1 shftfval ⊢A∈ℂ→FshiftA=zw|z∈ℂ∧z−AFw
3 2 breqd ⊢A∈ℂ→x−BFshiftAy↔x−Bzw|z∈ℂ∧z−AFwy
4 ovex ⊢x−B∈V
5 vex ⊢y∈V
6 eleq1 ⊢z=x−B→z∈ℂ↔x−B∈ℂ
7 oveq1 ⊢z=x−B→z−A=x-B-A
8 7 breq1d ⊢z=x−B→z−AFw↔x-B-AFw
9 6 8 anbi12d ⊢z=x−B→z∈ℂ∧z−AFw↔x−B∈ℂ∧x-B-AFw
10 breq2 ⊢w=y→x-B-AFw↔x-B-AFy
11 10 anbi2d ⊢w=y→x−B∈ℂ∧x-B-AFw↔x−B∈ℂ∧x-B-AFy
12 eqid ⊢zw|z∈ℂ∧z−AFw=zw|z∈ℂ∧z−AFw
13 4 5 9 11 12 brab ⊢x−Bzw|z∈ℂ∧z−AFwy↔x−B∈ℂ∧x-B-AFy
14 3 13 bitrdi ⊢A∈ℂ→x−BFshiftAy↔x−B∈ℂ∧x-B-AFy
15 14 ad2antrr ⊢A∈ℂ∧B∈ℂ∧x∈ℂ→x−BFshiftAy↔x−B∈ℂ∧x-B-AFy
16 subcl ⊢x∈ℂ∧B∈ℂ→x−B∈ℂ
17 16 biantrurd ⊢x∈ℂ∧B∈ℂ→x-B-AFy↔x−B∈ℂ∧x-B-AFy
18 17 ancoms ⊢B∈ℂ∧x∈ℂ→x-B-AFy↔x−B∈ℂ∧x-B-AFy
19 18 adantll ⊢A∈ℂ∧B∈ℂ∧x∈ℂ→x-B-AFy↔x−B∈ℂ∧x-B-AFy
20 sub32 ⊢x∈ℂ∧A∈ℂ∧B∈ℂ→x-A-B=x-B-A
21 subsub4 ⊢x∈ℂ∧A∈ℂ∧B∈ℂ→x-A-B=x−A+B
22 20 21 eqtr3d ⊢x∈ℂ∧A∈ℂ∧B∈ℂ→x-B-A=x−A+B
23 22 3expb ⊢x∈ℂ∧A∈ℂ∧B∈ℂ→x-B-A=x−A+B
24 23 ancoms ⊢A∈ℂ∧B∈ℂ∧x∈ℂ→x-B-A=x−A+B
25 24 breq1d ⊢A∈ℂ∧B∈ℂ∧x∈ℂ→x-B-AFy↔x−A+BFy
26 15 19 25 3bitr2d ⊢A∈ℂ∧B∈ℂ∧x∈ℂ→x−BFshiftAy↔x−A+BFy
27 26 pm5.32da ⊢A∈ℂ∧B∈ℂ→x∈ℂ∧x−BFshiftAy↔x∈ℂ∧x−A+BFy
28 27 opabbidv ⊢A∈ℂ∧B∈ℂ→xy|x∈ℂ∧x−BFshiftAy=xy|x∈ℂ∧x−A+BFy
29 ovex ⊢FshiftA∈V
30 29 shftfval ⊢B∈ℂ→FshiftAshiftB=xy|x∈ℂ∧x−BFshiftAy
31 30 adantl ⊢A∈ℂ∧B∈ℂ→FshiftAshiftB=xy|x∈ℂ∧x−BFshiftAy
32 addcl ⊢A∈ℂ∧B∈ℂ→A+B∈ℂ
33 1 shftfval ⊢A+B∈ℂ→FshiftA+B=xy|x∈ℂ∧x−A+BFy
34 32 33 syl ⊢A∈ℂ∧B∈ℂ→FshiftA+B=xy|x∈ℂ∧x−A+BFy
35 28 31 34 3eqtr4d ⊢A∈ℂ∧B∈ℂ→FshiftAshiftB=FshiftA+B