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 5 6	mpllmodd	|- ( ph -> P e. LMod )
14	1 5 6	mplsca	|- ( ph -> R = ( Scalar ` P ) )
15	14	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
16	4 15	eqtrid	|- ( ph -> C = ( Base ` ( Scalar ` P ) ) )
17	8 16	eleqtrd	|- ( ph -> X e. ( Base ` ( Scalar ` P ) ) )
18	1 7 3 11 2 5 6 9	mplmon	|- ( ph -> ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) e. B )
19		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
20		eqid	|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
21	7 19 10 20	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 )
22	13 17 18 21	syl3anc	|- ( ph -> ( X ( .s ` P ) ( y e. D |-> if ( y = K , ( 1r ` R ) , .0. ) ) ) e. B )
23	12 22	eqeltrrd	|- ( ph -> ( y e. D |-> if ( y = K , X , .0. ) ) e. B )