[STATEMENT]
lemma poly_eval_smult:
  assumes "P \<in> Pring_set R I"
  assumes "a \<in> carrier R"
  assumes "closed_fun R g"
  shows "poly_eval R S g (a \<odot>\<^bsub>Pring R I\<^esub> P)  =a \<odot>\<^bsub>Pring R I\<^esub> poly_eval R S g P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_eval R S g (a \<odot>\<^bsub>Pring R I\<^esub> P) = a \<odot>\<^bsub>Pring R I\<^esub> poly_eval R S g P
[PROOF STEP]
using poly_eval_scalar_mult assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<in> carrier R; ?g \<in> UNIV \<rightarrow> carrier R; ?P \<in> carrier R [\<X>\<^bsub>?I\<^esub>]\<rbrakk> \<Longrightarrow> poly_eval R ?S ?g (poly_scalar_mult R ?k ?P) = poly_scalar_mult R ?k (poly_eval R ?S ?g ?P)
P \<in> carrier R [\<X>\<^bsub>I\<^esub>]
a \<in> carrier R
g \<in> UNIV \<rightarrow> carrier R

goal (1 subgoal):
 1. poly_eval R S g (a \<odot>\<^bsub>Pring R I\<^esub> P) = a \<odot>\<^bsub>Pring R I\<^esub> poly_eval R S g P
[PROOF STEP]
by (metis Pring_smult)