Theorem shftidt

Description: Identity law for the shift operation. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	$$⊢F\in \mathrm{V}$$
Assertion	shftidt	$$⊢A\in ℂ\to \left(F\mathrm{shift}0\right)\left(A\right)=F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	$$⊢F\in \mathrm{V}$$
2	1	shftidt2	$$⊢F\mathrm{shift}0={F\upharpoonright }_{ℂ}$$
3	2	fveq1i	$$⊢\left(F\mathrm{shift}0\right)\left(A\right)=\left({F\upharpoonright }_{ℂ}\right)\left(A\right)$$
4		fvres	$$⊢A\in ℂ\to \left({F\upharpoonright }_{ℂ}\right)\left(A\right)=F\left(A\right)$$
5	3 4	syl5eq	$$⊢A\in ℂ\to \left(F\mathrm{shift}0\right)\left(A\right)=F\left(A\right)$$