[STATEMENT]
lemma IP_to_UP_closed:
  assumes "cring R"
  assumes "P \<in> carrier (Pring R {i::'c})"
  shows "IP_to_UP i P \<in> carrier (UP R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
have "IP_to_UP i P \<in> up R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IP_to_UP i P \<in> up R
[PROOF STEP]
apply(rule mem_upI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. IP_to_UP i P n \<in> carrier R
 2. \<exists>n. bound \<zero> n (IP_to_UP i P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cring R
P \<in> carrier (Pring R {i})

goal (2 subgoals):
 1. \<And>n. IP_to_UP i P n \<in> carrier R
 2. \<exists>n. bound \<zero> n (IP_to_UP i P)
[PROOF STEP]
apply (metis cring_def IP_to_UP_def ring.Pring_carrier_coeff')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. bound \<zero> n (IP_to_UP i P)
[PROOF STEP]
unfolding bound_def IP_to_UP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
assume A: "\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>\<^bsub>R\<^esub>"
[PROOF STATE]
proof (state)
this:
\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>
[PROOF STEP]
have 0: "\<forall>n. \<exists>m> n. (nat_to_mset i m) \<in> monomials_of R P"
[PROOF STATE]
proof (prove)
using this:
\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>

goal (1 subgoal):
 1. \<forall>n. \<exists>m>n. nat_to_mset i m \<in> monomials_of R P
[PROOF STEP]
by (meson assms(1) cring_def ring.complement_of_monomials_of)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>m>n. nat_to_mset i m \<in> monomials_of R P

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
have "\<not> finite {m. (nat_to_mset i m) \<in> monomials_of R P }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
assume "finite {m. nat_to_mset i m \<in> monomials_of R P}"
[PROOF STATE]
proof (state)
this:
finite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
have "\<exists>n. \<forall>m>n.  m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}"
[PROOF STATE]
proof (prove)
using this:
finite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. \<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
by (meson finite_nat_set_iff_bounded nat_less_le order.strict_trans)
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
have "\<exists>n. \<forall>m>n.  nat_to_mset i m \<notin> monomials_of R P"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. \<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P
[PROOF STEP]
by (simp add: monomials_of_def)
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P

goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P

goal (1 subgoal):
 1. False
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P
\<forall>n. \<exists>m>n. nat_to_mset i m \<in> monomials_of R P

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infinite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
obtain S where S_def: "infinite (S::nat set) \<and> (\<forall>m \<in> S. (nat_to_mset i m) \<in> monomials_of R P)"
[PROOF STATE]
proof (prove)
using this:
infinite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. (\<And>S. infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
have "inj_on (nat_to_mset i) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (nat_to_mset i) S
[PROOF STEP]
using inj_onI[of S "nat_to_mset i"]
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>x \<in> S; y \<in> S; nat_to_mset i x = nat_to_mset i y\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> inj_on (nat_to_mset i) S

goal (1 subgoal):
 1. inj_on (nat_to_mset i) S
[PROOF STEP]
by (meson nat_to_mset_inj)
[PROOF STATE]
proof (state)
this:
inj_on (nat_to_mset i) S

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on (nat_to_mset i) S
[PROOF STEP]
have 1: "infinite (nat_to_mset i ` S)"
[PROOF STATE]
proof (prove)
using this:
inj_on (nat_to_mset i) S

goal (1 subgoal):
 1. infinite (nat_to_mset i ` S)
[PROOF STEP]
using S_def finite_imageD
[PROOF STATE]
proof (prove)
using this:
inj_on (nat_to_mset i) S
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)
\<lbrakk>finite (?f ` ?A); inj_on ?f ?A\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. infinite (nat_to_mset i ` S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (nat_to_mset i ` S)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
have 2: "(nat_to_mset i ` S) \<subseteq> (monomials_of R P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_mset i ` S \<subseteq> monomials_of R P
[PROOF STEP]
using S_def
[PROOF STATE]
proof (prove)
using this:
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)

goal (1 subgoal):
 1. nat_to_mset i ` S \<subseteq> monomials_of R P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nat_to_mset i ` S \<subseteq> monomials_of R P

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_mset i ` S \<subseteq> monomials_of R P
[PROOF STEP]
have "infinite (monomials_of R P)"
[PROOF STATE]
proof (prove)
using this:
nat_to_mset i ` S \<subseteq> monomials_of R P

goal (1 subgoal):
 1. infinite (monomials_of R P)
[PROOF STEP]
using S_def "1" finite_subset
[PROOF STATE]
proof (prove)
using this:
nat_to_mset i ` S \<subseteq> monomials_of R P
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)
infinite (nat_to_mset i ` S)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. infinite (monomials_of R P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (monomials_of R P)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (monomials_of R P)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
infinite (monomials_of R P)

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
infinite (monomials_of R P)
cring R
P \<in> carrier (Pring R {i})

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis Pring_def cring_def partial_object.select_convs(1) ring.monomials_finite)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
IP_to_UP i P \<in> up R

goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IP_to_UP i P \<in> up R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
IP_to_UP i P \<in> up R

goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
by (metis (no_types, lifting) UP_def partial_object.select_convs(1))
[PROOF STATE]
proof (state)
this:
IP_to_UP i P \<in> carrier (UP R)

goal:
No subgoals!
[PROOF STEP]
qed