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 𝑃 = ( 𝐼 mPoly 𝑅 )
mplasclf.b 𝐵 = ( Base ‘ 𝑃 )
mplasclf.k 𝐾 = ( Base ‘ 𝑅 )
mplasclf.a 𝐴 = ( algSc ‘ 𝑃 )
mplasclf.i ( 𝜑𝐼𝑊 )
mplasclf.r ( 𝜑𝑅 ∈ Ring )
Assertion mplasclf ( 𝜑𝐴 : 𝐾𝐵 )

Proof

Step Hyp Ref Expression
1 mplasclf.p 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplasclf.b 𝐵 = ( Base ‘ 𝑃 )
3 mplasclf.k 𝐾 = ( Base ‘ 𝑅 )
4 mplasclf.a 𝐴 = ( algSc ‘ 𝑃 )
5 mplasclf.i ( 𝜑𝐼𝑊 )
6 mplasclf.r ( 𝜑𝑅 ∈ Ring )
7 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
8 1 mplring ( ( 𝐼𝑊𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
9 1 mpllmod ( ( 𝐼𝑊𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
10 eqid ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
11 4 7 8 9 10 2 asclf ( ( 𝐼𝑊𝑅 ∈ Ring ) → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 )
12 5 6 11 syl2anc ( 𝜑𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 )
13 1 5 6 mplsca ( 𝜑𝑅 = ( Scalar ‘ 𝑃 ) )
14 13 fveq2d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
15 3 14 syl5eq ( 𝜑𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
16 15 feq2d ( 𝜑 → ( 𝐴 : 𝐾𝐵𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 ) )
17 12 16 mpbird ( 𝜑𝐴 : 𝐾𝐵 )