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 ∈ ℂ → F shift A shift B = F shift A + B

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 1 shftfval ⊢ A ∈ ℂ → F shift A = z w | z ∈ ℂ ∧ z − A F w
3 2 breqd ⊢ A ∈ ℂ → x − B F shift A y ↔ x − B z w | z ∈ ℂ ∧ z − A F w y
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 − A F w ↔ x - B - A F w
9 6 8 anbi12d ⊢ z = x − B → z ∈ ℂ ∧ z − A F w ↔ x − B ∈ ℂ ∧ x - B - A F w
10 breq2 ⊢ w = y → x - B - A F w ↔ x - B - A F y
11 10 anbi2d ⊢ w = y → x − B ∈ ℂ ∧ x - B - A F w ↔ x − B ∈ ℂ ∧ x - B - A F y
12 eqid ⊢ z w | z ∈ ℂ ∧ z − A F w = z w | z ∈ ℂ ∧ z − A F w
13 4 5 9 11 12 brab ⊢ x − B z w | z ∈ ℂ ∧ z − A F w y ↔ x − B ∈ ℂ ∧ x - B - A F y
14 3 13 bitrdi ⊢ A ∈ ℂ → x − B F shift A y ↔ x − B ∈ ℂ ∧ x - B - A F y
15 14 ad2antrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ x ∈ ℂ → x − B F shift A y ↔ x − B ∈ ℂ ∧ x - B - A F y
16 subcl ⊢ x ∈ ℂ ∧ B ∈ ℂ → x − B ∈ ℂ
17 16 biantrurd ⊢ x ∈ ℂ ∧ B ∈ ℂ → x - B - A F y ↔ x − B ∈ ℂ ∧ x - B - A F y
18 17 ancoms ⊢ B ∈ ℂ ∧ x ∈ ℂ → x - B - A F y ↔ x − B ∈ ℂ ∧ x - B - A F y
19 18 adantll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ x ∈ ℂ → x - B - A F y ↔ x − B ∈ ℂ ∧ x - B - A F y
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 - A F y ↔ x − A + B F y
26 15 19 25 3bitr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ x ∈ ℂ → x − B F shift A y ↔ x − A + B F y
27 26 pm5.32da ⊢ A ∈ ℂ ∧ B ∈ ℂ → x ∈ ℂ ∧ x − B F shift A y ↔ x ∈ ℂ ∧ x − A + B F y
28 27 opabbidv ⊢ A ∈ ℂ ∧ B ∈ ℂ → x y | x ∈ ℂ ∧ x − B F shift A y = x y | x ∈ ℂ ∧ x − A + B F y
29 ovex ⊢ F shift A ∈ V
30 29 shftfval ⊢ B ∈ ℂ → F shift A shift B = x y | x ∈ ℂ ∧ x − B F shift A y
31 30 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A shift B = x y | x ∈ ℂ ∧ x − B F shift A y
32 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
33 1 shftfval ⊢ A + B ∈ ℂ → F shift A + B = x y | x ∈ ℂ ∧ x − A + B F y
34 32 33 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A + B = x y | x ∈ ℂ ∧ x − A + B F y
35 28 31 34 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A shift B = F shift A + B