Metamath Proof Explorer


Theorem ply1sclf

Description: A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1scl.p 𝑃 = ( Poly1𝑅 )
ply1scl.a 𝐴 = ( algSc ‘ 𝑃 )
coe1scl.k 𝐾 = ( Base ‘ 𝑅 )
ply1sclf.b 𝐵 = ( Base ‘ 𝑃 )
Assertion ply1sclf ( 𝑅 ∈ Ring → 𝐴 : 𝐾𝐵 )

Proof

Step Hyp Ref Expression
1 ply1scl.p 𝑃 = ( Poly1𝑅 )
2 ply1scl.a 𝐴 = ( algSc ‘ 𝑃 )
3 coe1scl.k 𝐾 = ( Base ‘ 𝑅 )
4 ply1sclf.b 𝐵 = ( Base ‘ 𝑃 )
5 1 ply1sca2 ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )
6 1 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
7 1 ply1lmod ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
8 df-base Base = Slot 1
9 8 3 strfvi 𝐾 = ( Base ‘ ( I ‘ 𝑅 ) )
10 2 5 6 7 9 4 asclf ( 𝑅 ∈ Ring → 𝐴 : 𝐾𝐵 )