Metamath Proof Explorer

Theorem shftfn

Description: Functionality and domain of a sequence shifted by A . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 
|- F e. _V
Assertion shftfn 
|- ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 relopabv 
 |-  Rel { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) }
3 2 a1i 
 |-  ( ( F Fn B /\ A e. CC ) -> Rel { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
4 fnfun 
 |-  ( F Fn B -> Fun F )
5 4 adantr 
 |-  ( ( F Fn B /\ A e. CC ) -> Fun F )
6 funmo 
 |-  ( Fun F -> E* w ( z - A ) F w )
7 vex 
 |-  z e. _V
8 vex 
 |-  w e. _V
9 eleq1w 
 |-  ( x = z -> ( x e. CC <-> z e. CC ) )
10 oveq1 
 |-  ( x = z -> ( x - A ) = ( z - A ) )
11 10 breq1d 
 |-  ( x = z -> ( ( x - A ) F y <-> ( z - A ) F y ) )
12 9 11 anbi12d 
 |-  ( x = z -> ( ( x e. CC /\ ( x - A ) F y ) <-> ( z e. CC /\ ( z - A ) F y ) ) )
13 breq2 
 |-  ( y = w -> ( ( z - A ) F y <-> ( z - A ) F w ) )
14 13 anbi2d 
 |-  ( y = w -> ( ( z e. CC /\ ( z - A ) F y ) <-> ( z e. CC /\ ( z - A ) F w ) ) )
15 eqid 
 |-  { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) }
16 7 8 12 14 15 brab 
 |-  ( z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w <-> ( z e. CC /\ ( z - A ) F w ) )
17 16 simprbi 
 |-  ( z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w -> ( z - A ) F w )
18 17 moimi 
 |-  ( E* w ( z - A ) F w -> E* w z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w )
19 6 18 syl 
 |-  ( Fun F -> E* w z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w )
20 19 alrimiv 
 |-  ( Fun F -> A. z E* w z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w )
21 5 20 syl 
 |-  ( ( F Fn B /\ A e. CC ) -> A. z E* w z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w )
22 dffun6 
 |-  ( Fun { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } <-> ( Rel { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } /\ A. z E* w z { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } w ) )
23 3 21 22 sylanbrc 
 |-  ( ( F Fn B /\ A e. CC ) -> Fun { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
24 1 shftfval 
 |-  ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
25 24 adantl 
 |-  ( ( F Fn B /\ A e. CC ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
26 25 funeqd 
 |-  ( ( F Fn B /\ A e. CC ) -> ( Fun ( F shift A ) <-> Fun { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) )
27 23 26 mpbird 
 |-  ( ( F Fn B /\ A e. CC ) -> Fun ( F shift A ) )
28 1 shftdm 
 |-  ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } )
29 fndm 
 |-  ( F Fn B -> dom F = B )
30 29 eleq2d 
 |-  ( F Fn B -> ( ( x - A ) e. dom F <-> ( x - A ) e. B ) )
31 30 rabbidv 
 |-  ( F Fn B -> { x e. CC | ( x - A ) e. dom F } = { x e. CC | ( x - A ) e. B } )
32 28 31 sylan9eqr 
 |-  ( ( F Fn B /\ A e. CC ) -> dom ( F shift A ) = { x e. CC | ( x - A ) e. B } )
33 df-fn 
 |-  ( ( F shift A ) Fn { x e. CC | ( x - A ) e. B } <-> ( Fun ( F shift A ) /\ dom ( F shift A ) = { x e. CC | ( x - A ) e. B } ) )
34 27 32 33 sylanbrc 
 |-  ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )