[STATEMENT]
lemma ideal_subgroup_generated:
  assumes "ideal \<aa> R (+) (\<cdot>) \<zero> \<one>" and "ideal \<bb> R (+) (\<cdot>) \<zero> \<one>"
  shows "ideal (ideal_gen_by_prod \<aa> \<bb>) R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (ideal_gen_by_prod \<aa> \<bb>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. ideal_gen_by_prod \<aa> \<bb> \<subseteq> R
 2. \<And>a b. \<lbrakk>a \<in> ideal_gen_by_prod \<aa> \<bb>; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a + b \<in> ideal_gen_by_prod \<aa> \<bb>
 3. \<zero> \<in> ideal_gen_by_prod \<aa> \<bb>
 4. \<And>a b c. \<lbrakk>a \<in> ideal_gen_by_prod \<aa> \<bb>; b \<in> ideal_gen_by_prod \<aa> \<bb>; c \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 5. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> \<zero> + a = a
 6. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> a + \<zero> = a
 7. \<And>u. u \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
 8. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 9. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "ideal_gen_by_prod \<aa> \<bb> \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_gen_by_prod \<aa> \<bb> \<subseteq> R
[PROOF STEP]
by (simp add: additive.subgroup_generated_is_subset ideal_gen_by_prod_def)
[PROOF STATE]
proof (state)
this:
ideal_gen_by_prod \<aa> \<bb> \<subseteq> R

goal (8 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> ideal_gen_by_prod \<aa> \<bb>; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a + b \<in> ideal_gen_by_prod \<aa> \<bb>
 2. \<zero> \<in> ideal_gen_by_prod \<aa> \<bb>
 3. \<And>a b c. \<lbrakk>a \<in> ideal_gen_by_prod \<aa> \<bb>; b \<in> ideal_gen_by_prod \<aa> \<bb>; c \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 4. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> \<zero> + a = a
 5. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> a + \<zero> = a
 6. \<And>u. u \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
 7. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 8. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "a + b \<in> ideal_gen_by_prod \<aa> \<bb>"
    if "a \<in> ideal_gen_by_prod \<aa> \<bb>" "b \<in> ideal_gen_by_prod \<aa> \<bb>"
    for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
using that additive.subgroup_generated_is_monoid monoid.composition_closed
[PROOF STATE]
proof (prove)
using this:
a \<in> ideal_gen_by_prod \<aa> \<bb>
b \<in> ideal_gen_by_prod \<aa> \<bb>
Group_Theory.monoid (additive.subgroup_generated ?H) (+) \<zero>
\<lbrakk>Group_Theory.monoid ?M ?composition ?unit; ?a \<in> ?M; ?b \<in> ?M\<rbrakk> \<Longrightarrow> ?composition ?a ?b \<in> ?M

goal (1 subgoal):
 1. a + b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
by (fastforce simp: ideal_gen_by_prod_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> ideal_gen_by_prod \<aa> \<bb>; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?a2 + ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>

goal (7 subgoals):
 1. \<zero> \<in> ideal_gen_by_prod \<aa> \<bb>
 2. \<And>a b c. \<lbrakk>a \<in> ideal_gen_by_prod \<aa> \<bb>; b \<in> ideal_gen_by_prod \<aa> \<bb>; c \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 3. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> \<zero> + a = a
 4. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> a + \<zero> = a
 5. \<And>u. u \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
 6. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 7. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "\<zero> \<in> ideal_gen_by_prod \<aa> \<bb>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
using additive.generate.unit additive.subgroup_generated_def ideal_gen_by_prod_def
[PROOF STATE]
proof (prove)
using this:
\<zero> \<in> additive.generate ?H
additive.subgroup_generated ?S = additive.generate (R \<inter> ?S)
ideal_gen_by_prod ?\<aa> ?\<bb> \<equiv> additive.subgroup_generated {a \<cdot> b |a b. a \<in> ?\<aa> \<and> b \<in> ?\<bb>}

goal (1 subgoal):
 1. \<zero> \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<zero> \<in> ideal_gen_by_prod \<aa> \<bb>

goal (6 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> ideal_gen_by_prod \<aa> \<bb>; b \<in> ideal_gen_by_prod \<aa> \<bb>; c \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a + b + c = a + (b + c)
 2. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> \<zero> + a = a
 3. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> a + \<zero> = a
 4. \<And>u. u \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
 5. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 6. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "a + b + c = a + (b + c)"
    if "a \<in> ideal_gen_by_prod \<aa> \<bb>" "b \<in> ideal_gen_by_prod \<aa> \<bb>" "c \<in> ideal_gen_by_prod \<aa> \<bb>"
    for a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b + c = a + (b + c)
[PROOF STEP]
using that additive.subgroup_generated_is_subset
[PROOF STATE]
proof (prove)
using this:
a \<in> ideal_gen_by_prod \<aa> \<bb>
b \<in> ideal_gen_by_prod \<aa> \<bb>
c \<in> ideal_gen_by_prod \<aa> \<bb>
additive.subgroup_generated ?H \<subseteq> R

goal (1 subgoal):
 1. a + b + c = a + (b + c)
[PROOF STEP]
unfolding ideal_gen_by_prod_def
[PROOF STATE]
proof (prove)
using this:
a \<in> additive.subgroup_generated {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
b \<in> additive.subgroup_generated {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
c \<in> additive.subgroup_generated {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
additive.subgroup_generated ?H \<subseteq> R

goal (1 subgoal):
 1. a + b + c = a + (b + c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> ideal_gen_by_prod \<aa> \<bb>; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>; ?c2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?a2 + ?b2 + ?c2 = ?a2 + (?b2 + ?c2)

goal (5 subgoals):
 1. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> \<zero> + a = a
 2. \<And>a. a \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> a + \<zero> = a
 3. \<And>u. u \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
 4. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 5. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "\<zero> + a = a" "a + \<zero> = a"
    if "a \<in> ideal_gen_by_prod \<aa> \<bb>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> + a = a &&& a + \<zero> = a
[PROOF STEP]
using that additive.subgroup_generated_is_subset
[PROOF STATE]
proof (prove)
using this:
a \<in> ideal_gen_by_prod \<aa> \<bb>
additive.subgroup_generated ?H \<subseteq> R

goal (1 subgoal):
 1. \<zero> + a = a &&& a + \<zero> = a
[PROOF STEP]
unfolding ideal_gen_by_prod_def
[PROOF STATE]
proof (prove)
using this:
a \<in> additive.subgroup_generated {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
additive.subgroup_generated ?H \<subseteq> R

goal (1 subgoal):
 1. \<zero> + a = a &&& a + \<zero> = a
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
?a2 \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> \<zero> + ?a2 = ?a2
?a2 \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> ?a2 + \<zero> = ?a2

goal (3 subgoals):
 1. \<And>u. u \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 3. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u"
    if "u \<in> ideal_gen_by_prod \<aa> \<bb>" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
[PROOF STEP]
using that additive.subgroup_generated_is_subgroup group.invertible
[PROOF STATE]
proof (prove)
using this:
u \<in> ideal_gen_by_prod \<aa> \<bb>
subgroup (additive.subgroup_generated ?H) R (+) \<zero>
\<lbrakk>Group_Theory.group ?G ?composition ?unit; ?u \<in> ?G\<rbrakk> \<Longrightarrow> monoid.invertible ?G ?composition ?unit ?u

goal (1 subgoal):
 1. monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> u
[PROOF STEP]
unfolding ideal_gen_by_prod_def subgroup_def
[PROOF STATE]
proof (prove)
using this:
u \<in> additive.subgroup_generated {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
submonoid (additive.subgroup_generated ?H) R (+) \<zero> \<and> Group_Theory.group (additive.subgroup_generated ?H) (+) \<zero>
\<lbrakk>Group_Theory.group ?G ?composition ?unit; ?u \<in> ?G\<rbrakk> \<Longrightarrow> monoid.invertible ?G ?composition ?unit ?u

goal (1 subgoal):
 1. monoid.invertible (additive.subgroup_generated {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}) (+) \<zero> u
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?u2 \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> monoid.invertible (ideal_gen_by_prod \<aa> \<bb>) (+) \<zero> ?u2

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>"
    if "a \<in> R" "b \<in> ideal_gen_by_prod \<aa> \<bb>" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> R
b \<in> ideal_gen_by_prod \<aa> \<bb>

goal (1 subgoal):
 1. a \<cdot> b \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
by (simp add: assms in_ideal_gen_by_prod)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> R; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?a2 \<cdot> ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a2 \<in> R; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?a2 \<cdot> ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>"
    if "a \<in> R" "b \<in> ideal_gen_by_prod \<aa> \<bb>" for a b
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a2 \<in> R; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?a2 \<cdot> ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>

goal (1 subgoal):
 1. b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a2 \<in> R; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?a2 \<cdot> ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>
a \<in> R
b \<in> ideal_gen_by_prod \<aa> \<bb>

goal (1 subgoal):
 1. b \<cdot> a \<in> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
by (metis \<open>ideal_gen_by_prod \<aa> \<bb> \<subseteq> R\<close> comm_mult in_mono)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> R; ?b2 \<in> ideal_gen_by_prod \<aa> \<bb>\<rbrakk> \<Longrightarrow> ?b2 \<cdot> ?a2 \<in> ideal_gen_by_prod \<aa> \<bb>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ideal_gen_by_prod_is_inter:
  assumes "ideal \<aa> R (+) (\<cdot>) \<zero> \<one>" and "ideal \<bb> R (+) (\<cdot>) \<zero> \<one>"
  shows "ideal_gen_by_prod \<aa> \<bb> = \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_gen_by_prod \<aa> \<bb> = \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
 2. \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I} \<subseteq> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
have "x \<in> ?rhs" if "x \<in> ?lhs" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> ideal_gen_by_prod \<aa> \<bb>

goal (1 subgoal):
 1. x \<in> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
[PROOF STEP]
unfolding ideal_gen_by_prod_def additive.subgroup_generated_def
[PROOF STATE]
proof (prove)
using this:
x \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal (1 subgoal):
 1. x \<in> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
[PROOF STEP]
by induction (force simp: ideal_zero ideal_inverse ideal_add)+
[PROOF STATE]
proof (state)
this:
?x2 \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> ?x2 \<in> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}

goal (2 subgoals):
 1. ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
 2. \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I} \<subseteq> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> ?x2 \<in> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> ideal_gen_by_prod \<aa> \<bb> \<Longrightarrow> ?x2 \<in> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}

goal (1 subgoal):
 1. ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I}

goal (1 subgoal):
 1. \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I} \<subseteq> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I} \<subseteq> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
using assms ideal_subgroup_generated
[PROOF STATE]
proof (prove)
using this:
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
\<lbrakk>ideal ?\<aa> R (+) (\<cdot>) \<zero> \<one>; ideal ?\<bb> R (+) (\<cdot>) \<zero> \<one>\<rbrakk> \<Longrightarrow> ideal (ideal_gen_by_prod ?\<aa> ?\<bb>) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I} \<subseteq> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
by (force simp: ideal_mult_in_subgroup_generated)
[PROOF STATE]
proof (state)
this:
\<Inter> {I. ideal I R (+) (\<cdot>) \<zero> \<one> \<and> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<subseteq> I} \<subseteq> ideal_gen_by_prod \<aa> \<bb>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_1 [simp]:
  shows "\<one> \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> \<notin> I
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<one> \<in> I \<Longrightarrow> False
[PROOF STEP]
assume "\<one> \<in> I"
[PROOF STATE]
proof (state)
this:
\<one> \<in> I

goal (1 subgoal):
 1. \<one> \<in> I \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<one> \<in> I
[PROOF STEP]
have "\<And>x. \<lbrakk>\<one> \<in> I; x \<in> R\<rbrakk> \<Longrightarrow> x \<in> I"
[PROOF STATE]
proof (prove)
using this:
\<one> \<in> I

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<one> \<in> I; x \<in> R\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
by (metis ideal(1) comm.multiplicative.right_unit)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<one> \<in> I; ?x2 \<in> R\<rbrakk> \<Longrightarrow> ?x2 \<in> I

goal (1 subgoal):
 1. \<one> \<in> I \<Longrightarrow> False
[PROOF STEP]
with \<open>\<one> \<in> I\<close>
[PROOF STATE]
proof (chain)
picking this:
\<one> \<in> I
\<lbrakk>\<one> \<in> I; ?x2 \<in> R\<rbrakk> \<Longrightarrow> ?x2 \<in> I
[PROOF STEP]
have "I = R"
[PROOF STATE]
proof (prove)
using this:
\<one> \<in> I
\<lbrakk>\<one> \<in> I; ?x2 \<in> R\<rbrakk> \<Longrightarrow> ?x2 \<in> I

goal (1 subgoal):
 1. I = R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I = R

goal (1 subgoal):
 1. \<one> \<in> I \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I = R
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
I = R

goal (1 subgoal):
 1. False
[PROOF STEP]
using carrier_neq
[PROOF STATE]
proof (prove)
using this:
I = R
I \<noteq> R

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_invertible:
  assumes "x \<in> I"
  shows "\<not> comm.multiplicative.invertible x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> comm.multiplicative.invertible x
[PROOF STEP]
using assms ideal(2) not_1
[PROOF STATE]
proof (prove)
using this:
x \<in> I
\<lbrakk>?a \<in> R; ?b \<in> I\<rbrakk> \<Longrightarrow> ?b \<cdot> ?a \<in> I
\<one> \<notin> I

goal (1 subgoal):
 1. \<not> comm.multiplicative.invertible x
[PROOF STEP]
by blast


[STATEMENT]
lemma submonoid_notin:
  assumes "S = {x \<in> R. x \<notin> I}"
  shows "submonoid S R (\<cdot>) \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid S R (\<cdot>) \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. S \<subseteq> R
 2. \<And>a b. \<lbrakk>a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> S
 3. \<one> \<in> S
[PROOF STEP]
show "S \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S = {x \<in> R. x \<notin> I}

goal (1 subgoal):
 1. S \<subseteq> R
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
S \<subseteq> R

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> S
 2. \<one> \<in> S
[PROOF STEP]
show "a \<cdot> b \<in> S"
    if "a \<in> S"
      and "b \<in> S"
    for a :: 'a
      and b :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b \<in> S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> S
b \<in> S

goal (1 subgoal):
 1. a \<cdot> b \<in> S
[PROOF STEP]
using absorbent assms
[PROOF STATE]
proof (prove)
using this:
a \<in> S
b \<in> S
\<lbrakk>?x \<in> R; ?y \<in> R; ?x \<cdot> ?y \<in> I\<rbrakk> \<Longrightarrow> ?x \<in> I \<or> ?y \<in> I
S = {x \<in> R. x \<notin> I}

goal (1 subgoal):
 1. a \<cdot> b \<in> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<in> S; ?b2 \<in> S\<rbrakk> \<Longrightarrow> ?a2 \<cdot> ?b2 \<in> S

goal (1 subgoal):
 1. \<one> \<in> S
[PROOF STEP]
show "\<one> \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> \<in> S
[PROOF STEP]
using assms carrier_neq ideal(1)
[PROOF STATE]
proof (prove)
using this:
S = {x \<in> R. x \<notin> I}
I \<noteq> R
\<lbrakk>?a \<in> R; ?b \<in> I\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> I

goal (1 subgoal):
 1. \<one> \<in> S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<one> \<in> S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cring0_spectrum_eq [simp]: "cring0.spectrum = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring0.spectrum = {}
[PROOF STEP]
unfolding cring0.spectrum_def pr_ideal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {I. comm_ring {0} ring0.subtraction ring0.subtraction 0 0 \<and> ideal I {0} ring0.subtraction ring0.subtraction 0 0 \<and> pr_ideal_axioms {0} I ring0.subtraction} = {}
[PROOF STEP]
by (metis (no_types, lifting) Collect_empty_eq cring0.ideal_zero pr_ideal.intro pr_ideal.not_1)


[STATEMENT]
lemma closed_subsets_R [simp]:
  shows "\<V> R = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<V> R = {}
[PROOF STEP]
using ideal_implies_subset
[PROOF STATE]
proof (prove)
using this:
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R

goal (1 subgoal):
 1. \<V> R = {}
[PROOF STEP]
by (auto simp: closed_subsets_def pr_ideal_axioms_def pr_ideal_def)


[STATEMENT]
lemma closed_subsets_zero [simp]:
  shows "\<V> {\<zero>} = Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<V> {\<zero>} = Spec
[PROOF STEP]
unfolding closed_subsets_def spectrum_def pr_ideal_def pr_ideal_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {I. (comm_ring R (+) (\<cdot>) \<zero> \<one> \<and> ideal I R (+) (\<cdot>) \<zero> \<one> \<and> I \<noteq> R \<and> (\<forall>x y. x \<in> R \<longrightarrow> y \<in> R \<longrightarrow> x \<cdot> y \<in> I \<longrightarrow> x \<in> I \<or> y \<in> I)) \<and> {\<zero>} \<subseteq> I} = {I. comm_ring R (+) (\<cdot>) \<zero> \<one> \<and> ideal I R (+) (\<cdot>) \<zero> \<one> \<and> I \<noteq> R \<and> (\<forall>x y. x \<in> R \<longrightarrow> y \<in> R \<longrightarrow> x \<cdot> y \<in> I \<longrightarrow> x \<in> I \<or> y \<in> I)}
[PROOF STEP]
by (auto dest: ideal_zero)


[STATEMENT]
lemma closed_subsets_ideal_aux:
  assumes \<aa>: "ideal \<aa> R (+) (\<cdot>) \<zero> \<one>" and \<bb>: "ideal \<bb> R (+) (\<cdot>) \<zero> \<one>"
      and prime: "pr_ideal R x (+) (\<cdot>) \<zero> \<one>" and disj: "\<aa> \<subseteq> x \<or> \<bb> \<subseteq> x"
  shows "ideal_gen_by_prod \<aa> \<bb> \<subseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_gen_by_prod \<aa> \<bb> \<subseteq> x
[PROOF STEP]
unfolding ideal_gen_by_prod_def additive.subgroup_generated_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}) \<subseteq> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}) \<Longrightarrow> xa \<in> x
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}) \<Longrightarrow> xa \<in> x
[PROOF STEP]
assume u: "u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})"
[PROOF STATE]
proof (state)
this:
u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal (1 subgoal):
 1. \<And>xa. xa \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}) \<Longrightarrow> xa \<in> x
[PROOF STEP]
have "\<aa> \<subseteq> R" "\<bb> \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aa> \<subseteq> R &&& \<bb> \<subseteq> R
[PROOF STEP]
using \<aa> \<bb> ideal_implies_subset
[PROOF STATE]
proof (prove)
using this:
ideal \<aa> R (+) (\<cdot>) \<zero> \<one>
ideal \<bb> R (+) (\<cdot>) \<zero> \<one>
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R

goal (1 subgoal):
 1. \<aa> \<subseteq> R &&& \<bb> \<subseteq> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<aa> \<subseteq> R
\<bb> \<subseteq> R

goal (1 subgoal):
 1. \<And>xa. xa \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}) \<Longrightarrow> xa \<in> x
[PROOF STEP]
show "u \<in> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> x
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
u \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})

goal (1 subgoal):
 1. u \<in> x
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<zero> \<in> x
 2. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> a \<in> x
 3. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 4. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
case unit
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<zero> \<in> x
 2. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> a \<in> x
 3. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 4. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> x
[PROOF STEP]
by (meson comm_ring.ideal_zero prime pr_ideal_def)
[PROOF STATE]
proof (state)
this:
\<zero> \<in> x

goal (3 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> a \<in> x
 2. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 3. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> a \<in> x
 2. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 3. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
case (incl a)
[PROOF STATE]
proof (state)
this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}

goal (3 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> a \<in> x
 2. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 3. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
[PROOF STEP]
have "a \<in> R"
[PROOF STATE]
proof (prove)
using this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}

goal (1 subgoal):
 1. a \<in> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> R

goal (3 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> a \<in> x
 2. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 3. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
with incl pr_ideal.axioms [OF prime]
[PROOF STATE]
proof (chain)
picking this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
comm_ring R (+) (\<cdot>) \<zero> \<one>
ideal x R (+) (\<cdot>) \<zero> \<one>
pr_ideal_axioms R x (\<cdot>)
a \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
comm_ring R (+) (\<cdot>) \<zero> \<one>
ideal x R (+) (\<cdot>) \<zero> \<one>
pr_ideal_axioms R x (\<cdot>)
a \<in> R

goal (1 subgoal):
 1. a \<in> x
[PROOF STEP]
by clarsimp (metis \<open>\<aa> \<subseteq> R\<close> \<open>\<bb> \<subseteq> R\<close> disj ideal.ideal subset_iff)
[PROOF STATE]
proof (state)
this:
a \<in> x

goal (2 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 2. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 2. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
case (inv a)
[PROOF STATE]
proof (state)
this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}

goal (2 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 2. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
[PROOF STEP]
have "a \<in> R"
[PROOF STATE]
proof (prove)
using this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}

goal (1 subgoal):
 1. a \<in> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> R

goal (2 subgoals):
 1. \<And>a. a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>} \<Longrightarrow> - a \<in> x
 2. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
with inv pr_ideal.axioms [OF prime]
[PROOF STATE]
proof (chain)
picking this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
comm_ring R (+) (\<cdot>) \<zero> \<one>
ideal x R (+) (\<cdot>) \<zero> \<one>
pr_ideal_axioms R x (\<cdot>)
a \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}
comm_ring R (+) (\<cdot>) \<zero> \<one>
ideal x R (+) (\<cdot>) \<zero> \<one>
pr_ideal_axioms R x (\<cdot>)
a \<in> R

goal (1 subgoal):
 1. - a \<in> x
[PROOF STEP]
by clarsimp (metis \<open>\<aa> \<subseteq> R\<close> \<open>\<bb> \<subseteq> R\<close> disj ideal.ideal ideal_inverse subset_iff)
[PROOF STATE]
proof (state)
this:
- a \<in> x

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
case (mult a b)
[PROOF STATE]
proof (state)
this:
a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> x
b \<in> x

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); a \<in> x; b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>}); b \<in> x\<rbrakk> \<Longrightarrow> a + b \<in> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> x
b \<in> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
b \<in> additive.generate (R \<inter> {a \<cdot> b |a b. a \<in> \<aa> \<and> b \<in> \<bb>})
a \<in> x
b \<in> x

