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 = ( 𝑓 ∈ V , 𝑥 ∈ ℂ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) 𝑓 𝑧 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cshi	⊢ shift
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cc	⊢ ℂ
5		vy	⊢ 𝑦
6		vz	⊢ 𝑧
7	5	cv	⊢ 𝑦
8	7 4	wcel	⊢ 𝑦 ∈ ℂ
9		cmin	⊢ −
10	3	cv	⊢ 𝑥
11	7 10 9	co	⊢ ( 𝑦 − 𝑥 )
12	1	cv	⊢ 𝑓
13	6	cv	⊢ 𝑧
14	11 13 12	wbr	⊢ ( 𝑦 − 𝑥 ) 𝑓 𝑧
15	8 14	wa	⊢ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) 𝑓 𝑧 )
16	15 5 6	copab	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) 𝑓 𝑧 ) }
17	1 3 2 4 16	cmpo	⊢ ( 𝑓 ∈ V , 𝑥 ∈ ℂ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) 𝑓 𝑧 ) } )
18	0 17	wceq	⊢ shift = ( 𝑓 ∈ V , 𝑥 ∈ ℂ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) 𝑓 𝑧 ) } )