This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )