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