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 ffvelrn
 |-  ( ( 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 )