[STATEMENT]
lemma SA_poly_to_SA_fun_monom':
  assumes "f \<in> carrier (SA n)"
  assumes "x \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)"
  assumes "t \<in> carrier Q\<^sub>p"
  shows "SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t#x) = (f x)\<otimes>t[^]\<^bsub>Q\<^sub>p\<^esub>k "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
have 0: "hd (t#x) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff (t # x) = t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lead_coeff (t # x) = t

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
have 1: "tl (t#x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (t # x) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tl (t # x) = x

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
have 2: "(t#x) \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)
[PROOF STEP]
by (metis add.commute assms  cartesian_power_cons plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
using 0 1 2 SA_poly_to_SA_fun_monom[of f n "t#x" k] assms SA_poly_to_SA_fun_monom
[PROOF STATE]
proof (prove)
using this:
lead_coeff (t # x) = t
tl (t # x) = x
t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)
\<lbrakk>f \<in> carrier (SA n); t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)\<rbrakk> \<Longrightarrow> SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f (tl (t # x)) \<otimes> lead_coeff (t # x) [^] k
f \<in> carrier (SA n)
x \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)
t \<in> carrier Q\<^sub>p
\<lbrakk>?f \<in> carrier (SA ?n); ?a \<in> carrier (Q\<^sub>p\<^bsup>Suc ?n\<^esup>)\<rbrakk> \<Longrightarrow> SA_poly_to_SA_fun ?n (up_ring.monom (UP (SA ?n)) ?f ?k) ?a = ?f (tl ?a) \<otimes> lead_coeff ?a [^] ?k

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k

goal:
No subgoals!
[PROOF STEP]
qed