# 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}\in \mathrm{V}$
Assertion shftf ${⊢}\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right):\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}⟶{C}$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 ffn ${⊢}{F}:{B}⟶{C}\to {F}Fn{B}$
3 1 shftfn ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)Fn\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}$
4 2 3 sylan ${⊢}\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)Fn\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}$
5 oveq1 ${⊢}{x}={y}\to {x}-{A}={y}-{A}$
6 5 eleq1d ${⊢}{x}={y}\to \left({x}-{A}\in {B}↔{y}-{A}\in {B}\right)$
7 6 elrab ${⊢}{y}\in \left\{{x}\in ℂ|{x}-{A}\in {B}\right\}↔\left({y}\in ℂ\wedge {y}-{A}\in {B}\right)$
8 simpr ${⊢}\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\to {A}\in ℂ$
9 simpl ${⊢}\left({y}\in ℂ\wedge {y}-{A}\in {B}\right)\to {y}\in ℂ$
10 1 shftval ${⊢}\left({A}\in ℂ\wedge {y}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left({y}\right)={F}\left({y}-{A}\right)$
11 8 9 10 syl2an ${⊢}\left(\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\wedge \left({y}\in ℂ\wedge {y}-{A}\in {B}\right)\right)\to \left({F}\mathrm{shift}{A}\right)\left({y}\right)={F}\left({y}-{A}\right)$
12 simpl ${⊢}\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\to {F}:{B}⟶{C}$
13 simpr ${⊢}\left({y}\in ℂ\wedge {y}-{A}\in {B}\right)\to {y}-{A}\in {B}$
14 ffvelrn ${⊢}\left({F}:{B}⟶{C}\wedge {y}-{A}\in {B}\right)\to {F}\left({y}-{A}\right)\in {C}$
15 12 13 14 syl2an ${⊢}\left(\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\wedge \left({y}\in ℂ\wedge {y}-{A}\in {B}\right)\right)\to {F}\left({y}-{A}\right)\in {C}$
16 11 15 eqeltrd ${⊢}\left(\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\wedge \left({y}\in ℂ\wedge {y}-{A}\in {B}\right)\right)\to \left({F}\mathrm{shift}{A}\right)\left({y}\right)\in {C}$
17 7 16 sylan2b ${⊢}\left(\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\wedge {y}\in \left\{{x}\in ℂ|{x}-{A}\in {B}\right\}\right)\to \left({F}\mathrm{shift}{A}\right)\left({y}\right)\in {C}$
18 17 ralrimiva ${⊢}\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\to \forall {y}\in \left\{{x}\in ℂ|{x}-{A}\in {B}\right\}\phantom{\rule{.4em}{0ex}}\left({F}\mathrm{shift}{A}\right)\left({y}\right)\in {C}$
19 ffnfv ${⊢}\left({F}\mathrm{shift}{A}\right):\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}⟶{C}↔\left(\left({F}\mathrm{shift}{A}\right)Fn\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}\wedge \forall {y}\in \left\{{x}\in ℂ|{x}-{A}\in {B}\right\}\phantom{\rule{.4em}{0ex}}\left({F}\mathrm{shift}{A}\right)\left({y}\right)\in {C}\right)$
20 4 18 19 sylanbrc ${⊢}\left({F}:{B}⟶{C}\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right):\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}⟶{C}$