Theorem idpfv

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

	Ref	Expression
Assertion	idpfv	⊢ ( 𝐴 ∈ ℂ → ( Xp ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-idp	⊢ Xp = ( I ↾ ℂ )
2	1	fveq1i	⊢ ( Xp ‘ 𝐴 ) = ( ( I ↾ ℂ ) ‘ 𝐴 )
3		fvresi	⊢ ( 𝐴 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝐴 ) = 𝐴 )
4	2 3	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( Xp ‘ 𝐴 ) = 𝐴 )