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\mathrm{mPoly}R$$
	mplcoe4.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplcoe4.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplcoe4.b	$$⊢B={\mathrm{Base}}_P$$
	mplcoe4.i	$$⊢\phi \to I\in W$$
	mplcoe4.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplcoe4.x	$$⊢\phi \to X\in B$$
Assertion	mplcoe4	$$⊢\phi \to X=\underset{k\in D}{{\sum }_P}\left(y\in D⟼if\left(y=k,X\left(k\right),\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplcoe4.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplcoe4.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mplcoe4.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplcoe4.b	$$⊢B={\mathrm{Base}}_P$$
5		mplcoe4.i	$$⊢\phi \to I\in W$$
6		mplcoe4.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		mplcoe4.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢1_R=1_R$$
9		eqid	$$⊢{\cdot }_P={\cdot }_P$$
10	1 2 3 8 5 4 9 6 7	mplcoe1	$$⊢\phi \to X=\underset{k\in D}{{\sum }_P}\left(X\left(k\right){\cdot }_P\left(y\in D⟼if\left(y=k,1_R,\underset{\dot{}}{0}\right)\right)\right)$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12	5	adantr	$$⊢\left(\phi \wedge k\in D\right)\to I\in W$$
13	6	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{Ring}$$
14		simpr	$$⊢\left(\phi \wedge k\in D\right)\to k\in D$$
15	1 11 4 2 7	mplelf	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
16	15	ffvelcdmda	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right)\in {\mathrm{Base}}_R$$
17	1 9 2 8 3 11 12 13 14 16	mplmon2	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right){\cdot }_P\left(y\in D⟼if\left(y=k,1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=k,X\left(k\right),\underset{\dot{}}{0}\right)\right)$$
18	17	mpteq2dva	$$⊢\phi \to \left(k\in D⟼X\left(k\right){\cdot }_P\left(y\in D⟼if\left(y=k,1_R,\underset{\dot{}}{0}\right)\right)\right)=\left(k\in D⟼\left(y\in D⟼if\left(y=k,X\left(k\right),\underset{\dot{}}{0}\right)\right)\right)$$
19	18	oveq2d	$$⊢\phi \to \underset{k\in D}{{\sum }_P}\left(X\left(k\right){\cdot }_P\left(y\in D⟼if\left(y=k,1_R,\underset{\dot{}}{0}\right)\right)\right)=\underset{k\in D}{{\sum }_P}\left(y\in D⟼if\left(y=k,X\left(k\right),\underset{\dot{}}{0}\right)\right)$$
20	10 19	eqtrd	$$⊢\phi \to X=\underset{k\in D}{{\sum }_P}\left(y\in D⟼if\left(y=k,X\left(k\right),\underset{\dot{}}{0}\right)\right)$$