Theorem mplmon2cl

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

	Ref	Expression
Hypotheses	mplmon2cl.p	$$⊢P=I\mathrm{mPoly}R$$
	mplmon2cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplmon2cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplmon2cl.c	$$⊢C={\mathrm{Base}}_R$$
	mplmon2cl.i	$$⊢\phi \to I\in W$$
	mplmon2cl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplmon2cl.b	$$⊢B={\mathrm{Base}}_P$$
	mplmon2cl.x	$$⊢\phi \to X\in C$$
	mplmon2cl.k	$$⊢\phi \to K\in D$$
Assertion	mplmon2cl	$$⊢\phi \to \left(y\in D⟼if\left(y=K,X,\underset{\dot{}}{0}\right)\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		mplmon2cl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplmon2cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mplmon2cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplmon2cl.c	$$⊢C={\mathrm{Base}}_R$$
5		mplmon2cl.i	$$⊢\phi \to I\in W$$
6		mplmon2cl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		mplmon2cl.b	$$⊢B={\mathrm{Base}}_P$$
8		mplmon2cl.x	$$⊢\phi \to X\in C$$
9		mplmon2cl.k	$$⊢\phi \to K\in D$$
10		eqid	$$⊢{\cdot }_P={\cdot }_P$$
11		eqid	$$⊢1_R=1_R$$
12	1 10 2 11 3 4 5 6 9 8	mplmon2	$$⊢\phi \to X{\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,\underset{\dot{}}{0}\right)\right)$$
13	1	mpllmod	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
14	5 6 13	syl2anc	$$⊢\phi \to P\in \mathrm{LMod}$$
15	1 5 6	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
16	15	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
17	4 16	syl5eq	$$⊢\phi \to C={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
18	8 17	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
19	1 7 3 11 2 5 6 9	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=K,1_R,\underset{\dot{}}{0}\right)\right)\in B$$
20		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
21		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
22	7 20 10 21	lmodvscl	$$⊢\left(P\in \mathrm{LMod}\wedge X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=K,1_R,\underset{\dot{}}{0}\right)\right)\in B\right)\to X{\cdot }_P\left(y\in D⟼if\left(y=K,1_R,\underset{\dot{}}{0}\right)\right)\in B$$
23	14 18 19 22	syl3anc	$$⊢\phi \to X{\cdot }_P\left(y\in D⟼if\left(y=K,1_R,\underset{\dot{}}{0}\right)\right)\in B$$
24	12 23	eqeltrrd	$$⊢\phi \to \left(y\in D⟼if\left(y=K,X,\underset{\dot{}}{0}\right)\right)\in B$$