Theorem plyconst

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

	Ref	Expression
Assertion	plyconst	|- ( ( S C_ CC /\ A e. S ) -> ( CC X. { A } ) e. ( Poly ` S ) )

Proof

Step	Hyp	Ref	Expression
1		exp0	|- ( z e. CC -> ( z ^ 0 ) = 1 )
2	1	adantl	|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( z ^ 0 ) = 1 )
3	2	oveq2d	|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = ( A x. 1 ) )
4		ssel2	|- ( ( S C_ CC /\ A e. S ) -> A e. CC )
5	4	adantr	|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> A e. CC )
6	5	mulid1d	|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. 1 ) = A )
7	3 6	eqtrd	|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = A )
8	7	mpteq2dva	|- ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( z e. CC |-> A ) )
9		fconstmpt	|- ( CC X. { A } ) = ( z e. CC |-> A )
10	8 9	eqtr4di	|- ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( CC X. { A } ) )
11		0nn0	|- 0 e. NN0
12		eqid	|- ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( z e. CC |-> ( A x. ( z ^ 0 ) ) )
13	12	ply1term	|- ( ( S C_ CC /\ A e. S /\ 0 e. NN0 ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) e. ( Poly ` S ) )
14	11 13	mp3an3	|- ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) e. ( Poly ` S ) )
15	10 14	eqeltrrd	|- ( ( S C_ CC /\ A e. S ) -> ( CC X. { A } ) e. ( Poly ` S ) )