Metamath Proof Explorer

Theorem mplmon2cl

Description: A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

Ref Expression
Hypotheses mplmon2cl.p 
|- P = ( I mPoly R )
mplmon2cl.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplmon2cl.z 
|- .0. = ( 0g ` R )
mplmon2cl.c 
|- C = ( Base ` R )
mplmon2cl.i 
|- ( ph -> I e. W )
mplmon2cl.r 
|- ( ph -> R e. Ring )
mplmon2cl.b 
|- B = ( Base ` P )
mplmon2cl.x 
|- ( ph -> X e. C )
mplmon2cl.k 
|- ( ph -> K e. D )
Assertion mplmon2cl 
|- ( ph -> ( y e. D |-> if ( y = K , X , .0. ) ) e. B )

Proof

Step Hyp Ref Expression
1 mplmon2cl.p 
 |-  P = ( I mPoly R )
2 mplmon2cl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplmon2cl.z 
 |-  .0. = ( 0g ` R )
4 mplmon2cl.c 
 |-  C = ( Base ` R )
5 mplmon2cl.i 
 |-  ( ph -> I e. W )
6 mplmon2cl.r 
 |-  ( ph -> R e. Ring )
7 mplmon2cl.b 
 |-  B = ( Base ` P )
8 mplmon2cl.x 
 |-  ( ph -> X e. C )
9 mplmon2cl.k 
 |-  ( ph -> K e. D )
10 eqid 
 |-  ( .s ` P ) = ( .s ` P )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 1 10 2 11 3 4 5 6 9 8 mplmon2 
 |-  ( ph -> ( X ( .s ` P ) ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = K , X , .0. ) ) )
13 1 mpllmod 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. LMod )
14 5 6 13 syl2anc 
 |-  ( ph -> P e. LMod )
15 1 5 6 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
16 15 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
17 4 16 syl5eq 
 |-  ( ph -> C = ( Base ` ( Scalar ` P ) ) )
18 8 17 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` P ) ) )
19 1 7 3 11 2 5 6 9 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) e. B )
20 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
21 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
22 7 20 10 21 lmodvscl 
 |-  ( ( P e. LMod /\ X e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) e. B ) -> ( X ( .s ` P ) ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) ) e. B )
23 14 18 19 22 syl3anc 
 |-  ( ph -> ( X ( .s ` P ) ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) ) e. B )
24 12 23 eqeltrrd 
 |-  ( ph -> ( y e. D |-> if ( y = K , X , .0. ) ) e. B )