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