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 e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cshi	|- shift
1		vf	|- f
2		cvv	|- _V
3		vx	|- x
4		cc	|- CC
5		vy	|- y
6		vz	|- z
7	5	cv	|- y
8	7 4	wcel	|- y e. CC
9		cmin	|- -
10	3	cv	|- x
11	7 10 9	co	|- ( y - x )
12	1	cv	|- f
13	6	cv	|- z
14	11 13 12	wbr	|- ( y - x ) f z
15	8 14	wa	|- ( y e. CC /\ ( y - x ) f z )
16	15 5 6	copab	|- { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) }
17	1 3 2 4 16	cmpo	|- ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
18	0 17	wceq	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )