Theorem plyid

Description: The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	plyid	|- ( ( S C_ CC /\ 1 e. S ) -> Xp e. ( Poly ` S ) )

Proof

Step	Hyp	Ref	Expression
1		mptresid	|- ( _I |` CC ) = ( z e. CC |-> z )
2		df-idp	|- Xp = ( _I |` CC )
3		exp1	|- ( z e. CC -> ( z ^ 1 ) = z )
4	3	mpteq2ia	|- ( z e. CC |-> ( z ^ 1 ) ) = ( z e. CC |-> z )
5	1 2 4	3eqtr4i	|- Xp = ( z e. CC |-> ( z ^ 1 ) )
6		1nn0	|- 1 e. NN0
7		plypow	|- ( ( S C_ CC /\ 1 e. S /\ 1 e. NN0 ) -> ( z e. CC |-> ( z ^ 1 ) ) e. ( Poly ` S ) )
8	6 7	mp3an3	|- ( ( S C_ CC /\ 1 e. S ) -> ( z e. CC |-> ( z ^ 1 ) ) e. ( Poly ` S ) )
9	5 8	eqeltrid	|- ( ( S C_ CC /\ 1 e. S ) -> Xp e. ( Poly ` S ) )