[STATEMENT]
lemma Fun_add_pow_apply:
  assumes "b \<in> carrier (Fun\<^bsub>n\<^esub> Q\<^sub>p)"
  assumes "a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)"
  shows "([(m::nat)]\<cdot>\<^bsub>Fun\<^bsub>n\<^esub> Q\<^sub>p\<^esub> b) a = [m]\<cdot>( b a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
have 0: "b a \<in> carrier Q\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b a \<in> carrier Q\<^sub>p
[PROOF STEP]
using Qp.function_ring_car_mem_closed assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> carrier (function_ring ?S Q\<^sub>p); ?s \<in> ?S\<rbrakk> \<Longrightarrow> ?f ?s \<in> carrier Q\<^sub>p
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. b a \<in> carrier Q\<^sub>p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
b a \<in> carrier Q\<^sub>p

goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
have 1: "ring (Fun\<^bsub>n\<^esub> Q\<^sub>p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
[PROOF STEP]
using function_ring_is_ring
[PROOF STATE]
proof (prove)
using this:
ring (function_ring (carrier (Q\<^sub>p\<^bsup>?n\<^esup>)) Q\<^sub>p)

goal (1 subgoal):
 1. ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)

goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
proof(induction m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
 2. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
 2. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
have "([(0::nat)] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) = \<zero>\<^bsub>Fun\<^bsub>n\<^esub> Q\<^sub>p\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
[PROOF STEP]
using 1 ring.add_pow_zero[of "Fun\<^bsub>n\<^esub> Q\<^sub>p" b ] assms
[PROOF STATE]
proof (prove)
using this:
ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
\<lbrakk>ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p); b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)\<rbrakk> \<Longrightarrow> [0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. [0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>

goal (2 subgoals):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
 2. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>

goal (1 subgoal):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
[PROOF STEP]
using  function_zero_eval Qp.nat_mult_zero assms
[PROOF STATE]
proof (prove)
using this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
?a \<in> carrier (Q\<^sub>p\<^bsup>?n\<^esup>) \<Longrightarrow> \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>?n\<^esup>)) Q\<^sub>p\<^esub> ?a = \<zero>
[0] \<cdot> ?x = \<zero>
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a

goal (1 subgoal):
 1. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a

goal (1 subgoal):
 1. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a

goal (1 subgoal):
 1. ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
using Suc ring.add_pow_Suc[of "SA n" b m] assms
[PROOF STATE]
proof (prove)
using this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
\<lbrakk>ring (SA n); b \<in> carrier (SA n)\<rbrakk> \<Longrightarrow> [Suc m] \<cdot>\<^bsub>SA n\<^esub> b = [m] \<cdot>\<^bsub>SA n\<^esub> b \<oplus>\<^bsub>SA n\<^esub> b
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
by (metis (no_types, lifting) "0" "1" Qp.ring_axioms SA_add SA_plus ring.add_pow_Suc)
[PROOF STATE]
proof (state)
this:
([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a

goal:
No subgoals!
[PROOF STEP]
qed