Theorem mplasclf

Description: The scalar injection is a function into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Hypotheses	mplasclf.p	$$⊢P=I\mathrm{mPoly}R$$
	mplasclf.b	$$⊢B={\mathrm{Base}}_P$$
	mplasclf.k	$$⊢K={\mathrm{Base}}_R$$
	mplasclf.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	mplasclf.i	$$⊢\phi \to I\in W$$
	mplasclf.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mplasclf	$$⊢\phi \to A:K⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mplasclf.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplasclf.b	$$⊢B={\mathrm{Base}}_P$$
3		mplasclf.k	$$⊢K={\mathrm{Base}}_R$$
4		mplasclf.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
5		mplasclf.i	$$⊢\phi \to I\in W$$
6		mplasclf.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
8	1	mplring	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{Ring}$$
9	1	mpllmod	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
11	4 7 8 9 10 2	asclf	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to A:{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}⟶B$$
12	5 6 11	syl2anc	$$⊢\phi \to A:{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}⟶B$$
13	1 5 6	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
14	13	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
15	3 14	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
16	15	feq2d	$$⊢\phi \to \left(A:K⟶B\leftrightarrow A:{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}⟶B\right)$$
17	12 16	mpbird	$$⊢\phi \to A:K⟶B$$