Theorem ply1sclcl

Description: The value of the algebra scalars function for (univariate) polynomials applied to a scalar results in a constant polynomial. (Contributed by AV, 27-Nov-2019)

	Ref	Expression
Hypotheses	ply1scl.p	|- P = ( Poly1 ` R )
	ply1scl.a	|- A = ( algSc ` P )
	coe1scl.k	|- K = ( Base ` R )
	ply1sclf.b	|- B = ( Base ` P )
Assertion	ply1sclcl	|- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. 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 2 3 4	ply1sclf	|- ( R e. Ring -> A : K --> B )
6	5	ffvelrnda	|- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. B )