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