Definition df-shft 11580

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 11590 for its value. (Contributed by NM, 20-Jul-2005.)

Assertion

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

Distinct variable group:   x, y, z, f

Detailed syntax breakdown of Definition df-shft

Step	Hyp	Ref	Expression
1		cshi 11579	. 2 class shift
2		vf	. . 3 setvar f
3		vx	. . 3 setvar x
4		cvv 2821	. . 3 class _V
5		cc 8177	. . 3 class CC
6		vy	. . . . . . 7 setvar y
7	6	cv 1401	. . . . . 6 class y
8	7, 5	wcel 2209	. . . . 5 wff y e. CC
9	3	cv 1401	. . . . . . 7 class x
10		cmin 8497	. . . . . . 7 class -
11	7, 9, 10	co 6085	. . . . . 6 class ( y - x )
12		vz	. . . . . . 7 setvar z
13	12	cv 1401	. . . . . 6 class z
14	2	cv 1401	. . . . . 6 class f
15	11, 13, 14	wbr 4130	. . . . 5 wff ( y - x ) f z
16	8, 15	wa 104	. . . 4 wff ( y e. CC /\ ( y - x ) f z )
17	16, 6, 12	copab 4191	. . 3 class { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) }
18	2, 3, 4, 5, 17	cmpo 6087	. 2 class ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
19	1, 18	wceq 1402	1 wff shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )

This definition is used by:  shftfvalg  11583  shftfval  11586