Theorem mplascl

Description: Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mplascl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplascl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mplascl.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplascl.b	$$⊢B={\mathrm{Base}}_R$$
5		mplascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
6		mplascl.i	$$⊢\phi \to I\in W$$
7		mplascl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		mplascl.x	$$⊢\phi \to X\in B$$
9	1 6 7	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
10	9	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
11	4 10	eqtrid	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
12	8 11	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
13		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
15		eqid	$$⊢{\cdot }_P={\cdot }_P$$
16		eqid	$$⊢1_P=1_P$$
17	5 13 14 15 16	asclval	$$⊢X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\to A\left(X\right)=X{\cdot }_P{1}_P$$
18	12 17	syl	$$⊢\phi \to A\left(X\right)=X{\cdot }_P{1}_P$$
19		eqid	$$⊢1_R=1_R$$
20	1 2 3 19 16 6 7	mpl1	$$⊢\phi \to 1_P=\left(y\in D⟼if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)$$
21	20	oveq2d	$$⊢\phi \to X{\cdot }_P{1}_P=X{\cdot }_P\left(y\in D⟼if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)$$
22	2	psrbag0	$$⊢I\in W\to I\times \left\{0\right\}\in D$$
23	6 22	syl	$$⊢\phi \to I\times \left\{0\right\}\in D$$
24	1 15 2 19 3 4 6 7 23 8	mplmon2	$$⊢\phi \to X{\cdot }_P\left(y\in D⟼if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)\right)$$
25	18 21 24	3eqtrd	$$⊢\phi \to A\left(X\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)\right)$$