[STATEMENT]
lemma proj_poly_syz_eq_zero_iff: "proj_poly_syz n p = 0 \<longleftrightarrow> (component_of_term ` keys p \<subseteq> {0..<n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (proj_poly_syz n p = 0) = (component_of_term ` keys p \<subseteq> {0..<n})
[PROOF STEP]
unfolding keys_eq_empty[symmetric] keys_proj_poly_syz
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_component (\<lambda>k. k + n) -` keys p = {}) = (component_of_term ` keys p \<subseteq> {0..<n})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map_component (\<lambda>k. k + n) -` keys p = {} \<Longrightarrow> component_of_term ` keys p \<subseteq> {0..<n}
 2. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
assume "map_component (\<lambda>k. k + n) -` keys p = {}" (is "?A = {}")
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) -` keys p = {}

goal (2 subgoals):
 1. map_component (\<lambda>k. k + n) -` keys p = {} \<Longrightarrow> component_of_term ` keys p \<subseteq> {0..<n}
 2. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
show "component_of_term ` keys p \<subseteq> {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n}
[PROOF STEP]
proof (rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "i \<in> component_of_term ` keys p"
[PROOF STATE]
proof (state)
this:
i \<in> component_of_term ` keys p

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> component_of_term ` keys p
[PROOF STEP]
obtain x where x: "x \<in> keys p" and i: "i = component_of_term x"
[PROOF STATE]
proof (prove)
using this:
i \<in> component_of_term ` keys p

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> keys p; i = component_of_term x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<in> keys p
i = component_of_term x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "i \<notin> {0..<n}"
[PROOF STATE]
proof (state)
this:
i \<notin> {0..<n}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "i - n + n = i"
[PROOF STATE]
proof (prove)
using this:
i \<notin> {0..<n}

goal (1 subgoal):
 1. i - n + n = i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i - n + n = i

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence 1: "map_component (\<lambda>k. k - n + n) x = x"
[PROOF STATE]
proof (prove)
using this:
i - n + n = i

goal (1 subgoal):
 1. map_component (\<lambda>k. k - n + n) x = x
[PROOF STEP]
by (simp add: map_component_def i term_simps)
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k - n + n) x = x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "map_component (\<lambda>k. k - n) x \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_component (\<lambda>k. k - n) x \<in> map_component (\<lambda>k. k + n) -` keys p
[PROOF STEP]
by (rule vimageI2, simp add: map_component_comp x 1)
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k - n) x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
map_component (\<lambda>k. k - n) x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: \<open>?A = {}\<close>)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` keys p \<subseteq> {0..<n}

goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
assume a: "component_of_term ` keys p \<subseteq> {0..<n}"
[PROOF STATE]
proof (state)
this:
component_of_term ` keys p \<subseteq> {0..<n}

goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
show "map_component (\<lambda>k. k + n) -` keys p = {}" (is "?A = {}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "?A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) -` keys p \<noteq> {}

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_component (\<lambda>k. k + n) -` keys p \<noteq> {}
[PROOF STEP]
obtain x where "x \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
map_component (\<lambda>k. k + n) -` keys p \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> map_component (\<lambda>k. k + n) -` keys p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "map_component (\<lambda>k. k + n) x \<in> keys p"
[PROOF STATE]
proof (prove)
using this:
x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) x \<in> keys p
[PROOF STEP]
by (rule vimageD)
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) x \<in> keys p

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` keys p \<subseteq> {0..<n}
map_component (\<lambda>k. k + n) x \<in> keys p
[PROOF STEP]
have "component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` keys p \<subseteq> {0..<n}
map_component (\<lambda>k. k + n) x \<in> keys p

goal (1 subgoal):
 1. component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) -` keys p = {}

goal:
No subgoals!
[PROOF STEP]
qed