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 mPoly R )
	mplasclf.b	|- B = ( Base ` P )
	mplasclf.k	|- K = ( Base ` R )
	mplasclf.a	|- A = ( algSc ` P )
	mplasclf.i	|- ( ph -> I e. W )
	mplasclf.r	|- ( ph -> R e. Ring )
Assertion	mplasclf	|- ( ph -> A : K --> B )

Proof

Step	Hyp	Ref	Expression
1		mplasclf.p	|- P = ( I mPoly R )
2		mplasclf.b	|- B = ( Base ` P )
3		mplasclf.k	|- K = ( Base ` R )
4		mplasclf.a	|- A = ( algSc ` P )
5		mplasclf.i	|- ( ph -> I e. W )
6		mplasclf.r	|- ( ph -> R e. Ring )
7		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
8	1	mplring	|- ( ( I e. W /\ R e. Ring ) -> P e. Ring )
9	1	mpllmod	|- ( ( I e. W /\ R e. Ring ) -> P e. LMod )
10		eqid	|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
11	4 7 8 9 10 2	asclf	|- ( ( I e. W /\ R e. Ring ) -> A : ( Base ` ( Scalar ` P ) ) --> B )
12	5 6 11	syl2anc	|- ( ph -> A : ( Base ` ( Scalar ` P ) ) --> B )
13	1 5 6	mplsca	|- ( ph -> R = ( Scalar ` P ) )
14	13	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
15	3 14	eqtrid	|- ( ph -> K = ( Base ` ( Scalar ` P ) ) )
16	15	feq2d	|- ( ph -> ( A : K --> B <-> A : ( Base ` ( Scalar ` P ) ) --> B ) )
17	12 16	mpbird	|- ( ph -> A : K --> B )