[STATEMENT]
lemma (in pr_ideal) local_ring_at_is_local:
  shows "local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
interpret cq: quotient_ring "R\<setminus>I" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>I) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (simp add: Comm_Ring.quotient_ring_def comm.comm_ring_axioms submonoid_pr_ideal)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
define \<ww> where "\<ww> \<equiv> {quotient_ring.frac (R\<setminus>I) R (+) (\<cdot>) \<zero> r s| r s. r \<in> I \<and> s \<in> (R \<setminus> I)}"
    \<comment>\<open>Now every proper ideal of @{term "R\<setminus>I"} is included in @{term \<ww>}, and the result follows trivially\<close>
[PROOF STATE]
proof (state)
this:
\<ww> \<equiv> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
have maximal: "\<aa> \<subseteq> \<ww>"
    if "lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at"
      and ne: "\<aa> \<noteq> carrier_local_ring_at" for \<aa>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aa> \<subseteq> \<ww>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<aa> \<Longrightarrow> x \<in> \<ww>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<aa> \<Longrightarrow> x \<in> \<ww>
[PROOF STEP]
interpret \<aa>: lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
\<aa> \<noteq> carrier_local_ring_at

goal (1 subgoal):
 1. lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<aa> \<Longrightarrow> x \<in> \<ww>
[PROOF STEP]
assume "x \<in> \<aa>"
[PROOF STATE]
proof (state)
this:
x \<in> \<aa>

goal (1 subgoal):
 1. \<And>x. x \<in> \<aa> \<Longrightarrow> x \<in> \<ww>
[PROOF STEP]
have "False" if "x \<notin> \<ww>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
obtain r s where "r \<in> R" "s \<in> R" "s \<notin> I" "r \<notin> I" "x = cq.frac r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; r \<notin> I; x = cq.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_from_carrier_local \<open>x \<in> \<aa>\<close> \<open>x \<notin> \<ww>\<close> [unfolded \<ww>_def, simplified]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> carrier_local_ring_at; \<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; ?X = cq.frac r s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
x \<in> \<aa>
\<forall>r s. s \<in> R \<longrightarrow> r \<in> I \<longrightarrow> x = cq.frac r s \<longrightarrow> s \<in> I

goal (1 subgoal):
 1. (\<And>r s. \<lbrakk>r \<in> R; s \<in> R; s \<notin> I; r \<notin> I; x = cq.frac r s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<aa>.additive.sub)
[PROOF STATE]
proof (state)
this:
r \<in> R
s \<in> R
s \<notin> I
r \<notin> I
x = cq.frac r s

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
s \<in> R
s \<notin> I
r \<notin> I
x = cq.frac r s
[PROOF STEP]
have sr: "cq.frac s r \<in> carrier_local_ring_at"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
s \<in> R
s \<notin> I
r \<notin> I
x = cq.frac r s

goal (1 subgoal):
 1. cq.frac s r \<in> carrier_local_ring_at
[PROOF STEP]
by (simp add: \<open>r \<in> R\<close> \<open>s \<in> R\<close> carrier_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
cq.frac s r \<in> carrier_local_ring_at

goal (1 subgoal):
 1. False
[PROOF STEP]
have [simp]: "r \<cdot> s \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<cdot> s \<notin> I
[PROOF STEP]
using \<open>r \<in> R\<close> \<open>r \<notin> I\<close> \<open>s \<in> R\<close> \<open>s \<notin> I\<close> absorbent
[PROOF STATE]
proof (prove)
using this:
r \<in> R
r \<notin> I
s \<in> R
s \<notin> I
\<lbrakk>?x \<in> R; ?y \<in> R; ?x \<cdot> ?y \<in> I\<rbrakk> \<Longrightarrow> ?x \<in> I \<or> ?y \<in> I

goal (1 subgoal):
 1. r \<cdot> s \<notin> I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<cdot> s \<notin> I

goal (1 subgoal):
 1. False
[PROOF STEP]
have "one_local_ring_at = cq.frac \<one> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_local_ring_at = cq.frac \<one> \<one>
[PROOF STEP]
by (simp add: one_local_ring_at_def cq.one_rel_def)
[PROOF STATE]
proof (state)
this:
one_local_ring_at = cq.frac \<one> \<one>

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
one_local_ring_at = cq.frac \<one> \<one>

goal (1 subgoal):
 1. False
[PROOF STEP]
have "... = cq.frac (s \<cdot> r) (r \<cdot> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.frac \<one> \<one> = cq.frac (s \<cdot> r) (r \<cdot> s)
[PROOF STEP]
using \<open>r \<in> R\<close> \<open>r \<notin> I\<close> \<open>s \<in> R\<close> \<open>s \<notin> I\<close>
[PROOF STATE]
proof (prove)
using this:
r \<in> R
r \<notin> I
s \<in> R
s \<notin> I

goal (1 subgoal):
 1. cq.frac \<one> \<one> = cq.frac (s \<cdot> r) (r \<cdot> s)
[PROOF STEP]
by (intro cq.frac_eqI [of \<one>]) (auto simp: comm.comm_mult)
[PROOF STATE]
proof (state)
this:
cq.frac \<one> \<one> = cq.frac (s \<cdot> r) (r \<cdot> s)

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cq.frac \<one> \<one> = cq.frac (s \<cdot> r) (r \<cdot> s)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "... = cq.mult_rel (cq.frac s r) (cq.frac r s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.frac (s \<cdot> r) (r \<cdot> s) = cq.mult_rel (cq.frac s r) (cq.frac r s)
[PROOF STEP]
using  \<open>r \<in> R\<close> \<open>r \<notin> I\<close> \<open>s \<in> R\<close> \<open>s \<notin> I\<close>
[PROOF STATE]
proof (prove)
using this:
r \<in> R
r \<notin> I
s \<in> R
s \<notin> I

goal (1 subgoal):
 1. cq.frac (s \<cdot> r) (r \<cdot> s) = cq.mult_rel (cq.frac s r) (cq.frac r s)
[PROOF STEP]
by (simp add: cq.mult_rel_frac)
[PROOF STATE]
proof (state)
this:
cq.frac (s \<cdot> r) (r \<cdot> s) = cq.mult_rel (cq.frac s r) (cq.frac r s)

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cq.frac (s \<cdot> r) (r \<cdot> s) = cq.mult_rel (cq.frac s r) (cq.frac r s)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<dots> = mult_local_ring_at (cq.frac s r) (cq.frac r s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.mult_rel (cq.frac s r) (cq.frac r s) = mult_local_ring_at (cq.frac s r) (cq.frac r s)
[PROOF STEP]
using mult_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
mult_local_ring_at \<equiv> cq.mult_rel

goal (1 subgoal):
 1. cq.mult_rel (cq.frac s r) (cq.frac r s) = mult_local_ring_at (cq.frac s r) (cq.frac r s)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
cq.mult_rel (cq.frac s r) (cq.frac r s) = mult_local_ring_at (cq.frac s r) (cq.frac r s)

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cq.mult_rel (cq.frac s r) (cq.frac r s) = mult_local_ring_at (cq.frac s r) (cq.frac r s)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "... \<in> \<aa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_local_ring_at (cq.frac s r) (cq.frac r s) \<in> \<aa>
[PROOF STEP]
using \<aa>.lideal \<open>x = cq.frac r s\<close> \<open>x \<in> \<aa>\<close> sr
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> carrier_local_ring_at; ?a \<in> \<aa>\<rbrakk> \<Longrightarrow> mult_local_ring_at ?r ?a \<in> \<aa>
x = cq.frac r s
x \<in> \<aa>
cq.frac s r \<in> carrier_local_ring_at

goal (1 subgoal):
 1. mult_local_ring_at (cq.frac s r) (cq.frac r s) \<in> \<aa>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mult_local_ring_at (cq.frac s r) (cq.frac r s) \<in> \<aa>

goal (1 subgoal):
 1. False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
one_local_ring_at \<in> \<aa>
[PROOF STEP]
have "one_local_ring_at \<in> \<aa>"
[PROOF STATE]
proof (prove)
using this:
one_local_ring_at \<in> \<aa>

goal (1 subgoal):
 1. one_local_ring_at \<in> \<aa>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
one_local_ring_at \<in> \<aa>

goal (1 subgoal):
 1. False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
one_local_ring_at \<in> \<aa>

goal (1 subgoal):
 1. False
[PROOF STEP]
using ne \<aa>.has_one_imp_equal
[PROOF STATE]
proof (prove)
using this:
one_local_ring_at \<in> \<aa>
\<aa> \<noteq> carrier_local_ring_at
one_local_ring_at \<in> \<aa> \<Longrightarrow> \<aa> = carrier_local_ring_at

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<notin> \<ww> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>x. x \<in> \<aa> \<Longrightarrow> x \<in> \<ww>
[PROOF STEP]
thus "x \<in> \<ww>"
[PROOF STATE]
proof (prove)
using this:
x \<notin> \<ww> \<Longrightarrow> False

goal (1 subgoal):
 1. x \<in> \<ww>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<ww>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>lideal ?\<aa>3 carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; ?\<aa>3 \<noteq> carrier_local_ring_at\<rbrakk> \<Longrightarrow> ?\<aa>3 \<subseteq> \<ww>

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
have uminus_closed: "uminus_local_ring_at u \<in> \<ww>" if "u \<in> \<ww>" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_local_ring_at u \<in> \<ww>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
u \<in> \<ww>

goal (1 subgoal):
 1. uminus_local_ring_at u \<in> \<ww>
[PROOF STEP]
by (force simp: \<ww>_def cq.uminus_rel_frac uminus_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
?u3 \<in> \<ww> \<Longrightarrow> uminus_local_ring_at ?u3 \<in> \<ww>

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
have add_closed: "add_local_ring_at a b \<in> \<ww>" if "a \<in> \<ww>" "b \<in> \<ww>" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
obtain ra sa rb sb where ab: "a = cq.frac ra sa" "b = cq.frac rb sb"
      and "ra \<in> I" "rb \<in> I" "sa \<in> R" "sa \<notin> I" "sb \<in> R" "sb \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ra sa rb sb. \<lbrakk>a = cq.frac ra sa; b = cq.frac rb sb; ra \<in> I; rb \<in> I; sa \<in> R; sa \<notin> I; sb \<in> R; sb \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>a \<in> \<ww>\<close> \<open>b \<in> \<ww>\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> \<ww>
b \<in> \<ww>

goal (1 subgoal):
 1. (\<And>ra sa rb sb. \<lbrakk>a = cq.frac ra sa; b = cq.frac rb sb; ra \<in> I; rb \<in> I; sa \<in> R; sa \<notin> I; sb \<in> R; sb \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<ww>_def)
[PROOF STATE]
proof (state)
this:
a = cq.frac ra sa
b = cq.frac rb sb
ra \<in> I
rb \<in> I
sa \<in> R
sa \<notin> I
sb \<in> R
sb \<notin> I

goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = cq.frac ra sa
b = cq.frac rb sb
ra \<in> I
rb \<in> I
sa \<in> R
sa \<notin> I
sb \<in> R
sb \<notin> I
[PROOF STEP]
have "add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)"
[PROOF STATE]
proof (prove)
using this:
a = cq.frac ra sa
b = cq.frac rb sb
ra \<in> I
rb \<in> I
sa \<in> R
sa \<notin> I
sb \<in> R
sb \<notin> I

goal (1 subgoal):
 1. add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)
[PROOF STEP]
by (force simp add: cq.add_rel_frac add_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)

goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)

goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
have "ra \<cdot> sb + rb \<cdot> sa \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ra \<cdot> sb + rb \<cdot> sa \<in> I
[PROOF STEP]
by (simp add: \<open>ra \<in> I\<close> \<open>rb \<in> I\<close> \<open>sa \<in> R\<close> \<open>sb \<in> R\<close> ideal(2))
[PROOF STATE]
proof (state)
this:
ra \<cdot> sb + rb \<cdot> sa \<in> I

goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)
ra \<cdot> sb + rb \<cdot> sa \<in> I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)
ra \<cdot> sb + rb \<cdot> sa \<in> I

