# 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}\in \mathrm{V}$
Assertion 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\}$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 relopab ${⊢}\mathrm{Rel}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
3 2 a1i ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \mathrm{Rel}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
4 fnfun ${⊢}{F}Fn{B}\to \mathrm{Fun}{F}$
5 4 adantr ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \mathrm{Fun}{F}$
6 funmo ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}\left({z}-{A}\right){F}{w}$
7 vex ${⊢}{z}\in \mathrm{V}$
8 vex ${⊢}{w}\in \mathrm{V}$
9 eleq1w ${⊢}{x}={z}\to \left({x}\in ℂ↔{z}\in ℂ\right)$
10 oveq1 ${⊢}{x}={z}\to {x}-{A}={z}-{A}$
11 10 breq1d ${⊢}{x}={z}\to \left(\left({x}-{A}\right){F}{y}↔\left({z}-{A}\right){F}{y}\right)$
12 9 11 anbi12d ${⊢}{x}={z}\to \left(\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)↔\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{y}\right)\right)$
13 breq2 ${⊢}{y}={w}\to \left(\left({z}-{A}\right){F}{y}↔\left({z}-{A}\right){F}{w}\right)$
14 13 anbi2d ${⊢}{y}={w}\to \left(\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{y}\right)↔\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)\right)$
15 eqid ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
16 7 8 12 14 15 brab ${⊢}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}↔\left({z}\in ℂ\wedge \left({z}-{A}\right){F}{w}\right)$
17 16 simprbi ${⊢}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}\to \left({z}-{A}\right){F}{w}$
18 17 moimi ${⊢}{\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}\left({z}-{A}\right){F}{w}\to {\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}$
19 6 18 syl ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}$
20 19 alrimiv ${⊢}\mathrm{Fun}{F}\to \forall {z}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}$
21 5 20 syl ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}$
22 dffun6 ${⊢}\mathrm{Fun}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}↔\left(\mathrm{Rel}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{w}\phantom{\rule{.4em}{0ex}}{z}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}{w}\right)$
23 3 21 22 sylanbrc ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \mathrm{Fun}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
24 1 shftfval ${⊢}{A}\in ℂ\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
25 24 adantl ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
26 25 funeqd ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \left(\mathrm{Fun}\left({F}\mathrm{shift}{A}\right)↔\mathrm{Fun}\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\right)$
27 23 26 mpbird ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \mathrm{Fun}\left({F}\mathrm{shift}{A}\right)$
28 1 shftdm ${⊢}{A}\in ℂ\to \mathrm{dom}\left({F}\mathrm{shift}{A}\right)=\left\{{x}\in ℂ|{x}-{A}\in \mathrm{dom}{F}\right\}$
29 fndm ${⊢}{F}Fn{B}\to \mathrm{dom}{F}={B}$
30 29 eleq2d ${⊢}{F}Fn{B}\to \left({x}-{A}\in \mathrm{dom}{F}↔{x}-{A}\in {B}\right)$
31 30 rabbidv ${⊢}{F}Fn{B}\to \left\{{x}\in ℂ|{x}-{A}\in \mathrm{dom}{F}\right\}=\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}$
32 28 31 sylan9eqr ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \mathrm{dom}\left({F}\mathrm{shift}{A}\right)=\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}$
33 df-fn ${⊢}\left({F}\mathrm{shift}{A}\right)Fn\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}↔\left(\mathrm{Fun}\left({F}\mathrm{shift}{A}\right)\wedge \mathrm{dom}\left({F}\mathrm{shift}{A}\right)=\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}\right)$
34 27 32 33 sylanbrc ${⊢}\left({F}Fn{B}\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)Fn\left\{{x}\in ℂ|{x}-{A}\in {B}\right\}$