goal (1 subgoal):
 1. a + b \<in> x
[PROOF STEP]
by (meson prime comm_ring.ideal_add pr_ideal_def)
[PROOF STATE]
proof (state)
this:
a + b \<in> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closed_subsets_ideal_iff:
  assumes "ideal \<aa> R (+) (\<cdot>) \<zero> \<one>" and "ideal \<bb> R (+) (\<cdot>) \<zero> \<one>"
  shows "\<V> (ideal_gen_by_prod \<aa> \<bb>) = (\<V> \<aa>) \<union> (\<V> \<bb>)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<V> ideal_gen_by_prod \<aa> \<bb> = \<V> \<aa> \<union> \<V> \<bb>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<V> ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<V> \<aa> \<union> \<V> \<bb>
 2. \<V> \<aa> \<union> \<V> \<bb> \<subseteq> \<V> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<V> ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<V> \<aa> \<union> \<V> \<bb>
[PROOF STEP]
unfolding closed_subsets_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> ideal_gen_by_prod \<aa> \<bb> \<subseteq> I} \<subseteq> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> \<aa> \<subseteq> I} \<union> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> \<bb> \<subseteq> I}
[PROOF STEP]
by clarsimp (meson assms ideal_implies_subset ideal_mult_in_subgroup_generated in_mono pr_ideal.absorbent)
[PROOF STATE]
proof (state)
this:
\<V> ideal_gen_by_prod \<aa> \<bb> \<subseteq> \<V> \<aa> \<union> \<V> \<bb>

goal (1 subgoal):
 1. \<V> \<aa> \<union> \<V> \<bb> \<subseteq> \<V> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<V> \<aa> \<union> \<V> \<bb> \<subseteq> \<V> ideal_gen_by_prod \<aa> \<bb>
[PROOF STEP]
unfolding closed_subsets_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> \<aa> \<subseteq> I} \<union> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> \<bb> \<subseteq> I} \<subseteq> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> ideal_gen_by_prod \<aa> \<bb> \<subseteq> I}
[PROOF STEP]
using closed_subsets_ideal_aux [OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pr_ideal R ?x (+) (\<cdot>) \<zero> \<one>; \<aa> \<subseteq> ?x \<or> \<bb> \<subseteq> ?x\<rbrakk> \<Longrightarrow> ideal_gen_by_prod \<aa> \<bb> \<subseteq> ?x

goal (1 subgoal):
 1. {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> \<aa> \<subseteq> I} \<union> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> \<bb> \<subseteq> I} \<subseteq> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one> \<and> ideal_gen_by_prod \<aa> \<bb> \<subseteq> I}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<V> \<aa> \<union> \<V> \<bb> \<subseteq> \<V> ideal_gen_by_prod \<aa> \<bb>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finsum_empty [simp]: "finsum {} f = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum {} f = \<zero>
[PROOF STEP]
by (simp add: additive.finprod_def)


[STATEMENT]
lemma finsum_insert:
  assumes "finite I" "i \<notin> I"
    and R: "f i \<in> R" "\<And>j. j \<in> I \<Longrightarrow> f j \<in> R"
  shows "finsum (insert i I) f = f i + finsum I f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum (insert i I) f = f i + finsum I f
[PROOF STEP]
unfolding additive.finprod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if finite (insert i I) then foldD R ((+) \<circ> f) \<zero> (insert i I) else \<zero>) = f i + (if finite I then foldD R ((+) \<circ> f) \<zero> I else \<zero>)
[PROOF STEP]
proof (subst LCD.foldD_insert [where B = "insert i I"])
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. LCD (insert i I) R ((+) \<circ> f)
 2. finite I
 3. i \<notin> I
 4. i \<in> insert i I
 5. \<zero> \<in> R
 6. I \<subseteq> insert i I
 7. (if finite (insert i I) then ((+) \<circ> f) i (foldD R ((+) \<circ> f) \<zero> I) else \<zero>) = f i + (if finite I then foldD R ((+) \<circ> f) \<zero> I else \<zero>)
[PROOF STEP]
show "LCD (insert i I) R ((+) \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LCD (insert i I) R ((+) \<circ> f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> insert i I; y \<in> insert i I; z \<in> R\<rbrakk> \<Longrightarrow> ((+) \<circ> f) x (((+) \<circ> f) y z) = ((+) \<circ> f) y (((+) \<circ> f) x z)
 2. \<And>x y. \<lbrakk>x \<in> insert i I; y \<in> R\<rbrakk> \<Longrightarrow> ((+) \<circ> f) x y \<in> R
[PROOF STEP]
show "((+) \<circ> f) x (((+) \<circ> f) y z) = ((+) \<circ> f) y (((+) \<circ> f) x z)"
      if "x \<in> insert i I" "y \<in> insert i I" "z \<in> R" for x y z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((+) \<circ> f) x (((+) \<circ> f) y z) = ((+) \<circ> f) y (((+) \<circ> f) x z)
[PROOF STEP]
using that additive.associative additive.commutative R
[PROOF STATE]
proof (prove)
using this:
x \<in> insert i I
y \<in> insert i I
z \<in> R
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a + ?b + ?c = ?a + (?b + ?c)
\<lbrakk>?x \<in> R; ?y \<in> R\<rbrakk> \<Longrightarrow> ?x + ?y = ?y + ?x
f i \<in> R
?j3 \<in> I \<Longrightarrow> f ?j3 \<in> R

goal (1 subgoal):
 1. ((+) \<circ> f) x (((+) \<circ> f) y z) = ((+) \<circ> f) y (((+) \<circ> f) x z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> insert i I; ?y3 \<in> insert i I; ?z3 \<in> R\<rbrakk> \<Longrightarrow> ((+) \<circ> f) ?x3 (((+) \<circ> f) ?y3 ?z3) = ((+) \<circ> f) ?y3 (((+) \<circ> f) ?x3 ?z3)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> insert i I; y \<in> R\<rbrakk> \<Longrightarrow> ((+) \<circ> f) x y \<in> R
[PROOF STEP]
show "((+) \<circ> f) x y \<in> R"
      if "x \<in> insert i I" "y \<in> R" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((+) \<circ> f) x y \<in> R
[PROOF STEP]
using that R
[PROOF STATE]
proof (prove)
using this:
x \<in> insert i I
y \<in> R
f i \<in> R
?j3 \<in> I \<Longrightarrow> f ?j3 \<in> R

goal (1 subgoal):
 1. ((+) \<circ> f) x y \<in> R
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> insert i I; ?y3 \<in> R\<rbrakk> \<Longrightarrow> ((+) \<circ> f) ?x3 ?y3 \<in> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LCD (insert i I) R ((+) \<circ> f)

goal (6 subgoals):
 1. finite I
 2. i \<notin> I
 3. i \<in> insert i I
 4. \<zero> \<in> R
 5. I \<subseteq> insert i I
 6. (if finite (insert i I) then ((+) \<circ> f) i (foldD R ((+) \<circ> f) \<zero> I) else \<zero>) = f i + (if finite I then foldD R ((+) \<circ> f) \<zero> I else \<zero>)
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma finsum_singleton [simp]:
  assumes "f i \<in> R"
  shows "finsum {i} f = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum {i} f = f i
[PROOF STEP]
by (metis additive.right_unit assms finite.emptyI finsum_empty finsum_insert insert_absorb insert_not_empty)


[STATEMENT]
lemma ex_15:
  fixes J :: "'b set" and \<aa> :: "'b \<Rightarrow> 'a set"
  assumes "J \<noteq> {}" and J: "\<And>j. j\<in>J \<Longrightarrow> ideal (\<aa> j) R (+) (\<cdot>) \<zero> \<one>"
  shows "\<V> ({x. \<exists>I f. x = finsum I f \<and> I \<subseteq> J \<and> finite I \<and> (\<forall>i. i\<in>I \<longrightarrow> f i \<in> \<aa> i)}) = (\<Inter>j\<in>J. \<V> (\<aa> j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
have "y \<in> U"
    if j: "j \<in> J" "y \<in> \<aa> j"
      and "pr_ideal R U (+) (\<cdot>) \<zero> \<one>"
      and U: "{finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} \<subseteq> U"
    for U j y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
have "y \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> R
[PROOF STEP]
using J j ideal_implies_subset
[PROOF STATE]
proof (prove)
using this:
?j3 \<in> J \<Longrightarrow> ideal (\<aa> ?j3) R (+) (\<cdot>) \<zero> \<one>
j \<in> J
y \<in> \<aa> j
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> ?A \<subseteq> R

goal (1 subgoal):
 1. y \<in> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> R

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> R
[PROOF STEP]
have y: "y = finsum {j} (\<lambda>_. y)"
[PROOF STATE]
proof (prove)
using this:
y \<in> R

goal (1 subgoal):
 1. y = finsum {j} (\<lambda>_. y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = finsum {j} (\<lambda>_. y)

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = finsum {j} (\<lambda>_. y)
[PROOF STEP]
have "y \<in> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)}"
[PROOF STATE]
proof (prove)
using this:
y = finsum {j} (\<lambda>_. y)

goal (1 subgoal):
 1. y \<in> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y = finsum {j} (\<lambda>_. y)
j \<in> J
y \<in> \<aa> j
pr_ideal R U (+) (\<cdot>) \<zero> \<one>
{finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} \<subseteq> U

goal (1 subgoal):
 1. y \<in> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)}

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)}

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
by (rule subsetD [OF U])
[PROOF STATE]
proof (state)
this:
y \<in> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j3 \<in> J; ?y3 \<in> \<aa> ?j3; pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one>; {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} \<subseteq> ?U3\<rbrakk> \<Longrightarrow> ?y3 \<in> ?U3

goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j3 \<in> J; ?y3 \<in> \<aa> ?j3; pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one>; {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} \<subseteq> ?U3\<rbrakk> \<Longrightarrow> ?y3 \<in> ?U3

goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
have PI: "pr_ideal R x (+) (\<cdot>) \<zero> \<one>" if "\<forall>j\<in>J. pr_ideal R x (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R x (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using that assms(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>J. pr_ideal R x (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> x
J \<noteq> {}

