Definition df-shft 6341

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 shftvalt 6346 for its value.

Assertion

Ref	Expression
df-shft	|- shift = {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}

Distinct variable group:   x,y,z,f,g

Detailed syntax breakdown of Definition df-shft

Step	Hyp	Ref	Expression
1		cshi 6340	. 2 class shift
2		vg	. . . . 5 set g
3	2	cv 955	. . . 4 class g
4		vy	. . . . . . . 8 set y
5	4	cv 955	. . . . . . 7 class y
6		cc 5232	. . . . . . 7 class CC
7	5, 6	wcel 958	. . . . . 6 wff y e. CC
8		vz	. . . . . . . 8 set z
9	8	cv 955	. . . . . . 7 class z
10		vx	. . . . . . . . . 10 set x
11	10	cv 955	. . . . . . . . 9 class x
12		cmin 5292	. . . . . . . . 9 class -
13	5, 11, 12	co 3963	. . . . . . . 8 class (y - x)
14		vf	. . . . . . . . 9 set f
15	14	cv 955	. . . . . . . 8 class f
16	13, 15	cfv 3182	. . . . . . 7 class (f` (y - x))
17	9, 16	wceq 956	. . . . . 6 wff z = (f` (y - x))
18	7, 17	wa 223	. . . . 5 wff (y e. CC /\ z = (f` (y - x)))
19	18, 4, 8	copab 2666	. . . 4 class {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}
20	3, 19	wceq 956	. . 3 wff g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}
21	20, 14, 10, 2	copab2 3964	. 2 class {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}
22	1, 21	wceq 956	1 wff shift = {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}

This definition is referenced by:  shftfval 6342

Copyright terms: Public domain