Metamath Proof Explorer

Theorem shftf

Description: Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 ffn 
 |-  ( F : B --> C -> F Fn B )
3 1 shftfn 
 |-  ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )
4 2 3 sylan 
 |-  ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )
5 oveq1 
 |-  ( x = y -> ( x - A ) = ( y - A ) )
6 5 eleq1d 
 |-  ( x = y -> ( ( x - A ) e. B <-> ( y - A ) e. B ) )
7 6 elrab 
 |-  ( y e. { x e. CC | ( x - A ) e. B } <-> ( y e. CC /\ ( y - A ) e. B ) )
8 simpr 
 |-  ( ( F : B --> C /\ A e. CC ) -> A e. CC )
9 simpl 
 |-  ( ( y e. CC /\ ( y - A ) e. B ) -> y e. CC )
10 1 shftval 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( F shift A ) ` y ) = ( F ` ( y - A ) ) )
11 8 9 10 syl2an 
 |-  ( ( ( F : B --> C /\ A e. CC ) /\ ( y e. CC /\ ( y - A ) e. B ) ) -> ( ( F shift A ) ` y ) = ( F ` ( y - A ) ) )
12 simpl 
 |-  ( ( F : B --> C /\ A e. CC ) -> F : B --> C )
13 simpr 
 |-  ( ( y e. CC /\ ( y - A ) e. B ) -> ( y - A ) e. B )
14 ffvelcdm 
 |-  ( ( F : B --> C /\ ( y - A ) e. B ) -> ( F ` ( y - A ) ) e. C )
15 12 13 14 syl2an 
 |-  ( ( ( F : B --> C /\ A e. CC ) /\ ( y e. CC /\ ( y - A ) e. B ) ) -> ( F ` ( y - A ) ) e. C )
16 11 15 eqeltrd 
 |-  ( ( ( F : B --> C /\ A e. CC ) /\ ( y e. CC /\ ( y - A ) e. B ) ) -> ( ( F shift A ) ` y ) e. C )
17 7 16 sylan2b 
 |-  ( ( ( F : B --> C /\ A e. CC ) /\ y e. { x e. CC | ( x - A ) e. B } ) -> ( ( F shift A ) ` y ) e. C )
18 17 ralrimiva 
 |-  ( ( F : B --> C /\ A e. CC ) -> A. y e. { x e. CC | ( x - A ) e. B } ( ( F shift A ) ` y ) e. C )
19 ffnfv 
 |-  ( ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C <-> ( ( F shift A ) Fn { x e. CC | ( x - A ) e. B } /\ A. y e. { x e. CC | ( x - A ) e. B } ( ( F shift A ) ` y ) e. C ) )
20 4 18 19 sylanbrc 
 |-  ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C )