Metamath Proof Explorer


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 syl5eq
 |-  ( 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 )