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 ⊢ shift = f ∈ V , x ∈ ℂ ⟼ y z | y ∈ ℂ ∧ y − x f z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cshi class shift
1 vf setvar f
2 cvv class 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 ∈ ℂ
9 cmin class −
10 3 cv setvar x
11 7 10 9 co class y − x
12 1 cv setvar f
13 6 cv setvar z
14 11 13 12 wbr wff y − x f z
15 8 14 wa wff y ∈ ℂ ∧ y − x f z
16 15 5 6 copab class y z | y ∈ ℂ ∧ y − x f z
17 1 3 2 4 16 cmpo class f ∈ V , x ∈ ℂ ⟼ y z | y ∈ ℂ ∧ y − x f z
18 0 17 wceq wff shift = f ∈ V , x ∈ ℂ ⟼ y z | y ∈ ℂ ∧ y − x f z