# Metamath Proof Explorer

## Theorem shftfval

Description: The value of the sequence shifter operation is a function on CC . A is ordinarily an integer. (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis shftfval.1 ${⊢}{F}\in \mathrm{V}$
Assertion shftfval ${⊢}{A}\in ℂ\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 ovex ${⊢}{x}-{A}\in \mathrm{V}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 2 3 breldm ${⊢}\left({x}-{A}\right){F}{y}\to {x}-{A}\in \mathrm{dom}{F}$
5 npcan ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\right)\to {x}-{A}+{A}={x}$
6 5 eqcomd ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\right)\to {x}={x}-{A}+{A}$
7 6 ancoms ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\right)\to {x}={x}-{A}+{A}$
8 oveq1 ${⊢}{w}={x}-{A}\to {w}+{A}={x}-{A}+{A}$
9 8 rspceeqv ${⊢}\left({x}-{A}\in \mathrm{dom}{F}\wedge {x}={x}-{A}+{A}\right)\to \exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{x}={w}+{A}$
10 4 7 9 syl2anr ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℂ\right)\wedge \left({x}-{A}\right){F}{y}\right)\to \exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{x}={w}+{A}$
11 vex ${⊢}{x}\in \mathrm{V}$
12 eqeq1 ${⊢}{z}={x}\to \left({z}={w}+{A}↔{x}={w}+{A}\right)$
13 12 rexbidv ${⊢}{z}={x}\to \left(\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}↔\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{x}={w}+{A}\right)$
14 11 13 elab ${⊢}{x}\in \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}↔\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{x}={w}+{A}$
15 10 14 sylibr ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℂ\right)\wedge \left({x}-{A}\right){F}{y}\right)\to {x}\in \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}$
16 2 3 brelrn ${⊢}\left({x}-{A}\right){F}{y}\to {y}\in \mathrm{ran}{F}$
17 16 adantl ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℂ\right)\wedge \left({x}-{A}\right){F}{y}\right)\to {y}\in \mathrm{ran}{F}$
18 15 17 jca ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℂ\right)\wedge \left({x}-{A}\right){F}{y}\right)\to \left({x}\in \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}\wedge {y}\in \mathrm{ran}{F}\right)$
19 18 expl ${⊢}{A}\in ℂ\to \left(\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\to \left({x}\in \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}\wedge {y}\in \mathrm{ran}{F}\right)\right)$
20 19 ssopab2dv ${⊢}{A}\in ℂ\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\subseteq \left\{⟨{x},{y}⟩|\left({x}\in \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}\wedge {y}\in \mathrm{ran}{F}\right)\right\}$
21 df-xp ${⊢}\left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}×\mathrm{ran}{F}=\left\{⟨{x},{y}⟩|\left({x}\in \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}\wedge {y}\in \mathrm{ran}{F}\right)\right\}$
22 20 21 sseqtrrdi ${⊢}{A}\in ℂ\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\subseteq \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}×\mathrm{ran}{F}$
23 1 dmex ${⊢}\mathrm{dom}{F}\in \mathrm{V}$
24 23 abrexex ${⊢}\left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}\in \mathrm{V}$
25 1 rnex ${⊢}\mathrm{ran}{F}\in \mathrm{V}$
26 24 25 xpex ${⊢}\left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}×\mathrm{ran}{F}\in \mathrm{V}$
27 ssexg ${⊢}\left(\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\subseteq \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}×\mathrm{ran}{F}\wedge \left\{{z}|\exists {w}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{z}={w}+{A}\right\}×\mathrm{ran}{F}\in \mathrm{V}\right)\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\in \mathrm{V}$
28 22 26 27 sylancl ${⊢}{A}\in ℂ\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\in \mathrm{V}$
29 breq ${⊢}{z}={F}\to \left(\left({x}-{w}\right){z}{y}↔\left({x}-{w}\right){F}{y}\right)$
30 29 anbi2d ${⊢}{z}={F}\to \left(\left({x}\in ℂ\wedge \left({x}-{w}\right){z}{y}\right)↔\left({x}\in ℂ\wedge \left({x}-{w}\right){F}{y}\right)\right)$
31 30 opabbidv ${⊢}{z}={F}\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{w}\right){z}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{w}\right){F}{y}\right)\right\}$
32 oveq2 ${⊢}{w}={A}\to {x}-{w}={x}-{A}$
33 32 breq1d ${⊢}{w}={A}\to \left(\left({x}-{w}\right){F}{y}↔\left({x}-{A}\right){F}{y}\right)$
34 33 anbi2d ${⊢}{w}={A}\to \left(\left({x}\in ℂ\wedge \left({x}-{w}\right){F}{y}\right)↔\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right)$
35 34 opabbidv ${⊢}{w}={A}\to \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{w}\right){F}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
36 df-shft ${⊢}\mathrm{shift}=\left({z}\in \mathrm{V},{w}\in ℂ⟼\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{w}\right){z}{y}\right)\right\}\right)$
37 31 35 36 ovmpog ${⊢}\left({F}\in \mathrm{V}\wedge {A}\in ℂ\wedge \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\in \mathrm{V}\right)\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
38 1 37 mp3an1 ${⊢}\left({A}\in ℂ\wedge \left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}\in \mathrm{V}\right)\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$
39 28 38 mpdan ${⊢}{A}\in ℂ\to {F}\mathrm{shift}{A}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge \left({x}-{A}\right){F}{y}\right)\right\}$