Theorem idpfv

Description: Value of the identity polynomial. (Contributed by SN, 30-Aug-2026)

	Ref	Expression
Assertion	idpfv	$$⊢A\in ℂ\to X^p\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		df-idp	$$⊢X^p={\mathrm{I}\upharpoonright }_{ℂ}$$
2	1	fveq1i	$$⊢X^p\left(A\right)=\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)$$
3		fvresi	$$⊢A\in ℂ\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)=A$$
4	2 3	eqtrid	$$⊢A\in ℂ\to X^p\left(A\right)=A$$