# Metamath Proof Explorer

## Definition df-shft

Description: Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of CC ) and produces a new function on CC . See shftval for its value. (Contributed by NM, 20-Jul-2005)

Ref Expression
Assertion df-shft ${⊢}\mathrm{shift}=\left({f}\in \mathrm{V},{x}\in ℂ⟼\left\{⟨{y},{z}⟩|\left({y}\in ℂ\wedge \left({y}-{x}\right){f}{z}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cshi ${class}\mathrm{shift}$
1 vf ${setvar}{f}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cc ${class}ℂ$
5 vy ${setvar}{y}$
6 vz ${setvar}{z}$
7 5 cv ${setvar}{y}$
8 7 4 wcel ${wff}{y}\in ℂ$
9 cmin ${class}-$
10 3 cv ${setvar}{x}$
11 7 10 9 co ${class}\left({y}-{x}\right)$
12 1 cv ${setvar}{f}$
13 6 cv ${setvar}{z}$
14 11 13 12 wbr ${wff}\left({y}-{x}\right){f}{z}$
15 8 14 wa ${wff}\left({y}\in ℂ\wedge \left({y}-{x}\right){f}{z}\right)$
16 15 5 6 copab ${class}\left\{⟨{y},{z}⟩|\left({y}\in ℂ\wedge \left({y}-{x}\right){f}{z}\right)\right\}$
17 1 3 2 4 16 cmpo ${class}\left({f}\in \mathrm{V},{x}\in ℂ⟼\left\{⟨{y},{z}⟩|\left({y}\in ℂ\wedge \left({y}-{x}\right){f}{z}\right)\right\}\right)$
18 0 17 wceq ${wff}\mathrm{shift}=\left({f}\in \mathrm{V},{x}\in ℂ⟼\left\{⟨{y},{z}⟩|\left({y}\in ℂ\wedge \left({y}-{x}\right){f}{z}\right)\right\}\right)$