Theorem coe0

Description: The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	coe0	|- ( coeff ` 0p ) = ( NN0 X. { 0 } )

Proof

Step	Hyp	Ref	Expression
1		0cnd	|- ( T. -> 0 e. CC )
2		ssid	|- CC C_ CC
3		ply0	|- ( CC C_ CC -> 0p e. ( Poly ` CC ) )
4	2 3	ax-mp	|- 0p e. ( Poly ` CC )
5		coemulc	|- ( ( 0 e. CC /\ 0p e. ( Poly ` CC ) ) -> ( coeff ` ( ( CC X. { 0 } ) oF x. 0p ) ) = ( ( NN0 X. { 0 } ) oF x. ( coeff ` 0p ) ) )
6	1 4 5	sylancl	|- ( T. -> ( coeff ` ( ( CC X. { 0 } ) oF x. 0p ) ) = ( ( NN0 X. { 0 } ) oF x. ( coeff ` 0p ) ) )
7		cnex	|- CC e. _V
8	7	a1i	|- ( T. -> CC e. _V )
9		plyf	|- ( 0p e. ( Poly ` CC ) -> 0p : CC --> CC )
10	4 9	mp1i	|- ( T. -> 0p : CC --> CC )
11		mul02	|- ( x e. CC -> ( 0 x. x ) = 0 )
12	11	adantl	|- ( ( T. /\ x e. CC ) -> ( 0 x. x ) = 0 )
13	8 10 1 1 12	caofid2	|- ( T. -> ( ( CC X. { 0 } ) oF x. 0p ) = ( CC X. { 0 } ) )
14		df-0p	|- 0p = ( CC X. { 0 } )
15	13 14	eqtr4di	|- ( T. -> ( ( CC X. { 0 } ) oF x. 0p ) = 0p )
16	15	fveq2d	|- ( T. -> ( coeff ` ( ( CC X. { 0 } ) oF x. 0p ) ) = ( coeff ` 0p ) )
17		nn0ex	|- NN0 e. _V
18	17	a1i	|- ( T. -> NN0 e. _V )
19		eqid	|- ( coeff ` 0p ) = ( coeff ` 0p )
20	19	coef3	|- ( 0p e. ( Poly ` CC ) -> ( coeff ` 0p ) : NN0 --> CC )
21	4 20	mp1i	|- ( T. -> ( coeff ` 0p ) : NN0 --> CC )
22	18 21 1 1 12	caofid2	|- ( T. -> ( ( NN0 X. { 0 } ) oF x. ( coeff ` 0p ) ) = ( NN0 X. { 0 } ) )
23	6 16 22	3eqtr3d	|- ( T. -> ( coeff ` 0p ) = ( NN0 X. { 0 } ) )
24	23	mptru	|- ( coeff ` 0p ) = ( NN0 X. { 0 } )