goal (1 subgoal):
 1. pr_ideal R x (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>J. pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?x3 \<Longrightarrow> pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>J. pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?x3 \<Longrightarrow> pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
have "finsum I f \<in> U"
    if "finite I"
      and "\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U"
      and "I \<subseteq> J" "\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i" for U I f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum I f \<in> U
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
finite I
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
I \<subseteq> J
\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i

goal (1 subgoal):
 1. finsum I f \<in> U
[PROOF STEP]
proof (induction I rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; {} \<subseteq> J; \<forall>i. i \<in> {} \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum {} f \<in> U
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
{} \<subseteq> J
\<forall>i. i \<in> {} \<longrightarrow> f i \<in> \<aa> i

goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; {} \<subseteq> J; \<forall>i. i \<in> {} \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum {} f \<in> U
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
{} \<subseteq> J
\<forall>i. i \<in> {} \<longrightarrow> f i \<in> \<aa> i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
{} \<subseteq> J
\<forall>i. i \<in> {} \<longrightarrow> f i \<in> \<aa> i

goal (1 subgoal):
 1. finsum {} f \<in> U
[PROOF STEP]
using PI assms ideal_zero
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
{} \<subseteq> J
\<forall>i. i \<in> {} \<longrightarrow> f i \<in> \<aa> i
\<forall>j\<in>J. pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?x3 \<Longrightarrow> pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one>
J \<noteq> {}
?j3 \<in> J \<Longrightarrow> ideal (\<aa> ?j3) R (+) (\<cdot>) \<zero> \<one>
ideal ?A R ?add ?mult \<zero> \<one> \<Longrightarrow> \<zero> \<in> ?A

goal (1 subgoal):
 1. finsum {} f \<in> U
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
finsum {} f \<in> U

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
case (insert i I)
[PROOF STATE]
proof (state)
this:
finite I
i \<notin> I
\<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; I \<subseteq> J; \<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum I f \<in> U
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
insert i I \<subseteq> J
\<forall>ia. ia \<in> insert i I \<longrightarrow> f ia \<in> \<aa> ia

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite I
i \<notin> I
\<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; I \<subseteq> J; \<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum I f \<in> U
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
insert i I \<subseteq> J
\<forall>ia. ia \<in> insert i I \<longrightarrow> f ia \<in> \<aa> ia
[PROOF STEP]
have "finsum (insert i I) f = f i + finsum I f"
[PROOF STATE]
proof (prove)
using this:
finite I
i \<notin> I
\<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; I \<subseteq> J; \<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum I f \<in> U
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
insert i I \<subseteq> J
\<forall>ia. ia \<in> insert i I \<longrightarrow> f ia \<in> \<aa> ia

goal (1 subgoal):
 1. finsum (insert i I) f = f i + finsum I f
[PROOF STEP]
by (metis assms(2) finsum_insert ideal_implies_subset insertCI subset_iff)
[PROOF STATE]
proof (state)
this:
finsum (insert i I) f = f i + finsum I f

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
finsum (insert i I) f = f i + finsum I f

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
have "... \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i + finsum I f \<in> U
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite I
i \<notin> I
\<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; I \<subseteq> J; \<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum I f \<in> U
\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U
insert i I \<subseteq> J
\<forall>ia. ia \<in> insert i I \<longrightarrow> f ia \<in> \<aa> ia

goal (1 subgoal):
 1. f i + finsum I f \<in> U
[PROOF STEP]
by (metis ideal_add insertCI pr_ideal.axioms(2) subset_eq)
[PROOF STATE]
proof (state)
this:
f i + finsum I f \<in> U

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; F \<subseteq> J; \<forall>i. i \<in> F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum F f \<in> U; \<forall>j\<in>J. pr_ideal R U (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> U; insert x F \<subseteq> J; \<forall>i. i \<in> insert x F \<longrightarrow> f i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum (insert x F) f \<in> U
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
finsum (insert i I) f \<in> U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finsum (insert i I) f \<in> U

goal (1 subgoal):
 1. finsum (insert i I) f \<in> U
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finsum (insert i I) f \<in> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?I3; \<forall>j\<in>J. pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?U3; ?I3 \<subseteq> J; \<forall>i. i \<in> ?I3 \<longrightarrow> ?f3 i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum ?I3 ?f3 \<in> ?U3

goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?j3 \<in> J; ?y3 \<in> \<aa> ?j3; pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one>; {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} \<subseteq> ?U3\<rbrakk> \<Longrightarrow> ?y3 \<in> ?U3
\<forall>j\<in>J. pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?x3 \<Longrightarrow> pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one>
\<lbrakk>finite ?I3; \<forall>j\<in>J. pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?U3; ?I3 \<subseteq> J; \<forall>i. i \<in> ?I3 \<longrightarrow> ?f3 i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum ?I3 ?f3 \<in> ?U3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j3 \<in> J; ?y3 \<in> \<aa> ?j3; pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one>; {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} \<subseteq> ?U3\<rbrakk> \<Longrightarrow> ?y3 \<in> ?U3
\<forall>j\<in>J. pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?x3 \<Longrightarrow> pr_ideal R ?x3 (+) (\<cdot>) \<zero> \<one>
\<lbrakk>finite ?I3; \<forall>j\<in>J. pr_ideal R ?U3 (+) (\<cdot>) \<zero> \<one> \<and> \<aa> j \<subseteq> ?U3; ?I3 \<subseteq> J; \<forall>i. i \<in> ?I3 \<longrightarrow> ?f3 i \<in> \<aa> i\<rbrakk> \<Longrightarrow> finsum ?I3 ?f3 \<in> ?U3

goal (1 subgoal):
 1. \<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)
[PROOF STEP]
by (auto simp: closed_subsets_def)
[PROOF STATE]
proof (state)
this:
\<V> {finsum I f |I f. I \<subseteq> J \<and> finite I \<and> (\<forall>i. i \<in> I \<longrightarrow> f i \<in> \<aa> i)} = (\<Inter>j\<in>J. \<V> \<aa> j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_zariski_open_empty [simp]: "is_zariski_open {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open {}
[PROOF STEP]
using UNIV is_zariski_open_def generated_topology_is_topology topological_space.open_empty
[PROOF STATE]
proof (prove)
using this:
generated_topology ?S ?B ?S
is_zariski_open ?U \<equiv> generated_topology Spec {U. \<exists>\<aa>. ideal \<aa> R (+) (\<cdot>) \<zero> \<one> \<and> U = Spec\<setminus>\<V> \<aa>} ?U
topological_space ?S (generated_topology ?S ?B)
topological_space ?S ?is_open \<Longrightarrow> ?is_open {}

goal (1 subgoal):
 1. is_zariski_open {}
[PROOF STEP]
by simp


[STATEMENT]
lemma is_zariski_open_Spec [simp]: "is_zariski_open Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open Spec
[PROOF STEP]
by (simp add: UNIV is_zariski_open_def)


[STATEMENT]
lemma is_zariski_open_Union [intro]:
  "(\<And>x. x \<in> F \<Longrightarrow> is_zariski_open x) \<Longrightarrow> is_zariski_open (\<Union> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> F \<Longrightarrow> is_zariski_open x) \<Longrightarrow> is_zariski_open (\<Union> F)
[PROOF STEP]
by (simp add: UN is_zariski_open_def)


[STATEMENT]
lemma is_zariski_open_Int [simp]:
  "\<lbrakk>is_zariski_open U; is_zariski_open V\<rbrakk> \<Longrightarrow> is_zariski_open (U \<inter> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; is_zariski_open V\<rbrakk> \<Longrightarrow> is_zariski_open (U \<inter> V)
[PROOF STEP]
using Int is_zariski_open_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>generated_topology ?S ?B ?U; generated_topology ?S ?B ?V\<rbrakk> \<Longrightarrow> generated_topology ?S ?B (?U \<inter> ?V)
is_zariski_open ?U \<equiv> generated_topology Spec {U. \<exists>\<aa>. ideal \<aa> R (+) (\<cdot>) \<zero> \<one> \<and> U = Spec\<setminus>\<V> \<aa>} ?U

goal (1 subgoal):
 1. \<lbrakk>is_zariski_open U; is_zariski_open V\<rbrakk> \<Longrightarrow> is_zariski_open (U \<inter> V)
[PROOF STEP]
by blast


[STATEMENT]
lemma zariski_is_topological_space [iff]:
  shows "topological_space Spec is_zariski_open"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. topological_space Spec is_zariski_open
[PROOF STEP]
unfolding is_zariski_open_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. topological_space Spec (generated_topology Spec {U. \<exists>\<aa>. ideal \<aa> R (+) (\<cdot>) \<zero> \<one> \<and> U = Spec\<setminus>\<V> \<aa>})
[PROOF STEP]
using generated_topology_is_topology
[PROOF STATE]
proof (prove)
using this:
topological_space ?S (generated_topology ?S ?B)

goal (1 subgoal):
 1. topological_space Spec (generated_topology Spec {U. \<exists>\<aa>. ideal \<aa> R (+) (\<cdot>) \<zero> \<one> \<and> U = Spec\<setminus>\<V> \<aa>})
[PROOF STEP]
by blast


[STATEMENT]
lemma zariski_open_is_subset:
  assumes "is_zariski_open U"
  shows "U \<subseteq> Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<subseteq> Spec
[PROOF STEP]
using assms zariski_is_topological_space topological_space.open_imp_subset
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
topological_space Spec is_zariski_open
\<lbrakk>topological_space ?S ?is_open; ?is_open ?U\<rbrakk> \<Longrightarrow> ?U \<subseteq> ?S

goal (1 subgoal):
 1. U \<subseteq> Spec
[PROOF STEP]
by auto


[STATEMENT]
lemma cring0_is_zariski_open [simp]: "cring0.is_zariski_open = (\<lambda>U. U={})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring0.is_zariski_open = (\<lambda>U. U = {})
[PROOF STEP]
using cring0.cring0_spectrum_eq cring0.is_zariski_open_empty cring0.zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
cring0.spectrum = {}
cring0.is_zariski_open {}
cring0.is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> cring0.spectrum

goal (1 subgoal):
 1. cring0.is_zariski_open = (\<lambda>U. U = {})
[PROOF STEP]
by blast


[STATEMENT]
lemma standard_open_is_zariski_open:
  assumes "x \<in> R"
  shows "is_zariski_open \<D>(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open \<D>(x)
[PROOF STEP]
unfolding is_zariski_open_def standard_open_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. generated_topology Spec {U. \<exists>\<aa>. ideal \<aa> R (+) (\<cdot>) \<zero> \<one> \<and> U = Spec\<setminus>\<V> \<aa>} (Spec\<setminus>\<V> \<langle>x\<rangle>)
[PROOF STEP]
using assms gen_ideal_ideal generated_topology.simps
[PROOF STATE]
proof (prove)
using this:
x \<in> R
?x \<in> R \<Longrightarrow> ideal \<langle>?x\<rangle> R (+) (\<cdot>) \<zero> \<one>
generated_topology ?S ?B ?a = (?a = ?S \<or> (\<exists>U V. ?a = U \<inter> V \<and> generated_topology ?S ?B U \<and> generated_topology ?S ?B V) \<or> (\<exists>K. ?a = \<Union> K \<and> (\<forall>x. x \<in> K \<longrightarrow> generated_topology ?S ?B x)) \<or> (\<exists>b. ?a = b \<and> b \<in> ?B \<and> b \<subseteq> ?S))

goal (1 subgoal):
 1. generated_topology Spec {U. \<exists>\<aa>. ideal \<aa> R (+) (\<cdot>) \<zero> \<one> \<and> U = Spec\<setminus>\<V> \<aa>} (Spec\<setminus>\<V> \<langle>x\<rangle>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma standard_open_is_subset:
  assumes "x \<in> R"
  shows "\<D>(x) \<subseteq> Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>(x) \<subseteq> Spec
[PROOF STEP]
by (simp add: assms standard_open_is_zariski_open zariski_open_is_subset)


[STATEMENT]
lemma belongs_standard_open_iff:
  assumes "x \<in> R" and "\<pp> \<in> Spec"
  shows "x \<notin> \<pp> \<longleftrightarrow> \<pp> \<in> \<D>(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> \<pp>) = (\<pp> \<in> \<D>(x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> R
\<pp> \<in> Spec

goal (1 subgoal):
 1. (x \<notin> \<pp>) = (\<pp> \<in> \<D>(x))
[PROOF STEP]
apply (auto simp: standard_open_def closed_subsets_def spectrum_def gen_ideal_def subset_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> R; pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>; x \<notin> \<pp>\<rbrakk> \<Longrightarrow> \<exists>t. (\<exists>r\<in>R. t = r \<cdot> x) \<and> t \<notin> \<pp>
 2. \<And>r. \<lbrakk>x \<in> R; pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>; r \<cdot> x \<notin> \<pp>; r \<in> R; x \<in> \<pp>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis pr_ideal.absorbent)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>x \<in> R; pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>; r \<cdot> x \<notin> \<pp>; r \<in> R; x \<in> \<pp>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (meson ideal.ideal(1) pr_ideal_def)


[STATEMENT]
lemma is_ring_from_is_homomorphism:
  shows "\<And>U. is_open U \<Longrightarrow> ring (\<FF> U) (+\<^bsub>U\<^esub>) (\<cdot>\<^bsub>U\<^esub>) \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
using is_ring_morphism ring_homomorphism.axioms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
ring_homomorphism ?\<eta> ?R ?addition ?multiplication ?zero ?unit ?R' ?addition' ?multiplication' ?zero' ?unit' \<Longrightarrow> ring ?R ?addition ?multiplication ?zero ?unit

goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma is_map_from_is_homomorphism:
  assumes "is_open U" and "is_open V" and "V \<subseteq> U"
  shows "Set_Theory.map (\<rho> U V) (\<FF> U) (\<FF> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (\<rho> U V) (\<FF> U) (\<FF> V)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open V
V \<subseteq> U

goal (1 subgoal):
 1. Set_Theory.map (\<rho> U V) (\<FF> U) (\<FF> V)
[PROOF STEP]
by (meson is_ring_morphism ring_homomorphism.axioms(1))


[STATEMENT]
lemma eq_\<rho>:
  assumes "is_open U" and "is_open V" and "is_open W" and "W \<subseteq> U \<inter> V" and "s \<in> \<FF> U" and "t \<in> \<FF> V"
    and "\<rho> U W s = \<rho> V W t" and "is_open W'" and "W' \<subseteq> W"
  shows "\<rho> U W' s = \<rho> V W' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> U W' s = \<rho> V W' t
[PROOF STEP]
by (metis Int_subset_iff assms assoc_comp comp_apply)


[STATEMENT]
lemma fam_morphisms_are_maps:
  assumes "is_open U"
  shows "Set_Theory.map (fam_morphisms U) (\<FF> U) (\<FF>' U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (fam_morphisms U) (\<FF> U) (\<FF>' U)
[PROOF STEP]
using assms is_ring_morphism
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open ?U \<Longrightarrow> ring_homomorphism (fam_morphisms ?U) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF>' ?U) +'\<^bsub>?U\<^esub> \<cdot>'\<^bsub>?U\<^esub> \<zero>'\<^bsub>?U\<^esub> \<one>'\<^bsub>?U\<^esub>

goal (1 subgoal):
 1. Set_Theory.map (fam_morphisms U) (\<FF> U) (\<FF>' U)
[PROOF STEP]
by (simp add: ring_homomorphism_def)


[STATEMENT]
lemma (in presheaf_of_rings) id_is_mor_pr_rngs:
  shows "morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof (intro morphism_presheaves_of_rings.intro morphism_presheaves_of_rings_axioms.intro)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 3. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 4. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
show "\<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U))
                                            (\<FF> U) (add_str U) (mult_str U) (zero_str U) (one_str U)
                                            (\<FF> U) (add_str U) (mult_str U) (zero_str U) (one_str U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by (metis identity_map is_map_from_is_homomorphism is_ring_morphism restrict_ext restrict_on_source subset_eq)
[PROOF STATE]
proof (state)
this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub>

goal (3 subgoals):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 3. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
show "\<And>U V. \<lbrakk>is_open U; is_open V; V \<subseteq> U\<rbrakk>
           \<Longrightarrow> (\<And>x. x \<in> (\<FF> U) \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V. \<lbrakk>is_open U; is_open V; V \<subseteq> U\<rbrakk> \<Longrightarrow> (\<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)
[PROOF STEP]
using map.map_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Set_Theory.map ?\<alpha> ?S ?T; ?a \<in> ?S\<rbrakk> \<Longrightarrow> ?\<alpha> ?a \<in> ?T

goal (1 subgoal):
 1. \<And>U V. \<lbrakk>is_open U; is_open V; V \<subseteq> U\<rbrakk> \<Longrightarrow> (\<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)
[PROOF STEP]
by (metis comp_apply is_map_from_is_homomorphism restrict_apply')
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_open ?U1; is_open ?V1; ?V1 \<subseteq> ?U1; ?x1 \<in> \<FF> ?U1\<rbrakk> \<Longrightarrow> (\<rho> ?U1 ?V1 \<circ> identity (\<FF> ?U1)) ?x1 = (identity (\<FF> ?V1) \<circ> \<rho> ?U1 ?V1) ?x1

goal (2 subgoals):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
[PROOF STEP]
qed (use presheaf_of_rings_axioms in auto)


[STATEMENT]
lemma comp_ring_morphisms:
  assumes "ring_homomorphism \<eta> A addA multA zeroA oneA B addB multB zeroB oneB"
and "ring_homomorphism \<theta> B addB multB zeroB oneB C addC multC zeroC oneC"
shows "ring_homomorphism (compose A \<theta> \<eta>) A addA multA zeroA oneA C addC multC zeroC oneC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<theta> \<circ> \<eta> \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
using comp_monoid_morphisms comp_group_morphisms assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>monoid_homomorphism ?\<eta> ?A ?multA ?oneA ?B ?multB ?oneB; monoid_homomorphism ?\<theta> ?B ?multB ?oneB ?C ?multC ?oneC\<rbrakk> \<Longrightarrow> monoid_homomorphism (?\<theta> \<circ> ?\<eta> \<down> ?A) ?A ?multA ?oneA ?C ?multC ?oneC
\<lbrakk>group_homomorphism ?\<eta> ?A ?multA ?oneA ?B ?multB ?oneB; group_homomorphism ?\<theta> ?B ?multB ?oneB ?C ?multC ?oneC\<rbrakk> \<Longrightarrow> group_homomorphism (?\<theta> \<circ> ?\<eta> \<down> ?A) ?A ?multA ?oneA ?C ?multC ?oneC
ring_homomorphism \<eta> A addA multA zeroA oneA B addB multB zeroB oneB
ring_homomorphism \<theta> B addB multB zeroB oneB C addC multC zeroC oneC

goal (1 subgoal):
 1. ring_homomorphism (\<theta> \<circ> \<eta> \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
by (metis monoid_homomorphism_def ring_homomorphism_def)


[STATEMENT]
lemma comp_of_presheaves:
  assumes 1: "morphism_presheaves_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF>' \<rho>' b' add_str' mult_str' zero_str' one_str' \<phi>"
    and 2: "morphism_presheaves_of_rings X is_open \<FF>' \<rho>' b' add_str' mult_str' zero_str' one_str' \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str'' \<phi>'"
  shows "morphism_presheaves_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str'' (\<lambda>U. (\<phi>' U \<circ> \<phi> U \<down> \<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str'' (\<lambda>U. \<phi>' U \<circ> \<phi> U \<down> \<FF> U)
[PROOF STEP]
proof (intro morphism_presheaves_of_rings.intro morphism_presheaves_of_rings_axioms.intro)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. presheaf_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings X is_open \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str''
 3. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (\<phi>' U \<circ> \<phi> U \<down> \<FF> U) (\<FF> U) (add_str U) (mult_str U) (zero_str U) (one_str U) (\<FF>'' U) (add_str'' U) (mult_str'' U) (zero_str'' U) (one_str'' U)
 4. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
show "ring_homomorphism (\<phi>' U \<circ> \<phi> U \<down> \<FF> U) (\<FF> U) (add_str U) (mult_str U) (zero_str U) (one_str U) (\<FF>'' U) (add_str'' U) (mult_str'' U) (zero_str'' U) (one_str'' U)"
    if "is_open U"
    for U :: "'a set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<phi>' U \<circ> \<phi> U \<down> \<FF> U) (\<FF> U) (add_str U) (mult_str U) (zero_str U) (one_str U) (\<FF>'' U) (add_str'' U) (mult_str'' U) (zero_str'' U) (one_str'' U)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
is_open U

goal (1 subgoal):
 1. ring_homomorphism (\<phi>' U \<circ> \<phi> U \<down> \<FF> U) (\<FF> U) (add_str U) (mult_str U) (zero_str U) (one_str U) (\<FF>'' U) (add_str'' U) (mult_str'' U) (zero_str'' U) (one_str'' U)
[PROOF STEP]
by (metis assms comp_ring_morphisms morphism_presheaves_of_rings.is_ring_morphism)
[PROOF STATE]
proof (state)
this:
is_open ?U \<Longrightarrow> ring_homomorphism (\<phi>' ?U \<circ> \<phi> ?U \<down> \<FF> ?U) (\<FF> ?U) (add_str ?U) (mult_str ?U) (zero_str ?U) (one_str ?U) (\<FF>'' ?U) (add_str'' ?U) (mult_str'' ?U) (zero_str'' ?U) (one_str'' ?U)

goal (3 subgoals):
 1. presheaf_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings X is_open \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str''
 3. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. presheaf_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings X is_open \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str''
 3. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
show "\<And>x. x \<in> (\<FF> U) \<Longrightarrow> (\<rho>'' U V \<circ> (\<phi>' U \<circ> \<phi> U \<down> \<FF> U)) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x"
    if "is_open U" "is_open V" "V \<subseteq> U" for U V
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open V
V \<subseteq> U

goal (1 subgoal):
 1. \<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
using morphism_presheaves_of_rings.comm_diagrams [OF 1]
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open V
V \<subseteq> U
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U; ?x \<in> \<FF> ?U\<rbrakk> \<Longrightarrow> (\<rho>' ?U ?V \<circ> \<phi> ?U) ?x = (\<phi> ?V \<circ> \<rho> ?U ?V) ?x

goal (1 subgoal):
 1. \<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
using morphism_presheaves_of_rings.comm_diagrams [OF 2]
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open V
V \<subseteq> U
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U; ?x \<in> \<FF> ?U\<rbrakk> \<Longrightarrow> (\<rho>' ?U ?V \<circ> \<phi> ?U) ?x = (\<phi> ?V \<circ> \<rho> ?U ?V) ?x
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U; ?x \<in> \<FF>' ?U\<rbrakk> \<Longrightarrow> (\<rho>'' ?U ?V \<circ> \<phi>' ?U) ?x = (\<phi>' ?V \<circ> \<rho>' ?U ?V) ?x

goal (1 subgoal):
 1. \<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
using presheaf_of_rings.is_map_from_is_homomorphism [OF morphism_presheaves_of_rings.axioms(1) [OF 1]]
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open V
V \<subseteq> U
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U; ?x \<in> \<FF> ?U\<rbrakk> \<Longrightarrow> (\<rho>' ?U ?V \<circ> \<phi> ?U) ?x = (\<phi> ?V \<circ> \<rho> ?U ?V) ?x
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U; ?x \<in> \<FF>' ?U\<rbrakk> \<Longrightarrow> (\<rho>'' ?U ?V \<circ> \<phi>' ?U) ?x = (\<phi>' ?V \<circ> \<rho>' ?U ?V) ?x
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (\<rho> ?U ?V) (\<FF> ?U) (\<FF> ?V)

goal (1 subgoal):
 1. \<And>x. x \<in> \<FF> U \<Longrightarrow> (\<rho>'' U V \<circ> \<phi>' U \<circ> \<phi> U \<down> \<FF> U) x = (\<phi>' V \<circ> \<phi> V \<down> \<FF> V \<circ> \<rho> U V) x
[PROOF STEP]
by (metis "1" comp_apply compose_eq map.map_closed morphism_presheaves_of_rings.fam_morphisms_are_maps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_open ?U1; is_open ?V1; ?V1 \<subseteq> ?U1; ?x \<in> \<FF> ?U1\<rbrakk> \<Longrightarrow> (\<rho>'' ?U1 ?V1 \<circ> \<phi>' ?U1 \<circ> \<phi> ?U1 \<down> \<FF> ?U1) ?x = (\<phi>' ?V1 \<circ> \<phi> ?V1 \<down> \<FF> ?V1 \<circ> \<rho> ?U1 ?V1) ?x

goal (2 subgoals):
 1. presheaf_of_rings X is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. presheaf_of_rings X is_open \<FF>'' \<rho>'' b'' add_str'' mult_str'' zero_str'' one_str''
[PROOF STEP]
qed (use assms in \<open>auto simp: morphism_presheaves_of_rings_def\<close>)


[STATEMENT]
lemma ind_is_open_imp_ring:
  "\<And>U. it.ind_is_open U
   \<Longrightarrow> ring (ind_sheaf U) (ind_add_str U) (ind_mult_str U) (ind_zero_str U) (ind_one_str U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. it.ind_is_open U \<Longrightarrow> ring (local.ind_sheaf U) (ind_add_str U) (ind_mult_str U) (ind_zero_str U) (ind_one_str U)
[PROOF STEP]
unfolding ind_add_str_def it.ind_is_open_def ind_mult_str_def ind_one_str_def ind_sheaf_def ind_zero_str_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ua. Ua \<subseteq> U \<and> (\<exists>V\<subseteq>S. is_open V \<and> Ua = U \<inter> V) \<Longrightarrow> ring (\<FF> (U \<inter> Ua)) +\<^bsub>U \<inter> Ua\<^esub> \<cdot>\<^bsub>U \<inter> Ua\<^esub> \<zero>\<^bsub>U \<inter> Ua\<^esub> \<one>\<^bsub>U \<inter> Ua\<^esub>
[PROOF STEP]
using is_open_subset is_ring_from_is_homomorphism it.is_subset open_inter
[PROOF STATE]
proof (prove)
using this:
is_open U
is_open ?U \<Longrightarrow> ring (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub>
U \<subseteq> S
\<lbrakk>is_open ?U; is_open ?V\<rbrakk> \<Longrightarrow> is_open (?U \<inter> ?V)

goal (1 subgoal):
 1. \<And>Ua. Ua \<subseteq> U \<and> (\<exists>V\<subseteq>S. is_open V \<and> Ua = U \<inter> V) \<Longrightarrow> ring (\<FF> (U \<inter> Ua)) +\<^bsub>U \<inter> Ua\<^esub> \<cdot>\<^bsub>U \<inter> Ua\<^esub> \<zero>\<^bsub>U \<inter> Ua\<^esub> \<one>\<^bsub>U \<inter> Ua\<^esub>
[PROOF STEP]
by force