Definition df-shft 7754

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 7759 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 7753	. 2 class shift
2		vg	. . . . 5 set g
3	2	cv 1297	. . . 4 class g
4		vy	. . . . . . . 8 set y
5	4	cv 1297	. . . . . . 7 class y
6		cc 6384	. . . . . . 7 class CC
7	5, 6	wcel 1300	. . . . . 6 wff y e. CC
8		vz	. . . . . . . 8 set z
9	8	cv 1297	. . . . . . 7 class z
10		vx	. . . . . . . . . 10 set x
11	10	cv 1297	. . . . . . . . 9 class x
12		cmin 6445	. . . . . . . . 9 class -
13	5, 11, 12	co 4884	. . . . . . . 8 class (y - x)
14		vf	. . . . . . . . 9 set f
15	14	cv 1297	. . . . . . . 8 class f
16	13, 15	cfv 3998	. . . . . . 7 class (f` (y - x))
17	9, 16	wceq 1298	. . . . . 6 wff z = (f` (y - x))
18	7, 17	wa 240	. . . . 5 wff (y e. CC /\ z = (f` (y - x)))
19	18, 4, 8	copab 3395	. . . 4 class {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}
20	3, 19	wceq 1298	. . 3 wff g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}
21	20, 14, 10, 2	copab2 4885	. 2 class {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}
22	1, 21	wceq 1298	1 wff shift = {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}

This definition is referenced by:  shftfval 7755

Copyright terms: Public domain