goal (1 subgoal):
 1. add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
unfolding \<ww>_def
[PROOF STATE]
proof (prove)
using this:
add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)
ra \<cdot> sb + rb \<cdot> sa \<in> I

goal (1 subgoal):
 1. add_local_ring_at a b \<in> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}
[PROOF STEP]
using \<open>sa \<in> R\<close> \<open>sa \<notin> I\<close> \<open>sb \<in> R\<close> \<open>sb \<notin> I\<close> ab absorbent
[PROOF STATE]
proof (prove)
using this:
add_local_ring_at (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> sb + rb \<cdot> sa) (sa \<cdot> sb)
ra \<cdot> sb + rb \<cdot> sa \<in> I
sa \<in> R
sa \<notin> I
sb \<in> R
sb \<notin> I
a = cq.frac ra sa
b = cq.frac rb sb
\<lbrakk>?x \<in> R; ?y \<in> R; ?x \<cdot> ?y \<in> I\<rbrakk> \<Longrightarrow> ?x \<in> I \<or> ?y \<in> I

goal (1 subgoal):
 1. add_local_ring_at a b \<in> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
add_local_ring_at a b \<in> \<ww>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> \<ww>; ?b3 \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at ?a3 ?b3 \<in> \<ww>

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
interpret \<ww>: lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms \<ww> carrier_local_ring_at add_local_ring_at zero_local_ring_at
 2. Group_Theory.monoid \<ww> add_local_ring_at zero_local_ring_at
 3. Group_Theory.group_axioms \<ww> add_local_ring_at zero_local_ring_at
 4. lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at
[PROOF STEP]
show subm: "submonoid_axioms \<ww> carrier_local_ring_at add_local_ring_at zero_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms \<ww> carrier_local_ring_at add_local_ring_at zero_local_ring_at
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<ww> \<subseteq> carrier_local_ring_at
 2. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 3. zero_local_ring_at \<in> \<ww>
[PROOF STEP]
show "\<ww> \<subseteq> carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ww> \<subseteq> carrier_local_ring_at
[PROOF STEP]
using \<ww>_def comm.comm_ring_axioms comm.frac_in_carrier_local comm_ring.spectrum_def pr_ideal_axioms
[PROOF STATE]
proof (prove)
using this:
\<ww> \<equiv> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}
comm_ring R (+) (\<cdot>) \<zero> \<one>
\<lbrakk>?\<pp> \<in> Spec; ?r \<in> R; ?s \<in> R; ?s \<notin> ?\<pp>\<rbrakk> \<Longrightarrow> quotient_ring.frac (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> ?r ?s \<in> R \<^bsub>?\<pp> (+) (\<cdot>) \<zero>\<^esub>
comm_ring ?R ?addition ?multiplication ?zero ?unit \<Longrightarrow> comm_ring.spectrum ?R ?addition ?multiplication ?zero ?unit \<equiv> {I. pr_ideal ?R I ?addition ?multiplication ?zero ?unit}
pr_ideal R I (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. \<ww> \<subseteq> carrier_local_ring_at
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<ww> \<subseteq> carrier_local_ring_at

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. zero_local_ring_at \<in> \<ww>
[PROOF STEP]
show "zero_local_ring_at \<in> \<ww>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_local_ring_at \<in> \<ww>
[PROOF STEP]
using \<ww>_def comm.spectrum_def comm.spectrum_imp_cxt_quotient_ring not_1 pr_ideal_axioms quotient_ring.zero_rel_def zero_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
\<ww> \<equiv> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
?\<pp> \<in> Spec \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> \<one>
\<one> \<notin> I
pr_ideal R I (+) (\<cdot>) \<zero> \<one>
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<Longrightarrow> quotient_ring.zero_rel ?S ?R ?addition ?multiplication ?zero ?unit = quotient_ring.frac ?S ?R ?addition ?multiplication ?zero ?zero ?unit
zero_local_ring_at \<equiv> cq.zero_rel

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
qed (auto simp: add_closed)
[PROOF STATE]
proof (state)
this:
submonoid_axioms \<ww> carrier_local_ring_at add_local_ring_at zero_local_ring_at

goal (3 subgoals):
 1. Group_Theory.monoid \<ww> add_local_ring_at zero_local_ring_at
 2. Group_Theory.group_axioms \<ww> add_local_ring_at zero_local_ring_at
 3. lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at
[PROOF STEP]
show mon: "Group_Theory.monoid \<ww> add_local_ring_at zero_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid \<ww> add_local_ring_at zero_local_ring_at
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. zero_local_ring_at \<in> \<ww>
 3. \<And>a b c. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>; c \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)
 4. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 5. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
show "zero_local_ring_at \<in> \<ww>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_local_ring_at \<in> \<ww>
[PROOF STEP]
by (meson subm submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
zero_local_ring_at \<in> \<ww>

goal (4 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a b c. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>; c \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 4. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a b c. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>; c \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 4. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a b c. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>; c \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 4. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
assume "a \<in> \<ww>" "b \<in> \<ww>" "c \<in> \<ww>"
[PROOF STATE]
proof (state)
this:
a \<in> \<ww>
b \<in> \<ww>
c \<in> \<ww>

goal (4 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a b c. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>; c \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 4. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<ww>
b \<in> \<ww>
c \<in> \<ww>
[PROOF STEP]
show "add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<ww>
b \<in> \<ww>
c \<in> \<ww>

goal (1 subgoal):
 1. add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)
[PROOF STEP]
by (meson additive.associative in_mono subm submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
add_local_ring_at (add_local_ring_at a b) c = add_local_ring_at a (add_local_ring_at b c)

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
assume "a \<in> \<ww>"
[PROOF STATE]
proof (state)
this:
a \<in> \<ww>

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at zero_local_ring_at a = a
 3. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
show "add_local_ring_at zero_local_ring_at a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_local_ring_at zero_local_ring_at a = a
[PROOF STEP]
by (meson \<open>a \<in> \<ww>\<close> subm additive.left_unit in_mono submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
add_local_ring_at zero_local_ring_at a = a

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
 2. \<And>a. a \<in> \<ww> \<Longrightarrow> add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
show "add_local_ring_at a zero_local_ring_at = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_local_ring_at a zero_local_ring_at = a
[PROOF STEP]
by (meson \<open>a \<in> \<ww>\<close> additive.right_unit in_mono subm submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
add_local_ring_at a zero_local_ring_at = a

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<ww>; b \<in> \<ww>\<rbrakk> \<Longrightarrow> add_local_ring_at a b \<in> \<ww>
[PROOF STEP]
qed (auto simp: add_closed)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid \<ww> add_local_ring_at zero_local_ring_at

goal (2 subgoals):
 1. Group_Theory.group_axioms \<ww> add_local_ring_at zero_local_ring_at
 2. lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at
[PROOF STEP]
show "Group_Theory.group_axioms \<ww> add_local_ring_at zero_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms \<ww> add_local_ring_at zero_local_ring_at
[PROOF STEP]
proof unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> \<ww> \<Longrightarrow> monoid.invertible \<ww> add_local_ring_at zero_local_ring_at u
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> \<ww> \<Longrightarrow> monoid.invertible \<ww> add_local_ring_at zero_local_ring_at u
[PROOF STEP]
assume "u \<in> \<ww>"
[PROOF STATE]
proof (state)
this:
u \<in> \<ww>

goal (1 subgoal):
 1. \<And>u. u \<in> \<ww> \<Longrightarrow> monoid.invertible \<ww> add_local_ring_at zero_local_ring_at u
[PROOF STEP]
show "monoid.invertible \<ww> add_local_ring_at zero_local_ring_at u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible \<ww> add_local_ring_at zero_local_ring_at u
[PROOF STEP]
proof (rule monoid.invertibleI [OF mon])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. add_local_ring_at u ?v = zero_local_ring_at
 2. add_local_ring_at ?v u = zero_local_ring_at
 3. u \<in> \<ww>
 4. ?v \<in> \<ww>
[PROOF STEP]
show "add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at
[PROOF STEP]
using \<open>u \<in> \<ww>\<close>
[PROOF STATE]
proof (prove)
using this:
u \<in> \<ww>

goal (1 subgoal):
 1. add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at
[PROOF STEP]
apply (clarsimp simp add: \<ww>_def add_local_ring_at_def zero_local_ring_at_def uminus_local_ring_at_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>u = cq.frac r s; r \<in> I; s \<in> R; s \<notin> I\<rbrakk> \<Longrightarrow> cq.add_rel (cq.frac r s) (cq.uminus_rel (cq.frac r s)) = cq.zero_rel
[PROOF STEP]
by (metis Diff_iff  additive.submonoid_axioms cq.add_minus_zero_rel cq.valid_frac_def submonoid.sub)
[PROOF STATE]
proof (state)
this:
add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at

goal (3 subgoals):
 1. add_local_ring_at (uminus_local_ring_at u) u = zero_local_ring_at
 2. u \<in> \<ww>
 3. uminus_local_ring_at u \<in> \<ww>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at
[PROOF STEP]
show "add_local_ring_at (uminus_local_ring_at u) u = zero_local_ring_at"
[PROOF STATE]
proof (prove)
using this:
add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at

goal (1 subgoal):
 1. add_local_ring_at (uminus_local_ring_at u) u = zero_local_ring_at
[PROOF STEP]
using subm
[PROOF STATE]
proof (prove)
using this:
add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at
submonoid_axioms \<ww> carrier_local_ring_at add_local_ring_at zero_local_ring_at

goal (1 subgoal):
 1. add_local_ring_at (uminus_local_ring_at u) u = zero_local_ring_at
[PROOF STEP]
unfolding submonoid_axioms_def
[PROOF STATE]
proof (prove)
using this:
add_local_ring_at u (uminus_local_ring_at u) = zero_local_ring_at
\<ww> \<subseteq> carrier_local_ring_at \<and> (\<forall>a b. a \<in> \<ww> \<longrightarrow> b \<in> \<ww> \<longrightarrow> add_local_ring_at a b \<in> \<ww>) \<and> zero_local_ring_at \<in> \<ww>

goal (1 subgoal):
 1. add_local_ring_at (uminus_local_ring_at u) u = zero_local_ring_at
[PROOF STEP]
by (simp add: \<open>u \<in> \<ww>\<close> additive.commutative subset_iff uminus_closed)
[PROOF STATE]
proof (state)
this:
add_local_ring_at (uminus_local_ring_at u) u = zero_local_ring_at

goal (2 subgoals):
 1. u \<in> \<ww>
 2. uminus_local_ring_at u \<in> \<ww>
[PROOF STEP]
qed (use \<open>u \<in> \<ww>\<close> uminus_closed in auto)
[PROOF STATE]
proof (state)
this:
monoid.invertible \<ww> add_local_ring_at zero_local_ring_at u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms \<ww> add_local_ring_at zero_local_ring_at

goal (1 subgoal):
 1. lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at
[PROOF STEP]
show "lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
assume a: "a \<in> carrier_local_ring_at"
[PROOF STATE]
proof (state)
this:
a \<in> carrier_local_ring_at

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> carrier_local_ring_at
[PROOF STEP]
obtain ra sa where a: "a = cq.frac ra sa" and "ra \<in> R" and sa: "sa \<in> R" "sa \<notin> I"
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier_local_ring_at

goal (1 subgoal):
 1. (\<And>ra sa. \<lbrakk>a = cq.frac ra sa; ra \<in> R; sa \<in> R; sa \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson frac_from_carrier_local)
[PROOF STATE]
proof (state)
this:
a = cq.frac ra sa
ra \<in> R
sa \<in> R
sa \<notin> I

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = cq.frac ra sa
ra \<in> R
sa \<in> R
sa \<notin> I
[PROOF STEP]
have "a \<in> carrier_local_ring_at"
[PROOF STATE]
proof (prove)
using this:
a = cq.frac ra sa
ra \<in> R
sa \<in> R
sa \<notin> I

goal (1 subgoal):
 1. a \<in> carrier_local_ring_at
[PROOF STEP]
by (simp add: comm.frac_in_carrier_local comm.spectrum_def pr_ideal_axioms)
[PROOF STATE]
proof (state)
this:
a \<in> carrier_local_ring_at

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
assume "b \<in> \<ww>"
[PROOF STATE]
proof (state)
this:
b \<in> \<ww>

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> \<ww>
[PROOF STEP]
obtain rb sb where b: "b = cq.frac rb sb" and "rb \<in> I" and sb: "sb \<in> R" "sb \<notin> I"
[PROOF STATE]
proof (prove)
using this:
b \<in> \<ww>

goal (1 subgoal):
 1. (\<And>rb sb. \<lbrakk>b = cq.frac rb sb; rb \<in> I; sb \<in> R; sb \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<ww>_def
[PROOF STATE]
proof (prove)
using this:
b \<in> \<ww>
\<ww> \<equiv> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}

goal (1 subgoal):
 1. (\<And>rb sb. \<lbrakk>b = cq.frac rb sb; rb \<in> I; sb \<in> R; sb \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = cq.frac rb sb
rb \<in> I
sb \<in> R
sb \<notin> I

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
have "cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb)
[PROOF STEP]
using \<open>ra \<in> R\<close> sa  \<open>rb \<in> I\<close> sb
[PROOF STATE]
proof (prove)
using this:
ra \<in> R
sa \<in> R
sa \<notin> I
rb \<in> I
sb \<in> R
sb \<notin> I

goal (1 subgoal):
 1. cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb)
[PROOF STEP]
by (force simp: cq.mult_rel_frac)
[PROOF STATE]
proof (state)
this:
cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb)

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> carrier_local_ring_at; a \<in> \<ww>\<rbrakk> \<Longrightarrow> mult_local_ring_at r a \<in> \<ww>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb)
[PROOF STEP]
show "mult_local_ring_at a b \<in> \<ww>"
[PROOF STATE]
proof (prove)
using this:
cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb)

goal (1 subgoal):
 1. mult_local_ring_at a b \<in> \<ww>
[PROOF STEP]
apply (clarsimp simp add: mult_local_ring_at_def \<ww>_def a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.mult_rel (cq.frac ra sa) (cq.frac rb sb) = cq.frac (ra \<cdot> rb) (sa \<cdot> sb) \<Longrightarrow> \<exists>r s. cq.frac (ra \<cdot> rb) (sa \<cdot> sb) = cq.frac r s \<and> r \<in> I \<and> s \<in> R \<and> s \<notin> I
[PROOF STEP]
by (metis Diff_iff \<open>ra \<in> R\<close> \<open>rb \<in> I\<close> cq.sub_composition_closed ideal(1) sa sb)
[PROOF STATE]
proof (state)
this:
mult_local_ring_at a b \<in> \<ww>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lideal_axioms \<ww> carrier_local_ring_at mult_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
have max: "max_lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<ww> \<noteq> carrier_local_ring_at
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; \<aa> \<noteq> carrier_local_ring_at; \<ww> \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> \<ww> = \<aa>
[PROOF STEP]
have False
      if "s \<in> R\<setminus>I" "r \<in> I" and eq: "cq.frac \<one> \<one> = cq.frac r s" for r s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using that eq_from_eq_frac [OF eq] \<open>r \<in> I\<close> comm.additive.abelian_group_axioms
[PROOF STATE]
proof (prove)
using this:
s \<in> R\<setminus>I
r \<in> I
cq.frac \<one> \<one> = cq.frac r s
\<lbrakk>\<one> \<in> R\<setminus>I; s \<in> R\<setminus>I; \<one> \<in> R; r \<in> R; \<And>h. \<lbrakk>h \<in> R\<setminus>I; h \<cdot> (s \<cdot> \<one> - \<one> \<cdot> r) = \<zero>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
r \<in> I
abelian_group R (+) \<zero>

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding abelian_group_def
[PROOF STATE]
proof (prove)
using this:
s \<in> R\<setminus>I
r \<in> I
cq.frac \<one> \<one> = cq.frac r s
\<lbrakk>\<one> \<in> R\<setminus>I; s \<in> R\<setminus>I; \<one> \<in> R; r \<in> R; \<And>h. \<lbrakk>h \<in> R\<setminus>I; h \<cdot> (s \<cdot> \<one> - \<one> \<cdot> r) = \<zero>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
r \<in> I
Group_Theory.group R (+) \<zero> \<and> commutative_monoid R (+) \<zero>

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis Diff_iff absorbent additive.sub comm.additive.cancel_imp_equal comm.inverse_distributive(1) comm.multiplicative.composition_closed cq.sub_unit_closed ideal(1))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s3 \<in> R\<setminus>I; ?r3 \<in> I; cq.frac \<one> \<one> = cq.frac ?r3 ?s3\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<ww> \<noteq> carrier_local_ring_at
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; \<aa> \<noteq> carrier_local_ring_at; \<ww> \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> \<ww> = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?s3 \<in> R\<setminus>I; ?r3 \<in> I; cq.frac \<one> \<one> = cq.frac ?r3 ?s3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "cq.frac \<one> \<one> \<notin> \<ww>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s3 \<in> R\<setminus>I; ?r3 \<in> I; cq.frac \<one> \<one> = cq.frac ?r3 ?s3\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. cq.frac \<one> \<one> \<notin> \<ww>
[PROOF STEP]
using \<ww>_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s3 \<in> R\<setminus>I; ?r3 \<in> I; cq.frac \<one> \<one> = cq.frac ?r3 ?s3\<rbrakk> \<Longrightarrow> False
\<ww> \<equiv> {cq.frac r s |r s. r \<in> I \<and> s \<in> R\<setminus>I}

goal (1 subgoal):
 1. cq.frac \<one> \<one> \<notin> \<ww>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cq.frac \<one> \<one> \<notin> \<ww>

goal (2 subgoals):
 1. \<ww> \<noteq> carrier_local_ring_at
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; \<aa> \<noteq> carrier_local_ring_at; \<ww> \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> \<ww> = \<aa>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cq.frac \<one> \<one> \<notin> \<ww>

goal (2 subgoals):
 1. \<ww> \<noteq> carrier_local_ring_at
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; \<aa> \<noteq> carrier_local_ring_at; \<ww> \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> \<ww> = \<aa>
[PROOF STEP]
have "cq.frac \<one> \<one> \<in> carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.frac \<one> \<one> \<in> carrier_local_ring_at
[PROOF STEP]
using carrier_local_ring_at_def cq.multiplicative.unit_closed cq.one_rel_def
[PROOF STATE]
proof (prove)
using this:
carrier_local_ring_at \<equiv> cq.carrier_quotient_ring
cq.one_rel \<in> cq.carrier_quotient_ring
cq.one_rel = cq.frac \<one> \<one>

goal (1 subgoal):
 1. cq.frac \<one> \<one> \<in> carrier_local_ring_at
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
cq.frac \<one> \<one> \<in> carrier_local_ring_at

goal (2 subgoals):
 1. \<ww> \<noteq> carrier_local_ring_at
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; \<aa> \<noteq> carrier_local_ring_at; \<ww> \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> \<ww> = \<aa>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cq.frac \<one> \<one> \<notin> \<ww>
cq.frac \<one> \<one> \<in> carrier_local_ring_at
[PROOF STEP]
show "\<ww> \<noteq> carrier_local_ring_at"
[PROOF STATE]
proof (prove)
using this:
cq.frac \<one> \<one> \<notin> \<ww>
cq.frac \<one> \<one> \<in> carrier_local_ring_at

goal (1 subgoal):
 1. \<ww> \<noteq> carrier_local_ring_at
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<ww> \<noteq> carrier_local_ring_at

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at; \<aa> \<noteq> carrier_local_ring_at; \<ww> \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> \<ww> = \<aa>
[PROOF STEP]
qed (use maximal in blast)
[PROOF STATE]
proof (state)
this:
max_lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
have "\<And>J. max_lideal J carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
\<Longrightarrow> J = \<ww>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>J. max_lideal J carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at \<Longrightarrow> J = \<ww>
[PROOF STEP]
by (metis maximal max max_lideal.axioms(1) max_lideal.is_max max_lideal.neq_ring)
[PROOF STATE]
proof (state)
this:
max_lideal ?J3 carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at \<Longrightarrow> ?J3 = \<ww>

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
with max
[PROOF STATE]
proof (chain)
picking this:
max_lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
max_lideal ?J3 carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at \<Longrightarrow> ?J3 = \<ww>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
max_lideal \<ww> carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
max_lideal ?J3 carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at \<Longrightarrow> ?J3 = \<ww>

goal (1 subgoal):
 1. local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at
[PROOF STEP]
by (metis local.ring_axioms local_ring_axioms_def local_ring_def)
[PROOF STATE]
proof (state)
this:
local_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at zero_local_ring_at one_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma id_is_local_ring_morphism:
  assumes "local_ring A add mult zero one"
  shows "local_ring_morphism (identity A) A add mult zero one A add mult zero one"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
interpret local_ring A add mult zero one
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring A add mult zero one
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Set_Theory.map (identity A) A A
 2. monoid_homomorphism_axioms (identity A) A add zero add zero
 3. monoid_homomorphism_axioms (identity A) A mult one mult one
 4. local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
show "Set_Theory.map (identity A) A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (identity A) A A
[PROOF STEP]
by (simp add: Set_Theory.map_def)
[PROOF STATE]
proof (state)
this:
Set_Theory.map (identity A) A A

goal (3 subgoals):
 1. monoid_homomorphism_axioms (identity A) A add zero add zero
 2. monoid_homomorphism_axioms (identity A) A mult one mult one
 3. local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
show "monoid_homomorphism_axioms (identity A) A add zero add zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism_axioms (identity A) A add zero add zero
[PROOF STEP]
by (simp add: monoid_homomorphism_axioms_def)
[PROOF STATE]
proof (state)
this:
monoid_homomorphism_axioms (identity A) A add zero add zero

goal (2 subgoals):
 1. monoid_homomorphism_axioms (identity A) A mult one mult one
 2. local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
show "monoid_homomorphism_axioms (identity A) A mult one mult one"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism_axioms (identity A) A mult one mult one
[PROOF STEP]
by (simp add: monoid_homomorphism_axioms_def)
[PROOF STATE]
proof (state)
this:
monoid_homomorphism_axioms (identity A) A mult one mult one

goal (1 subgoal):
 1. local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
show "local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A add mult zero one; max_lideal \<ww>\<^sub>B A add mult zero one\<rbrakk> \<Longrightarrow> identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
fix \<ww>\<^sub>A \<ww>\<^sub>B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A add mult zero one; max_lideal \<ww>\<^sub>B A add mult zero one\<rbrakk> \<Longrightarrow> identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
assume "max_lideal \<ww>\<^sub>A A add mult zero one" "max_lideal \<ww>\<^sub>B A add mult zero one"
[PROOF STATE]
proof (state)
this:
max_lideal \<ww>\<^sub>A A add mult zero one
max_lideal \<ww>\<^sub>B A add mult zero one

goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A add mult zero one; max_lideal \<ww>\<^sub>B A add mult zero one\<rbrakk> \<Longrightarrow> identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_lideal \<ww>\<^sub>A A add mult zero one
max_lideal \<ww>\<^sub>B A add mult zero one
[PROOF STEP]
have "\<ww>\<^sub>B \<inter> A = \<ww>\<^sub>A"
[PROOF STATE]
proof (prove)
using this:
max_lideal \<ww>\<^sub>A A add mult zero one
max_lideal \<ww>\<^sub>B A add mult zero one

goal (1 subgoal):
 1. \<ww>\<^sub>B \<inter> A = \<ww>\<^sub>A
[PROOF STEP]
by (metis Int_absorb2 is_unique lideal.subset max_lideal.axioms(1))
[PROOF STATE]
proof (state)
this:
\<ww>\<^sub>B \<inter> A = \<ww>\<^sub>A

goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A add mult zero one; max_lideal \<ww>\<^sub>B A add mult zero one\<rbrakk> \<Longrightarrow> identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ww>\<^sub>B \<inter> A = \<ww>\<^sub>A
[PROOF STEP]
show "identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A"
[PROOF STATE]
proof (prove)
using this:
\<ww>\<^sub>B \<inter> A = \<ww>\<^sub>A

goal (1 subgoal):
 1. identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
by (simp add: preimage_identity_self)
[PROOF STATE]
proof (state)
this:
identity A \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local_ring_morphism_axioms (identity A) A add mult zero one A add mult zero one

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local_ring_morphism (identity A) A add mult zero one A add mult zero one

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ring_epimorphism) preim_subset_imp_subset:
  assumes "\<eta> \<^sup>\<inverse> R I \<subseteq> \<eta> \<^sup>\<inverse> R J" and "I \<subseteq> R'"
  shows "I \<subseteq> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> J
[PROOF STEP]
using Int_absorb1 assms surjective
[PROOF STATE]
proof (prove)
using this:
?B \<subseteq> ?A \<Longrightarrow> ?A \<inter> ?B = ?B
\<eta> \<^sup>\<inverse> R I \<subseteq> \<eta> \<^sup>\<inverse> R J
I \<subseteq> R'
\<eta> ` R = R'

goal (1 subgoal):
 1. I \<subseteq> J
[PROOF STEP]
by blast


[STATEMENT]
lemma iso_is_local_ring_morphism:
  assumes "local_ring A addA multA zeroA oneA"
    and "ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
interpret A: local_ring A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring A addA multA zeroA oneA
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
local_ring A addA multA zeroA oneA

goal (1 subgoal):
 1. local_ring A addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
interpret B: ring B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring B addB multB zeroB oneB
[PROOF STEP]
by (meson assms(2) ring_homomorphism_def ring_isomorphism_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
interpret f: ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
interpret preB: ring "f \<^sup>\<inverse> A B" addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by (metis (no_types) A.ring_axioms f.multiplicative.image.subset image_subset_iff_subset_vimage inf.absorb2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
fix I J
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
assume "max_lideal I B addB multB zeroB oneB"
[PROOF STATE]
proof (state)
this:
max_lideal I B addB multB zeroB oneB

goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_lideal I B addB multB zeroB oneB
[PROOF STEP]
interpret MI: max_lideal I B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
using this:
max_lideal I B addB multB zeroB oneB

goal (1 subgoal):
 1. max_lideal I B addB multB zeroB oneB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
assume "max_lideal J B addB multB zeroB oneB"
[PROOF STATE]
proof (state)
this:
max_lideal J B addB multB zeroB oneB

goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_lideal J B addB multB zeroB oneB
[PROOF STEP]
interpret MJ: max_lideal J B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
using this:
max_lideal J B addB multB zeroB oneB

goal (1 subgoal):
 1. max_lideal J B addB multB zeroB oneB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
interpret GI: subgroup I B addB zeroB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup I B addB zeroB
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
have "max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by (metis (no_types) MI.max_lideal_axioms f.ring_isomorphism_axioms preim_of_max_lideal_is_max)
[PROOF STATE]
proof (state)
this:
max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA

goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA

goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
have "max_lideal (f \<^sup>\<inverse> A J) (f \<^sup>\<inverse> A B) addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal (f \<^sup>\<inverse> A J) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by (meson MJ.max_lideal_axioms f.ring_isomorphism_axioms preim_of_max_lideal_is_max)
[PROOF STATE]
proof (state)
this:
max_lideal (f \<^sup>\<inverse> A J) (f \<^sup>\<inverse> A B) addA multA zeroA oneA

goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
max_lideal (f \<^sup>\<inverse> A J) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
have "f \<^sup>\<inverse> A I = f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
using this:
max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
max_lideal (f \<^sup>\<inverse> A J) (f \<^sup>\<inverse> A B) addA multA zeroA oneA

goal (1 subgoal):
 1. f \<^sup>\<inverse> A I = f \<^sup>\<inverse> A J
[PROOF STEP]
by (metis A.is_unique Int_absorb1 f.multiplicative.image.subset image_subset_iff_subset_vimage)
[PROOF STATE]
proof (state)
this:
f \<^sup>\<inverse> A I = f \<^sup>\<inverse> A J

goal (3 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I B addB multB zeroB oneB; max_lideal J B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 3. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<^sup>\<inverse> A I = f \<^sup>\<inverse> A J
[PROOF STEP]
show "I = J"
[PROOF STATE]
proof (prove)
using this:
f \<^sup>\<inverse> A I = f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. I = J
[PROOF STEP]
by (metis MI.lideal_axioms MI.neq_ring MJ.max_lideal_axioms MJ.subset f.preim_subset_imp_subset max_lideal.is_max subset_refl)
[PROOF STATE]
proof (state)
this:
I = J

goal (2 subgoals):
 1. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 2. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
 2. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
show "\<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB
[PROOF STEP]
by (meson A.has_max_lideal assms(2) im_of_max_lideal_is_max)
[PROOF STATE]
proof (state)
this:
\<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB

goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
fix \<ww>\<^sub>A \<ww>\<^sub>B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
assume "max_lideal \<ww>\<^sub>A A addA multA zeroA oneA"
        and "max_lideal \<ww>\<^sub>B B addB multB zeroB oneB"
[PROOF STATE]
proof (state)
this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>B B addB multB zeroB oneB

goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B B addB multB zeroB oneB\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>B B addB multB zeroB oneB
[PROOF STEP]
show "f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A"
[PROOF STATE]
proof (prove)
using this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>B B addB multB zeroB oneB

goal (1 subgoal):
 1. f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
by (metis A.is_unique f.multiplicative.image.subset f.ring_isomorphism_axioms image_subset_iff_subset_vimage inf.absorb2 preim_of_max_lideal_is_max)
[PROOF STATE]
proof (state)
this:
f \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in monoid_homomorphism) monoid_epimorphism_image:
   "monoid_epimorphism \<eta> M (\<cdot>) \<one> (\<eta> ` M) (\<cdot>') \<one>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_epimorphism \<eta> M (\<cdot>) \<one> (\<eta> ` M) (\<cdot>') \<one>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. monoid_epimorphism \<eta> M (\<cdot>) \<one> (\<eta> ` M) (\<cdot>') \<one>'
[PROOF STEP]
interpret monoid "\<eta> ` M" "(\<cdot>')" "\<one>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<eta> ` M) (\<cdot>') \<one>'
[PROOF STEP]
using image.sub.monoid_axioms
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid (\<eta> ` M) (\<cdot>') \<one>'

goal (1 subgoal):
 1. Group_Theory.monoid (\<eta> ` M) (\<cdot>') \<one>'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. monoid_epimorphism \<eta> M (\<cdot>) \<one> (\<eta> ` M) (\<cdot>') \<one>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_epimorphism \<eta> M (\<cdot>) \<one> (\<eta> ` M) (\<cdot>') \<one>'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<eta> \<in> M \<rightarrow>\<^sub>E \<eta> ` M
 2. \<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> \<eta> (x \<cdot> y) = \<eta> x \<cdot>' \<eta> y
 3. \<eta> \<one> = \<one>'
 4. \<eta> ` M = \<eta> ` M
[PROOF STEP]
qed (auto simp: bij_betw_def commutes_with_unit commutes_with_composition)
[PROOF STATE]
proof (state)
this:
monoid_epimorphism \<eta> M (\<cdot>) \<one> (\<eta> ` M) (\<cdot>') \<one>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group_homomorphism) group_epimorphism_image:
   "group_epimorphism \<eta> G (\<cdot>) \<one> (\<eta> ` G) (\<cdot>') \<one>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_epimorphism \<eta> G (\<cdot>) \<one> (\<eta> ` G) (\<cdot>') \<one>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. group_epimorphism \<eta> G (\<cdot>) \<one> (\<eta> ` G) (\<cdot>') \<one>'
[PROOF STEP]
interpret group "\<eta> ` G" "(\<cdot>')" "\<one>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group (\<eta> ` G) (\<cdot>') \<one>'
[PROOF STEP]
using image.sub.group_axioms
[PROOF STATE]
proof (prove)
using this:
Group_Theory.group (\<eta> ` G) (\<cdot>') \<one>'

goal (1 subgoal):
 1. Group_Theory.group (\<eta> ` G) (\<cdot>') \<one>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. group_epimorphism \<eta> G (\<cdot>) \<one> (\<eta> ` G) (\<cdot>') \<one>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_epimorphism \<eta> G (\<cdot>) \<one> (\<eta> ` G) (\<cdot>') \<one>'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<eta> \<in> G \<rightarrow>\<^sub>E \<eta> ` G
 2. \<And>x y. \<lbrakk>x \<in> G; y \<in> G\<rbrakk> \<Longrightarrow> \<eta> (x \<cdot> y) = \<eta> x \<cdot>' \<eta> y
 3. \<eta> \<one> = \<one>'
 4. \<eta> ` G = \<eta> ` G
[PROOF STEP]
qed (auto simp: bij_betw_def commutes_with_composition)
[PROOF STATE]
proof (state)
this:
group_epimorphism \<eta> G (\<cdot>) \<one> (\<eta> ` G) (\<cdot>') \<one>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ring_homomorphism) ring_epimorphism_preimage:
   "ring_epimorphism \<eta> R (+) (\<cdot>) \<zero> \<one> (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_epimorphism \<eta> R (+) (\<cdot>) \<zero> \<one> (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ring_epimorphism \<eta> R (+) (\<cdot>) \<zero> \<one> (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'
[PROOF STEP]
interpret ring "\<eta> ` R" "(+')" "(\<cdot>')" "\<zero>'" "\<one>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<eta> ` R; y \<in> \<eta> ` R\<rbrakk> \<Longrightarrow> x +' y = y +' x
 2. \<And>a b c. \<lbrakk>a \<in> \<eta> ` R; b \<in> \<eta> ` R; c \<in> \<eta> ` R\<rbrakk> \<Longrightarrow> a \<cdot>' (b +' c) = a \<cdot>' b +' a \<cdot>' c
 3. \<And>a b c. \<lbrakk>a \<in> \<eta> ` R; b \<in> \<eta> ` R; c \<in> \<eta> ` R\<rbrakk> \<Longrightarrow> (b +' c) \<cdot>' a = b \<cdot>' a +' c \<cdot>' a
[PROOF STEP]
qed (auto simp add: target.distributive target.additive.commutative)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ring_epimorphism \<eta> R (+) (\<cdot>) \<zero> \<one> (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_epimorphism \<eta> R (+) (\<cdot>) \<zero> \<one> (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<eta> \<in> R \<rightarrow>\<^sub>E \<eta> ` R
 2. \<And>x y. \<lbrakk>x \<in> R; y \<in> R\<rbrakk> \<Longrightarrow> \<eta> (x + y) = \<eta> x +' \<eta> y
 3. \<eta> \<zero> = \<zero>'
 4. \<And>x y. \<lbrakk>x \<in> R; y \<in> R\<rbrakk> \<Longrightarrow> \<eta> (x \<cdot> y) = \<eta> x \<cdot>' \<eta> y
 5. \<eta> \<one> = \<one>'
 6. \<eta> ` R = \<eta> ` R
[PROOF STEP]
qed (auto simp: additive.commutes_with_composition additive.commutes_with_unit
      multiplicative.commutes_with_composition multiplicative.commutes_with_unit)
[PROOF STATE]
proof (state)
this:
ring_epimorphism \<eta> R (+) (\<cdot>) \<zero> \<one> (\<eta> ` R) (+') (\<cdot>') \<zero>' \<one>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_of_local_ring_morphisms:
  assumes "local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB"
      and "local_ring_morphism g B addB multB zeroB oneB C addC multC zeroC oneC"
    shows "local_ring_morphism (compose A g f) A addA multA zeroA oneA C addC multC zeroC oneC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
interpret f: local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
interpret g: local_ring_morphism g B addB multB zeroB oneB C addC multC zeroC oneC
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism g B addB multB zeroB oneB C addC multC zeroC oneC
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
interpret gf: ring_homomorphism "compose A g f" A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
using comp_ring_morphisms f.ring_homomorphism_axioms g.ring_homomorphism_axioms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>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\<rbrakk> \<Longrightarrow> ring_homomorphism (?\<theta> \<circ> ?\<eta> \<down> ?A) ?A ?addA ?multA ?zeroA ?oneA ?C ?addC ?multC ?zeroC ?oneC
ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
ring_homomorphism g B addB multB zeroB oneB C addC multC zeroC oneC

goal (1 subgoal):
 1. ring_homomorphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
obtain \<ww>\<^sub>B where \<ww>\<^sub>B: "max_lideal \<ww>\<^sub>B B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<ww>\<^sub>B. max_lideal \<ww>\<^sub>B B addB multB zeroB oneB \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f.target.has_max_lideal
[PROOF STATE]
proof (prove)
using this:
\<exists>\<ww>. max_lideal \<ww> B addB multB zeroB oneB

goal (1 subgoal):
 1. (\<And>\<ww>\<^sub>B. max_lideal \<ww>\<^sub>B B addB multB zeroB oneB \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
max_lideal \<ww>\<^sub>B B addB multB zeroB oneB

goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local_ring_morphism_axioms (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
show "local_ring_morphism_axioms (compose A g f) A addA multA zeroA oneA C addC multC zeroC oneC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_morphism_axioms (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
fix \<ww>\<^sub>A \<ww>\<^sub>C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
assume max: "max_lideal \<ww>\<^sub>A A addA multA zeroA oneA"
                  "max_lideal \<ww>\<^sub>C C addC multC zeroC oneC"
[PROOF STATE]
proof (state)
this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>C C addC multC zeroC oneC

goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
interpret maxA: max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
[PROOF STEP]
using max
[PROOF STATE]
proof (prove)
using this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>C C addC multC zeroC oneC

goal (1 subgoal):
 1. max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
interpret maxC: max_lideal \<ww>\<^sub>C C addC multC zeroC oneC
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal \<ww>\<^sub>C C addC multC zeroC oneC
[PROOF STEP]
using max
[PROOF STATE]
proof (prove)
using this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>C C addC multC zeroC oneC

goal (1 subgoal):
 1. max_lideal \<ww>\<^sub>C C addC multC zeroC oneC
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
have "B \<subseteq> g -` C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> g -` C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<subseteq> g -` C

goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
with max
[PROOF STATE]
proof (chain)
picking this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>C C addC multC zeroC oneC
B \<subseteq> g -` C
[PROOF STEP]
interpret maxg: max_lideal "g \<^sup>\<inverse> B \<ww>\<^sub>C" "g \<^sup>\<inverse> B C" addB multB zeroB oneB
[PROOF STATE]
proof (prove)
using this:
max_lideal \<ww>\<^sub>A A addA multA zeroA oneA
max_lideal \<ww>\<^sub>C C addC multC zeroC oneC
B \<subseteq> g -` C

goal (1 subgoal):
 1. max_lideal (g \<^sup>\<inverse> B \<ww>\<^sub>C) (g \<^sup>\<inverse> B C) addB multB zeroB oneB
[PROOF STEP]
by (metis Int_absorb1 \<ww>\<^sub>B g.preimage_of_max_lideal)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
interpret maxgf: Group_Theory.monoid "(g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C" addA zeroA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid ((g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C) addA zeroA
[PROOF STEP]
by (simp add: monoid_def vimage_def gf.additive.commutes_with_composition
                      gf.additive.commutes_with_unit f.source.additive.associative)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<ww>\<^sub>A \<ww>\<^sub>B. \<lbrakk>max_lideal \<ww>\<^sub>A A addA multA zeroA oneA; max_lideal \<ww>\<^sub>B C addC multC zeroC oneC\<rbrakk> \<Longrightarrow> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>B = \<ww>\<^sub>A
[PROOF STEP]
show "(g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C = \<ww>\<^sub>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C = \<ww>\<^sub>A
[PROOF STEP]
proof (rule maxA.is_max [symmetric])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lideal ((g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C) A addA multA zeroA oneA
 2. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
 3. \<ww>\<^sub>A \<subseteq> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
show "lideal ((g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C) A addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal ((g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C) A addA multA zeroA oneA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>u. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<Longrightarrow> maxgf.invertible u
 5. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>u. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<Longrightarrow> maxgf.invertible u
 5. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
assume u: "u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C"
[PROOF STATE]
proof (state)
this:
u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (5 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>u. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<Longrightarrow> maxgf.invertible u
 5. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
have "u \<in> A"
[PROOF STATE]
proof (prove)
using this:
u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (1 subgoal):
 1. u \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> A

goal (5 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>u. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<Longrightarrow> maxgf.invertible u
 5. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
show "maxgf.invertible u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxgf.invertible u
[PROOF STEP]
proof (rule maxgf.invertibleI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. addA u ?v = zeroA
 2. addA ?v u = zeroA
 3. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. ?v \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
show "addA u (f.source.additive.inverse u) = zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f.source.subtraction u u = zeroA
[PROOF STEP]
using f.source.additive.invertible_right_inverse \<open>u \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f.source.additive.invertible ?u; ?u \<in> A\<rbrakk> \<Longrightarrow> f.source.subtraction ?u ?u = zeroA
u \<in> A

goal (1 subgoal):
 1. f.source.subtraction u u = zeroA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f.source.subtraction u u = zeroA

goal (3 subgoals):
 1. addA (f.source.additive.inverse u) u = zeroA
 2. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. f.source.additive.inverse u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
have "(g \<circ> f \<down> A) (f.source.additive.inverse u) = g.target.additive.inverse (g (f u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ> f \<down> A) (f.source.additive.inverse u) = g.target.additive.inverse (g (f u))
[PROOF STEP]
by (metis f.source.additive.invertible \<open>u \<in> A\<close> compose_eq
                    gf.additive.invertible_commutes_with_inverse)
[PROOF STATE]
proof (state)
this:
(g \<circ> f \<down> A) (f.source.additive.inverse u) = g.target.additive.inverse (g (f u))

goal (3 subgoals):
 1. addA (f.source.additive.inverse u) u = zeroA
 2. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. f.source.additive.inverse u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g \<circ> f \<down> A) (f.source.additive.inverse u) = g.target.additive.inverse (g (f u))
[PROOF STEP]
show "(f.source.additive.inverse u) \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C"
[PROOF STATE]
proof (prove)
using this:
(g \<circ> f \<down> A) (f.source.additive.inverse u) = g.target.additive.inverse (g (f u))

goal (1 subgoal):
 1. f.source.additive.inverse u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
by (metis f.source.additive.invertible f.source.additive.invertible_inverse_closed
                    g.target.additive.group_axioms Int_iff compose_eq
                    maxC.additive.subgroup_inverse_iff f.map_closed g.map_axioms group.invertible
                    map.map_closed u vimage_eq)
[PROOF STATE]
proof (state)
this:
f.source.additive.inverse u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (2 subgoals):
 1. addA (f.source.additive.inverse u) u = zeroA
 2. u \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
qed (use u \<open>u \<in> A\<close> in auto)
[PROOF STATE]
proof (state)
this:
maxgf.invertible u

goal (4 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
fix r a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
assume "r \<in> A" and "a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C"
[PROOF STATE]
proof (state)
this:
r \<in> A
a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (4 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 4. \<And>r a. \<lbrakk>r \<in> A; a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> A
a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
show "multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C"
[PROOF STATE]
proof (prove)
using this:
r \<in> A
a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (1 subgoal):
 1. multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
by (simp add: maxC.lideal gf.multiplicative.commutes_with_composition)
[PROOF STATE]
proof (state)
this:
multA r a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (3 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C; b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C\<rbrakk> \<Longrightarrow> addA a b \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
 3. zeroA \<in> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
qed (use maxgf.unit_closed maxgf.composition_closed in auto)
[PROOF STATE]
proof (state)
this:
lideal ((g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C) A addA multA zeroA oneA

goal (2 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
 2. \<ww>\<^sub>A \<subseteq> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
have "\<And>x. x \<in> \<ww>\<^sub>A \<Longrightarrow> g (f x) \<in> \<ww>\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> \<ww>\<^sub>A \<Longrightarrow> g (f x) \<in> \<ww>\<^sub>C
[PROOF STEP]
by (metis IntD1 \<ww>\<^sub>B f.preimage_of_max_lideal g.preimage_of_max_lideal max vimageD)
[PROOF STATE]
proof (state)
this:
?x1 \<in> \<ww>\<^sub>A \<Longrightarrow> g (f ?x1) \<in> \<ww>\<^sub>C

goal (2 subgoals):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
 2. \<ww>\<^sub>A \<subseteq> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x1 \<in> \<ww>\<^sub>A \<Longrightarrow> g (f ?x1) \<in> \<ww>\<^sub>C
[PROOF STEP]
show "\<ww>\<^sub>A \<subseteq> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C"
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> \<ww>\<^sub>A \<Longrightarrow> g (f ?x1) \<in> \<ww>\<^sub>C

goal (1 subgoal):
 1. \<ww>\<^sub>A \<subseteq> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C
[PROOF STEP]
by (auto simp: compose_eq)
[PROOF STATE]
proof (state)
this:
\<ww>\<^sub>A \<subseteq> (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C

goal (1 subgoal):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
[PROOF STEP]
have "oneB \<notin> g -` \<ww>\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oneB \<notin> g -` \<ww>\<^sub>C
[PROOF STEP]
using maxg.has_one_imp_equal maxg.neq_ring
[PROOF STATE]
proof (prove)
using this:
oneB \<in> g \<^sup>\<inverse> B \<ww>\<^sub>C \<Longrightarrow> g \<^sup>\<inverse> B \<ww>\<^sub>C = g \<^sup>\<inverse> B C
g \<^sup>\<inverse> B \<ww>\<^sub>C \<noteq> g \<^sup>\<inverse> B C

goal (1 subgoal):
 1. oneB \<notin> g -` \<ww>\<^sub>C
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
oneB \<notin> g -` \<ww>\<^sub>C

goal (1 subgoal):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
oneB \<notin> g -` \<ww>\<^sub>C
[PROOF STEP]
have "g oneB \<notin> \<ww>\<^sub>C"
[PROOF STATE]
proof (prove)
using this:
oneB \<notin> g -` \<ww>\<^sub>C

goal (1 subgoal):
 1. g oneB \<notin> \<ww>\<^sub>C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g oneB \<notin> \<ww>\<^sub>C

goal (1 subgoal):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g oneB \<notin> \<ww>\<^sub>C
[PROOF STEP]
show "(g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A"
[PROOF STATE]
proof (prove)
using this:
g oneB \<notin> \<ww>\<^sub>C

goal (1 subgoal):
 1. (g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A
[PROOF STEP]
by (metis Int_iff compose_eq f.multiplicative.commutes_with_unit f.source.multiplicative.unit_closed vimage_eq)
[PROOF STATE]
proof (state)
this:
(g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C \<noteq> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(g \<circ> f \<down> A) \<^sup>\<inverse> A \<ww>\<^sub>C = \<ww>\<^sub>A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local_ring_morphism_axioms (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local_ring_morphism (g \<circ> f \<down> A) A addA multA zeroA oneA C addC multC zeroC oneC

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma key_map_is_map:
  assumes  "\<pp> \<in> U"
  shows "Set_Theory.map (key_map U) (\<O> U) (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.key_map U \<in> \<O> U \<rightarrow>\<^sub>E pi.carrier_local_ring_at
[PROOF STEP]
have "\<And>s. s \<in> \<O> U \<Longrightarrow> s \<pp> \<in> (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using sheaf_spec_def assms is_regular_def
[PROOF STATE]
proof (prove)
using this:
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}
\<pp> \<in> U
is_regular ?s ?U \<equiv> \<forall>\<pp>. \<pp> \<in> ?U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> ?U \<and> \<pp> \<in> V \<and> is_locally_frac ?s V)

goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?s3 \<in> \<O> U \<Longrightarrow> ?s3 \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. local.key_map U \<in> \<O> U \<rightarrow>\<^sub>E pi.carrier_local_ring_at
[PROOF STEP]
thus "key_map U \<in> (\<O> U) \<rightarrow>\<^sub>E (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
?s3 \<in> \<O> U \<Longrightarrow> ?s3 \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. local.key_map U \<in> \<O> U \<rightarrow>\<^sub>E pi.carrier_local_ring_at
[PROOF STEP]
using key_map_def extensional_funcset_def
[PROOF STATE]
proof (prove)
using this:
?s3 \<in> \<O> U \<Longrightarrow> ?s3 \<pp> \<in> pi.carrier_local_ring_at
local.key_map ?U \<equiv> \<lambda>s\<in>\<O> ?U. s \<pp>
?S \<rightarrow>\<^sub>E ?T = (?S \<rightarrow> ?T) \<inter> extensional ?S

goal (1 subgoal):
 1. local.key_map U \<in> \<O> U \<rightarrow>\<^sub>E pi.carrier_local_ring_at
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.key_map U \<in> \<O> U \<rightarrow>\<^sub>E pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed