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

Metamath Proof Explorer

Theorem shftfib

Description: Value of a fiber of the relation F . (Contributed by Mario Carneiro, 4-Nov-2013)

Ref Expression
Hypothesis shftfval.1 
|- F e. _V
Assertion shftfib 
|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 1 shftfval 
 |-  ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
3 2 breqd 
 |-  ( A e. CC -> ( B ( F shift A ) z <-> B { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } z ) )
4 eleq1 
 |-  ( x = B -> ( x e. CC <-> B e. CC ) )
5 oveq1 
 |-  ( x = B -> ( x - A ) = ( B - A ) )
6 5 breq1d 
 |-  ( x = B -> ( ( x - A ) F y <-> ( B - A ) F y ) )
7 4 6 anbi12d 
 |-  ( x = B -> ( ( x e. CC /\ ( x - A ) F y ) <-> ( B e. CC /\ ( B - A ) F y ) ) )
8 breq2 
 |-  ( y = z -> ( ( B - A ) F y <-> ( B - A ) F z ) )
9 8 anbi2d 
 |-  ( y = z -> ( ( B e. CC /\ ( B - A ) F y ) <-> ( B e. CC /\ ( B - A ) F z ) ) )
10 eqid 
 |-  { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) }
11 7 9 10 brabg 
 |-  ( ( B e. CC /\ z e. _V ) -> ( B { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } z <-> ( B e. CC /\ ( B - A ) F z ) ) )
12 11 elvd 
 |-  ( B e. CC -> ( B { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } z <-> ( B e. CC /\ ( B - A ) F z ) ) )
13 3 12 sylan9bb 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B ( F shift A ) z <-> ( B e. CC /\ ( B - A ) F z ) ) )
14 ibar 
 |-  ( B e. CC -> ( ( B - A ) F z <-> ( B e. CC /\ ( B - A ) F z ) ) )
15 14 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( B - A ) F z <-> ( B e. CC /\ ( B - A ) F z ) ) )
16 13 15 bitr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B ( F shift A ) z <-> ( B - A ) F z ) )
17 16 abbidv 
 |-  ( ( A e. CC /\ B e. CC ) -> { z | B ( F shift A ) z } = { z | ( B - A ) F z } )
18 imasng 
 |-  ( B e. CC -> ( ( F shift A ) " { B } ) = { z | B ( F shift A ) z } )
19 18 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = { z | B ( F shift A ) z } )
20 ovex 
 |-  ( B - A ) e. _V
21 imasng 
 |-  ( ( B - A ) e. _V -> ( F " { ( B - A ) } ) = { z | ( B - A ) F z } )
22 20 21 mp1i 
 |-  ( ( A e. CC /\ B e. CC ) -> ( F " { ( B - A ) } ) = { z | ( B - A ) F z } )
23 17 19 22 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )