This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shft2rab

Description: If B is a shift of A by C , then A is a shift of B by -u C . (Contributed by Mario Carneiro, 22-Mar-2014) (Revised by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses ovolshft.1 
|- ( ph -> A C_ RR )
ovolshft.2 
|- ( ph -> C e. RR )
ovolshft.3 
|- ( ph -> B = { x e. RR | ( x - C ) e. A } )
Assertion shft2rab 
|- ( ph -> A = { y e. RR | ( y - -u C ) e. B } )

Proof

Step Hyp Ref Expression
1 ovolshft.1 
 |-  ( ph -> A C_ RR )
2 ovolshft.2 
 |-  ( ph -> C e. RR )
3 ovolshft.3 
 |-  ( ph -> B = { x e. RR | ( x - C ) e. A } )
4 1 sseld 
 |-  ( ph -> ( y e. A -> y e. RR ) )
5 4 pm4.71rd 
 |-  ( ph -> ( y e. A <-> ( y e. RR /\ y e. A ) ) )
6 recn 
 |-  ( y e. RR -> y e. CC )
7 2 recnd 
 |-  ( ph -> C e. CC )
8 subneg 
 |-  ( ( y e. CC /\ C e. CC ) -> ( y - -u C ) = ( y + C ) )
9 6 7 8 syl2anr 
 |-  ( ( ph /\ y e. RR ) -> ( y - -u C ) = ( y + C ) )
10 3 adantr 
 |-  ( ( ph /\ y e. RR ) -> B = { x e. RR | ( x - C ) e. A } )
11 9 10 eleq12d 
 |-  ( ( ph /\ y e. RR ) -> ( ( y - -u C ) e. B <-> ( y + C ) e. { x e. RR | ( x - C ) e. A } ) )
12 id 
 |-  ( y e. RR -> y e. RR )
13 readdcl 
 |-  ( ( y e. RR /\ C e. RR ) -> ( y + C ) e. RR )
14 12 2 13 syl2anr 
 |-  ( ( ph /\ y e. RR ) -> ( y + C ) e. RR )
15 oveq1 
 |-  ( x = ( y + C ) -> ( x - C ) = ( ( y + C ) - C ) )
16 15 eleq1d 
 |-  ( x = ( y + C ) -> ( ( x - C ) e. A <-> ( ( y + C ) - C ) e. A ) )
17 16 elrab3 
 |-  ( ( y + C ) e. RR -> ( ( y + C ) e. { x e. RR | ( x - C ) e. A } <-> ( ( y + C ) - C ) e. A ) )
18 14 17 syl 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + C ) e. { x e. RR | ( x - C ) e. A } <-> ( ( y + C ) - C ) e. A ) )
19 pncan 
 |-  ( ( y e. CC /\ C e. CC ) -> ( ( y + C ) - C ) = y )
20 6 7 19 syl2anr 
 |-  ( ( ph /\ y e. RR ) -> ( ( y + C ) - C ) = y )
21 20 eleq1d 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( y + C ) - C ) e. A <-> y e. A ) )
22 11 18 21 3bitrd 
 |-  ( ( ph /\ y e. RR ) -> ( ( y - -u C ) e. B <-> y e. A ) )
23 22 pm5.32da 
 |-  ( ph -> ( ( y e. RR /\ ( y - -u C ) e. B ) <-> ( y e. RR /\ y e. A ) ) )
24 5 23 bitr4d 
 |-  ( ph -> ( y e. A <-> ( y e. RR /\ ( y - -u C ) e. B ) ) )
25 24 eqabdv 
 |-  ( ph -> A = { y | ( y e. RR /\ ( y - -u C ) e. B ) } )
26 df-rab 
 |-  { y e. RR | ( y - -u C ) e. B } = { y | ( y e. RR /\ ( y - -u C ) e. B ) }
27 25 26 eqtr4di 
 |-  ( ph -> A = { y e. RR | ( y - -u C ) e. B } )