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 e. _V
Assertion 2shfti
|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) shift B ) = ( F shift ( A + B ) ) )

Proof

Step Hyp Ref Expression
1 shftfval.1
 |-  F e. _V
2 1 shftfval
 |-  ( A e. CC -> ( F shift A ) = { <. z , w >. | ( z e. CC /\ ( z - A ) F w ) } )
3 2 breqd
 |-  ( A e. CC -> ( ( x - B ) ( F shift A ) y <-> ( x - B ) { <. z , w >. | ( z e. CC /\ ( z - A ) F w ) } y ) )
4 ovex
 |-  ( x - B ) e. _V
5 vex
 |-  y e. _V
6 eleq1
 |-  ( z = ( x - B ) -> ( z e. CC <-> ( x - B ) e. CC ) )
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 e. CC /\ ( z - A ) F w ) <-> ( ( x - B ) e. CC /\ ( ( 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 ) e. CC /\ ( ( x - B ) - A ) F w ) <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) ) )
12 eqid
 |-  { <. z , w >. | ( z e. CC /\ ( z - A ) F w ) } = { <. z , w >. | ( z e. CC /\ ( z - A ) F w ) }
13 4 5 9 11 12 brab
 |-  ( ( x - B ) { <. z , w >. | ( z e. CC /\ ( z - A ) F w ) } y <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) )
14 3 13 bitrdi
 |-  ( A e. CC -> ( ( x - B ) ( F shift A ) y <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) ) )
15 14 ad2antrr
 |-  ( ( ( A e. CC /\ B e. CC ) /\ x e. CC ) -> ( ( x - B ) ( F shift A ) y <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) ) )
16 subcl
 |-  ( ( x e. CC /\ B e. CC ) -> ( x - B ) e. CC )
17 16 biantrurd
 |-  ( ( x e. CC /\ B e. CC ) -> ( ( ( x - B ) - A ) F y <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) ) )
18 17 ancoms
 |-  ( ( B e. CC /\ x e. CC ) -> ( ( ( x - B ) - A ) F y <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) ) )
19 18 adantll
 |-  ( ( ( A e. CC /\ B e. CC ) /\ x e. CC ) -> ( ( ( x - B ) - A ) F y <-> ( ( x - B ) e. CC /\ ( ( x - B ) - A ) F y ) ) )
20 sub32
 |-  ( ( x e. CC /\ A e. CC /\ B e. CC ) -> ( ( x - A ) - B ) = ( ( x - B ) - A ) )
21 subsub4
 |-  ( ( x e. CC /\ A e. CC /\ B e. CC ) -> ( ( x - A ) - B ) = ( x - ( A + B ) ) )
22 20 21 eqtr3d
 |-  ( ( x e. CC /\ A e. CC /\ B e. CC ) -> ( ( x - B ) - A ) = ( x - ( A + B ) ) )
23 22 3expb
 |-  ( ( x e. CC /\ ( A e. CC /\ B e. CC ) ) -> ( ( x - B ) - A ) = ( x - ( A + B ) ) )
24 23 ancoms
 |-  ( ( ( A e. CC /\ B e. CC ) /\ x e. CC ) -> ( ( x - B ) - A ) = ( x - ( A + B ) ) )
25 24 breq1d
 |-  ( ( ( A e. CC /\ B e. CC ) /\ x e. CC ) -> ( ( ( x - B ) - A ) F y <-> ( x - ( A + B ) ) F y ) )
26 15 19 25 3bitr2d
 |-  ( ( ( A e. CC /\ B e. CC ) /\ x e. CC ) -> ( ( x - B ) ( F shift A ) y <-> ( x - ( A + B ) ) F y ) )
27 26 pm5.32da
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( x e. CC /\ ( x - B ) ( F shift A ) y ) <-> ( x e. CC /\ ( x - ( A + B ) ) F y ) ) )
28 27 opabbidv
 |-  ( ( A e. CC /\ B e. CC ) -> { <. x , y >. | ( x e. CC /\ ( x - B ) ( F shift A ) y ) } = { <. x , y >. | ( x e. CC /\ ( x - ( A + B ) ) F y ) } )
29 ovex
 |-  ( F shift A ) e. _V
30 29 shftfval
 |-  ( B e. CC -> ( ( F shift A ) shift B ) = { <. x , y >. | ( x e. CC /\ ( x - B ) ( F shift A ) y ) } )
31 30 adantl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) shift B ) = { <. x , y >. | ( x e. CC /\ ( x - B ) ( F shift A ) y ) } )
32 addcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
33 1 shftfval
 |-  ( ( A + B ) e. CC -> ( F shift ( A + B ) ) = { <. x , y >. | ( x e. CC /\ ( x - ( A + B ) ) F y ) } )
34 32 33 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( F shift ( A + B ) ) = { <. x , y >. | ( x e. CC /\ ( x - ( A + B ) ) F y ) } )
35 28 31 34 3eqtr4d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) shift B ) = ( F shift ( A + B ) ) )