Metamath Proof Explorer

Theorem idpfv

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

Ref Expression
Assertion idpfv 
|- ( A e. CC -> ( Xp ` A ) = A )

Proof

Step Hyp Ref Expression
1 df-idp 
 |-  Xp = ( _I |` CC )
2 1 fveq1i 
 |-  ( Xp ` A ) = ( ( _I |` CC ) ` A )
3 fvresi 
 |-  ( A e. CC -> ( ( _I |` CC ) ` A ) = A )
4 2 3 eqtrid 
 |-  ( A e. CC -> ( Xp ` A ) = A )