Metamath Proof Explorer

Theorem coe1mon

Description: Coefficient vector of a monomial. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1moneq.p 
|- P = ( Poly1 ` R )
ply1moneq.x 
|- X = ( var1 ` R )
ply1moneq.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
coe1mon.r 
|- ( ph -> R e. Ring )
coe1mon.n 
|- ( ph -> N e. NN0 )
coe1mon.0 
|- .0. = ( 0g ` R )
coe1mon.1 
|- .1. = ( 1r ` R )
Assertion coe1mon 
|- ( ph -> ( coe1 ` ( N .^ X ) ) = ( k e. NN0 |-> if ( k = N , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 ply1moneq.p 
 |-  P = ( Poly1 ` R )
2 ply1moneq.x 
 |-  X = ( var1 ` R )
3 ply1moneq.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
4 coe1mon.r 
 |-  ( ph -> R e. Ring )
5 coe1mon.n 
 |-  ( ph -> N e. NN0 )
6 coe1mon.0 
 |-  .0. = ( 0g ` R )
7 coe1mon.1 
 |-  .1. = ( 1r ` R )
8 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
9 4 8 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
10 9 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
11 7 10 eqtrid 
 |-  ( ph -> .1. = ( 1r ` ( Scalar ` P ) ) )
12 11 oveq1d 
 |-  ( ph -> ( .1. ( .s ` P ) ( N .^ X ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( N .^ X ) ) )
13 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
14 4 13 syl 
 |-  ( ph -> P e. LMod )
15 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
16 eqid 
 |-  ( Base ` P ) = ( Base ` P )
17 1 2 15 3 16 ply1moncl 
 |-  ( ( R e. Ring /\ N e. NN0 ) -> ( N .^ X ) e. ( Base ` P ) )
18 4 5 17 syl2anc 
 |-  ( ph -> ( N .^ X ) e. ( Base ` P ) )
19 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
20 eqid 
 |-  ( .s ` P ) = ( .s ` P )
21 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
22 16 19 20 21 lmodvs1 
 |-  ( ( P e. LMod /\ ( N .^ X ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( N .^ X ) ) = ( N .^ X ) )
23 14 18 22 syl2anc 
 |-  ( ph -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( N .^ X ) ) = ( N .^ X ) )
24 12 23 eqtrd 
 |-  ( ph -> ( .1. ( .s ` P ) ( N .^ X ) ) = ( N .^ X ) )
25 24 fveq2d 
 |-  ( ph -> ( coe1 ` ( .1. ( .s ` P ) ( N .^ X ) ) ) = ( coe1 ` ( N .^ X ) ) )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 26 7 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
28 4 27 syl 
 |-  ( ph -> .1. e. ( Base ` R ) )
29 6 26 1 2 20 15 3 coe1tm 
 |-  ( ( R e. Ring /\ .1. e. ( Base ` R ) /\ N e. NN0 ) -> ( coe1 ` ( .1. ( .s ` P ) ( N .^ X ) ) ) = ( k e. NN0 |-> if ( k = N , .1. , .0. ) ) )
30 4 28 5 29 syl3anc 
 |-  ( ph -> ( coe1 ` ( .1. ( .s ` P ) ( N .^ X ) ) ) = ( k e. NN0 |-> if ( k = N , .1. , .0. ) ) )
31 25 30 eqtr3d 
 |-  ( ph -> ( coe1 ` ( N .^ X ) ) = ( k e. NN0 |-> if ( k = N , .1. , .0. ) ) )