Theorem ply1sclf

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

	Ref	Expression
Hypotheses	ply1scl.p	|- P = ( Poly1 ` R )
	ply1scl.a	|- A = ( algSc ` P )
	coe1scl.k	|- K = ( Base ` R )
	ply1sclf.b	|- B = ( Base ` P )
Assertion	ply1sclf	|- ( R e. Ring -> A : K --> B )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	|- P = ( Poly1 ` R )
2		ply1scl.a	|- A = ( algSc ` P )
3		coe1scl.k	|- K = ( Base ` R )
4		ply1sclf.b	|- B = ( Base ` P )
5	1	ply1sca2	|- ( _I ` R ) = ( Scalar ` P )
6	1	ply1ring	|- ( R e. Ring -> P e. Ring )
7	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
8		df-base	|- Base = Slot 1
9	8 3	strfvi	|- K = ( Base ` ( _I ` R ) )
10	2 5 6 7 9 4	asclf	|- ( R e. Ring -> A : K --> B )