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 syl6bb 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