This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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