Theorem mplcoe4

Description: Decompose a polynomial into a finite sum of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mplcoe4.p	|- P = ( I mPoly R )
2		mplcoe4.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3		mplcoe4.z	|- .0. = ( 0g ` R )
4		mplcoe4.b	|- B = ( Base ` P )
5		mplcoe4.i	|- ( ph -> I e. W )
6		mplcoe4.r	|- ( ph -> R e. Ring )
7		mplcoe4.x	|- ( ph -> X e. B )
8		eqid	|- ( 1r ` R ) = ( 1r ` R )
9		eqid	|- ( .s ` P ) = ( .s ` P )
10	1 2 3 8 5 4 9 6 7	mplcoe1	|- ( ph -> X = ( P gsum ( k e. D |-> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) ) ) )
11		eqid	|- ( Base ` R ) = ( Base ` R )
12	5	adantr	|- ( ( ph /\ k e. D ) -> I e. W )
13	6	adantr	|- ( ( ph /\ k e. D ) -> R e. Ring )
14		simpr	|- ( ( ph /\ k e. D ) -> k e. D )
15	1 11 4 2 7	mplelf	|- ( ph -> X : D --> ( Base ` R ) )
16	15	ffvelrnda	|- ( ( ph /\ k e. D ) -> ( X ` k ) e. ( Base ` R ) )
17	1 9 2 8 3 11 12 13 14 16	mplmon2	|- ( ( ph /\ k e. D ) -> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) )
18	17	mpteq2dva	|- ( ph -> ( k e. D |-> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) ) = ( k e. D |-> ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) ) )
19	18	oveq2d	|- ( ph -> ( P gsum ( k e. D |-> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) ) ) = ( P gsum ( k e. D |-> ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) ) ) )
20	10 19	eqtrd	|- ( ph -> X = ( P gsum ( k e. D |-> ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) ) ) )