Metamath Proof Explorer

Theorem coe1z

Description: The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses coe1z.p 
|- P = ( Poly1 ` R )
coe1z.z 
|- .0. = ( 0g ` P )
coe1z.y 
|- Y = ( 0g ` R )
Assertion coe1z 
|- ( R e. Ring -> ( coe1 ` .0. ) = ( NN0 X. { Y } ) )

Proof

Step Hyp Ref Expression
1 coe1z.p 
 |-  P = ( Poly1 ` R )
2 coe1z.z 
 |-  .0. = ( 0g ` P )
3 coe1z.y 
 |-  Y = ( 0g ` R )
4 fconst6g 
 |-  ( a e. NN0 -> ( 1o X. { a } ) : 1o --> NN0 )
5 4 adantl 
 |-  ( ( R e. Ring /\ a e. NN0 ) -> ( 1o X. { a } ) : 1o --> NN0 )
6 nn0ex 
 |-  NN0 e. _V
7 1oex 
 |-  1o e. _V
8 6 7 elmap 
 |-  ( ( 1o X. { a } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { a } ) : 1o --> NN0 )
9 5 8 sylibr 
 |-  ( ( R e. Ring /\ a e. NN0 ) -> ( 1o X. { a } ) e. ( NN0 ^m 1o ) )
10 eqidd 
 |-  ( R e. Ring -> ( a e. NN0 |-> ( 1o X. { a } ) ) = ( a e. NN0 |-> ( 1o X. { a } ) ) )
11 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
12 psr1baslem 
 |-  ( NN0 ^m 1o ) = { c e. ( NN0 ^m 1o ) | ( `' c " NN ) e. Fin }
13 11 1 2 ply1mpl0 
 |-  .0. = ( 0g ` ( 1o mPoly R ) )
14 1on 
 |-  1o e. On
15 14 a1i 
 |-  ( R e. Ring -> 1o e. On )
16 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
17 11 12 3 13 15 16 mpl0 
 |-  ( R e. Ring -> .0. = ( ( NN0 ^m 1o ) X. { Y } ) )
18 fconstmpt 
 |-  ( ( NN0 ^m 1o ) X. { Y } ) = ( b e. ( NN0 ^m 1o ) |-> Y )
19 17 18 eqtrdi 
 |-  ( R e. Ring -> .0. = ( b e. ( NN0 ^m 1o ) |-> Y ) )
20 eqidd 
 |-  ( b = ( 1o X. { a } ) -> Y = Y )
21 9 10 19 20 fmptco 
 |-  ( R e. Ring -> ( .0. o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) = ( a e. NN0 |-> Y ) )
22 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
23 eqid 
 |-  ( Base ` P ) = ( Base ` P )
24 23 2 ring0cl 
 |-  ( P e. Ring -> .0. e. ( Base ` P ) )
25 eqid 
 |-  ( coe1 ` .0. ) = ( coe1 ` .0. )
26 eqid 
 |-  ( a e. NN0 |-> ( 1o X. { a } ) ) = ( a e. NN0 |-> ( 1o X. { a } ) )
27 25 23 1 26 coe1fval2 
 |-  ( .0. e. ( Base ` P ) -> ( coe1 ` .0. ) = ( .0. o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
28 22 24 27 3syl 
 |-  ( R e. Ring -> ( coe1 ` .0. ) = ( .0. o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
29 fconstmpt 
 |-  ( NN0 X. { Y } ) = ( a e. NN0 |-> Y )
30 29 a1i 
 |-  ( R e. Ring -> ( NN0 X. { Y } ) = ( a e. NN0 |-> Y ) )
31 21 28 30 3eqtr4d 
 |-  ( R e. Ring -> ( coe1 ` .0. ) = ( NN0 X. { Y } ) )