Definition df-shft 10587

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

Assertion

Ref	Expression
df-shft	⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})

Distinct variable group:   𝑥,𝑦,𝑧,𝑓

Detailed syntax breakdown of Definition df-shft

Step	Hyp	Ref	Expression
1		cshi 10586	. 2 class shift
2		vf	. . 3 setvar 𝑓
3		vx	. . 3 setvar 𝑥
4		cvv 2686	. . 3 class V
5		cc 7618	. . 3 class ℂ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1330	. . . . . 6 class 𝑦
8	7, 5	wcel 1480	. . . . 5 wff 𝑦 ∈ ℂ
9	3	cv 1330	. . . . . . 7 class 𝑥
10		cmin 7933	. . . . . . 7 class −
11	7, 9, 10	co 5774	. . . . . 6 class (𝑦 − 𝑥)
12		vz	. . . . . . 7 setvar 𝑧
13	12	cv 1330	. . . . . 6 class 𝑧
14	2	cv 1330	. . . . . 6 class 𝑓
15	11, 13, 14	wbr 3929	. . . . 5 wff (𝑦 − 𝑥)𝑓𝑧
16	8, 15	wa 103	. . . 4 wff (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)
17	16, 6, 12	copab 3988	. . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}
18	2, 3, 4, 5, 17	cmpo 5776	. 2 class (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})
19	1, 18	wceq 1331	1 wff shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})

This definition is referenced by:  shftfvalg  10590  shftfval  10593