[STATEMENT]
lemma rel_I1:
  assumes "s \<in> \<FF> U" "x \<in> \<lfloor>U, s\<rfloor>" "U \<in> I"
  shows "(U, s) \<sim> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U, s) \<sim> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (U, s) \<sim> x
[PROOF STEP]
have Us: "\<lfloor>U, s\<rfloor> \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U, s\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> \<FF> U
x \<in> \<lfloor>U, s\<rfloor>
U \<in> I

goal (1 subgoal):
 1. \<lfloor>U, s\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
unfolding carrier_direct_lim_def class_of_def
[PROOF STATE]
proof (prove)
using this:
s \<in> \<FF> U
x \<in> rel.Class (U, s)
U \<in> I

goal (1 subgoal):
 1. rel.Class (U, s) \<in> rel.Partition
[PROOF STEP]
by (simp add: equivalence.Class_in_Partition rel_is_equivalence)
[PROOF STATE]
proof (state)
this:
\<lfloor>U, s\<rfloor> \<in> carrier_direct_lim

goal (1 subgoal):
 1. (U, s) \<sim> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>U, s\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>U, s\<rfloor> \<in> carrier_direct_lim

goal (1 subgoal):
 1. (U, s) \<sim> x
[PROOF STEP]
using rel_Class_iff assms
[PROOF STATE]
proof (prove)
using this:
\<lfloor>U, s\<rfloor> \<in> carrier_direct_lim
?x \<sim> ?y = (?y \<in> Sigma I \<FF> \<and> ?x \<in> rel.Class ?y)
s \<in> \<FF> U
x \<in> \<lfloor>U, s\<rfloor>
U \<in> I

goal (1 subgoal):
 1. (U, s) \<sim> x
[PROOF STEP]
by (metis carrier_direct_lim_def class_of_def mem_Sigma_iff rel.Block_self rel.Class_self rel.block_closed)
[PROOF STATE]
proof (state)
this:
(U, s) \<sim> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_I2:
  assumes "s \<in> \<FF> U" "x \<in> \<lfloor>U, s\<rfloor>" "U \<in> I"
  shows "(U, s) \<sim> (SOME x. x \<in> \<lfloor>U, s\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U, s) \<sim> (SOME x. x \<in> \<lfloor>U, s\<rfloor>)
[PROOF STEP]
using carrier_direct_lim_def class_of_def rel_carrier_Eps_in(2) rel_carrier_Eps_in(3) assms
[PROOF STATE]
proof (prove)
using this:
carrier_direct_lim \<equiv> rel.Partition
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
?X \<in> carrier_direct_lim \<Longrightarrow> (SOME x. x \<in> ?X) \<in> Sigma I \<FF>
?X \<in> carrier_direct_lim \<Longrightarrow> ?X = \<lfloor>fst (SOME x. x \<in> ?X), snd (SOME x. x \<in> ?X)\<rfloor>
s \<in> \<FF> U
x \<in> \<lfloor>U, s\<rfloor>
U \<in> I

goal (1 subgoal):
 1. (U, s) \<sim> (SOME x. x \<in> \<lfloor>U, s\<rfloor>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma carrier_direct_limE:
  assumes "X \<in> carrier_direct_lim"
  obtains U s where "U \<in> I" "s \<in> \<FF> U" "X = \<lfloor>U,s\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U s. \<lbrakk>U \<in> I; s \<in> \<FF> U; X = \<lfloor>U, s\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms carrier_direct_lim_def class_of_def
[PROOF STATE]
proof (prove)
using this:
X \<in> carrier_direct_lim
carrier_direct_lim \<equiv> rel.Partition
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)

goal (1 subgoal):
 1. (\<And>U s. \<lbrakk>U \<in> I; s \<in> \<FF> U; X = \<lfloor>U, s\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma neighborhoods_eq:"neighborhoods x = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neighborhoods x = I
[PROOF STEP]
unfolding index neighborhoods_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {U. is_open U \<and> x \<in> U} = {U. is_open U \<and> x \<in> U}
[PROOF STEP]
by simp


[STATEMENT]
lemma class_of_in_stalk:
  assumes "A \<in> (neighborhoods x)" and "z \<in> \<FF> A"
  shows "class_of A z \<in> carrier_stalk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>A, z\<rfloor> \<in> carrier_stalk
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>A, z\<rfloor> \<in> carrier_stalk
[PROOF STEP]
interpret equivalence "Sigma I \<FF>" "{(x, y). x \<sim> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence (Sigma I \<FF>) {(x, y). x \<sim> y}
[PROOF STEP]
using rel_is_equivalence
[PROOF STATE]
proof (prove)
using this:
equivalence (Sigma I \<FF>) {(x, y). x \<sim> y}

goal (1 subgoal):
 1. equivalence (Sigma I \<FF>) {(x, y). x \<sim> y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>A, z\<rfloor> \<in> carrier_stalk
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>A, z\<rfloor> \<in> carrier_stalk
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> neighborhoods x
z \<in> \<FF> A

goal (1 subgoal):
 1. \<lfloor>A, z\<rfloor> \<in> carrier_stalk
[PROOF STEP]
unfolding carrier_stalk_def neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
A \<in> {U. is_open U \<and> x \<in> U}
z \<in> \<FF> A

goal (1 subgoal):
 1. \<lfloor>A, z\<rfloor> \<in> dlim \<FF> \<rho> {U. is_open U \<and> x \<in> U}
[PROOF STEP]
by (metis (no_types, lifting) carrier_direct_lim_def class_of_def index mem_Sigma_iff natural.map_closed)
[PROOF STATE]
proof (state)
this:
\<lfloor>A, z\<rfloor> \<in> carrier_stalk

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stalk_is_ring:
  assumes "is_open V" and "x \<in> V"
  shows "ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)
[PROOF STEP]
interpret r: ring carrier_direct_lim add_rel mult_rel "\<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor>" "\<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor>
[PROOF STEP]
using assms direct_lim_is_ring index
[PROOF STATE]
proof (prove)
using this:
is_open V
x \<in> V
?U \<in> I \<Longrightarrow> ring carrier_direct_lim add_rel mult_rel \<lfloor>?U, \<zero>\<^bsub>?U\<^esub>\<rfloor> \<lfloor>?U, \<one>\<^bsub>?U\<^esub>\<rfloor>
I = {U. is_open U \<and> x \<in> U}

goal (1 subgoal):
 1. ring carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)
[PROOF STEP]
using r.additive.monoid_axioms
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid carrier_direct_lim add_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor>

goal (1 subgoal):
 1. ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)
[PROOF STEP]
unfolding zero_stalk_def one_stalk_def add_stalk_def mult_stalk_def carrier_stalk_def
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid carrier_direct_lim add_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor>

goal (1 subgoal):
 1. ring (dlim \<FF> \<rho> (neighborhoods x)) add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor>
[PROOF STEP]
using index neighborhoods_def r.ring_axioms
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid carrier_direct_lim add_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor>
I = {U. is_open U \<and> x \<in> U}
neighborhoods ?x \<equiv> {U. is_open U \<and> ?x \<in> U}
ring carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor>

goal (1 subgoal):
 1. ring (dlim \<FF> \<rho> (neighborhoods x)) add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ring carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_zero_stalk [simp]:
  assumes "V \<in> I"
  shows "(V, zero_str V) \<in> zero_stalk V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V, \<zero>\<^bsub>V\<^esub>) \<in> zero_stalk V
[PROOF STEP]
by (simp add: assms zero_stalk_def class_of_def class_of_0_in equivalence.Class_self rel_is_equivalence)


[STATEMENT]
lemma in_one_stalk [simp]:
  assumes "V \<in> I"
  shows "(V, one_str V) \<in> one_stalk V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V, \<one>\<^bsub>V\<^esub>) \<in> one_stalk V
[PROOF STEP]
by (simp add: assms one_stalk_def class_of_def class_of_1_in equivalence.Class_self rel_is_equivalence)


[STATEMENT]
lemma universal_property_for_stalk:
  fixes A:: "'c set" and \<psi>:: "'a set \<Rightarrow> ('b \<Rightarrow> 'c)"
  assumes ringA: "ring A add mult zero one"
    and hom: "\<And>U. U \<in> neighborhoods x \<Longrightarrow> ring_homomorphism (\<psi> U) (\<FF> U) (+\<^bsub>U\<^esub>) (\<cdot>\<^bsub>U\<^esub>) \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> A add mult zero one"
    and eq: "\<And>U V s. \<lbrakk>U \<in> neighborhoods x; V \<in> neighborhoods x; V\<subseteq>U; s \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<psi> V \<circ> \<rho> U V) s = \<psi> U s"
  shows "\<forall>V\<in>(neighborhoods x). \<exists>!u. ring_homomorphism u
carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one
\<and> (\<forall>U\<in>(neighborhoods x). \<forall>s\<in>(\<FF> U). (u \<circ> canonical_fun U) s = \<psi> U s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)
[PROOF STEP]
note neighborhoods_eq [simp]
[PROOF STATE]
proof (state)
this:
neighborhoods x = I

goal (1 subgoal):
 1. \<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)
[PROOF STEP]
have "\<forall>V\<in>I. \<exists>!u. ring_homomorphism u carrier_direct_lim add_rel mult_rel
                      \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and>
                          (\<forall>U\<in>I. \<forall>x\<in>\<FF> U. (u \<circ> canonical_fun U) x = \<psi> U x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V\<in>I. \<exists>!u. ring_homomorphism u carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and> (\<forall>U\<in>I. \<forall>x\<in>\<FF> U. (u \<circ> canonical_fun U) x = \<psi> U x)
[PROOF STEP]
apply (rule universal_property[OF ringA hom])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>U. U \<in> I \<Longrightarrow> U \<in> neighborhoods x
 2. \<And>U V x. \<lbrakk>U \<in> I; V \<in> I; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<psi> V \<circ> \<rho> U V) x = \<psi> U x
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?U1 \<in> neighborhoods x; ?V1 \<in> neighborhoods x; ?V1 \<subseteq> ?U1; ?s1 \<in> \<FF> ?U1\<rbrakk> \<Longrightarrow> (\<psi> ?V1 \<circ> \<rho> ?U1 ?V1) ?s1 = \<psi> ?U1 ?s1

goal (2 subgoals):
 1. \<And>U. U \<in> I \<Longrightarrow> U \<in> neighborhoods x
 2. \<And>U V x. \<lbrakk>U \<in> I; V \<in> I; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (\<psi> V \<circ> \<rho> U V) x = \<psi> U x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>I. \<exists>!u. ring_homomorphism u carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and> (\<forall>U\<in>I. \<forall>x\<in>\<FF> U. (u \<circ> canonical_fun U) x = \<psi> U x)

goal (1 subgoal):
 1. \<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>I. \<exists>!u. ring_homomorphism u carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and> (\<forall>U\<in>I. \<forall>x\<in>\<FF> U. (u \<circ> canonical_fun U) x = \<psi> U x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>I. \<exists>!u. ring_homomorphism u carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and> (\<forall>U\<in>I. \<forall>x\<in>\<FF> U. (u \<circ> canonical_fun U) x = \<psi> U x)

goal (1 subgoal):
 1. \<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)
[PROOF STEP]
unfolding carrier_stalk_def add_stalk_def mult_stalk_def zero_stalk_def one_stalk_def
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>I. \<exists>!u. ring_homomorphism u carrier_direct_lim add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and> (\<forall>U\<in>I. \<forall>x\<in>\<FF> U. (u \<circ> canonical_fun U) x = \<psi> U x)

goal (1 subgoal):
 1. \<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u (dlim \<FF> \<rho> (neighborhoods x)) add_rel mult_rel \<lfloor>V, \<zero>\<^bsub>V\<^esub>\<rfloor> \<lfloor>V, \<one>\<^bsub>V\<^esub>\<rfloor> A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>neighborhoods x. \<exists>!u. ring_homomorphism u carrier_stalk add_stalk mult_stalk (zero_stalk V) (one_stalk V) A add mult zero one \<and> (\<forall>U\<in>neighborhoods x. \<forall>s\<in>\<FF> U. (u \<circ> canonical_fun U) s = \<psi> U s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma psubset_ring: "I \<subset> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subset> R
[PROOF STEP]
using neq_ring
[PROOF STATE]
proof (prove)
using this:
I \<noteq> R

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


[STATEMENT]
lemma subset: "I \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> R
[PROOF STEP]
by blast


[STATEMENT]
lemma has_one_imp_equal:
  assumes "\<one> \<in> I"
  shows "I = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I = R
[PROOF STEP]
by (metis assms lideal subset multiplicative.right_unit subsetI subset_antisym)


[STATEMENT]
lemma (in comm_ring) ideal_iff_lideal:
  "ideal I R (+) (\<cdot>) \<zero> \<one> \<longleftrightarrow> lideal I R (+) (\<cdot>) \<zero> \<one>" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal I R (+) (\<cdot>) \<zero> \<one> = lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> lideal I R (+) (\<cdot>) \<zero> \<one>
 2. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
ideal I R (+) (\<cdot>) \<zero> \<one>

goal (2 subgoals):
 1. ideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> lideal I R (+) (\<cdot>) \<zero> \<one>
 2. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
interpret I: ideal I R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
using this:
ideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> lideal I R (+) (\<cdot>) \<zero> \<one>
 2. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> R; a \<in> I\<rbrakk> \<Longrightarrow> r \<cdot> a \<in> I
[PROOF STEP]
qed (use I.ideal in presburger)
[PROOF STATE]
proof (state)
this:
lideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
lideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
interpret I: lideal I R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
using this:
lideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> I
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> I
[PROOF STEP]
fix r a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> I
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> I
[PROOF STEP]
assume "r \<in> R" "a \<in> I"
[PROOF STATE]
proof (state)
this:
r \<in> R
a \<in> I

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> a \<cdot> b \<in> I
 2. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
a \<in> I
[PROOF STEP]
show "r \<cdot> a \<in> I"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
a \<in> I

goal (1 subgoal):
 1. r \<cdot> a \<in> I
[PROOF STEP]
using I.lideal
[PROOF STATE]
proof (prove)
using this:
r \<in> R
a \<in> I
\<lbrakk>?r \<in> R; ?a \<in> I\<rbrakk> \<Longrightarrow> ?r \<cdot> ?a \<in> I

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> R; b \<in> I\<rbrakk> \<Longrightarrow> b \<cdot> a \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<cdot> a \<in> I
[PROOF STEP]
show "a \<cdot> r \<in> I"
[PROOF STATE]
proof (prove)
using this:
r \<cdot> a \<in> I

goal (1 subgoal):
 1. a \<cdot> r \<in> I
[PROOF STEP]
by (simp add: \<open>a \<in> I\<close> \<open>r \<in> R\<close> comm_mult)
[PROOF STATE]
proof (state)
this:
a \<cdot> r \<in> I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal I R (+) (\<cdot>) \<zero> \<one>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in comm_ring) max_ideal_iff_max_lideal:
  "max_ideal R I (+) (\<cdot>) \<zero> \<one> \<longleftrightarrow> max_lideal I R (+) (\<cdot>) \<zero> \<one>" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal R I (+) (\<cdot>) \<zero> \<one> = max_lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. max_ideal R I (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_lideal I R (+) (\<cdot>) \<zero> \<one>
 2. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
max_ideal R I (+) (\<cdot>) \<zero> \<one>

goal (2 subgoals):
 1. max_ideal R I (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_lideal I R (+) (\<cdot>) \<zero> \<one>
 2. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
interpret I: max_ideal R I "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
using this:
max_ideal R I (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. max_ideal R I (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_lideal I R (+) (\<cdot>) \<zero> \<one>
 2. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lideal_axioms I R (\<cdot>)
 2. max_lideal_axioms I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show "lideal_axioms I R (\<cdot>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal_axioms I R (\<cdot>)
[PROOF STEP]
by (simp add: I.ideal(1) lideal_axioms.intro)
[PROOF STATE]
proof (state)
this:
lideal_axioms I R (\<cdot>)

goal (1 subgoal):
 1. max_lideal_axioms I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show "max_lideal_axioms I R (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal_axioms I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (simp add: I.is_max I.neq_ring ideal_iff_lideal max_lideal_axioms.intro)
[PROOF STATE]
proof (state)
this:
max_lideal_axioms I R (+) (\<cdot>) \<zero> \<one>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max_lideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
max_lideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
interpret I: max_lideal I R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
using this:
max_lideal I R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. max_lideal I R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal I R (+) (\<cdot>) \<zero> \<one> \<Longrightarrow> max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ideal_axioms I R (\<cdot>)
 2. max_ideal_axioms R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show "ideal_axioms I R (\<cdot>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_axioms I R (\<cdot>)
[PROOF STEP]
by (meson I.lideal_axioms ideal_def ideal_iff_lideal)
[PROOF STATE]
proof (state)
this:
ideal_axioms I R (\<cdot>)

goal (1 subgoal):
 1. max_ideal_axioms R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
show "max_ideal_axioms R I (+) (\<cdot>) \<zero> \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal_axioms R I (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (meson I.is_max I.neq_ring ideal_iff_lideal max_ideal_axioms.intro)
[PROOF STATE]
proof (state)
this:
max_ideal_axioms R I (+) (\<cdot>) \<zero> \<one>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max_ideal R I (+) (\<cdot>) \<zero> \<one>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma im_of_ideal_is_ideal:
  assumes I: "ideal I A addA multA zeroA oneA"
    and f: "ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "ideal (f ` I) B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
interpret IA: ideal I A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal I A addA multA zeroA oneA
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
ideal I A addA multA zeroA oneA

goal (1 subgoal):
 1. ideal I A addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
interpret fepi: ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms (f ` I) B addB zeroB
 2. Group_Theory.monoid (f ` I) addB zeroB
 3. Group_Theory.group_axioms (f ` I) addB zeroB
 4. ideal_axioms (f ` I) B multB
[PROOF STEP]
show sma: "submonoid_axioms (f ` I) B addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms (f ` I) B addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f ` I \<subseteq> B
 2. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 3. zeroB \<in> f ` I
[PROOF STEP]
show "f ` I \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` I \<subseteq> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` I \<subseteq> B

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
[PROOF STEP]
have "zeroA \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroA \<in> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
zeroA \<in> I

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zeroA \<in> I
[PROOF STEP]
show "zeroB \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
zeroA \<in> I

goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
using fepi.additive.commutes_with_unit
[PROOF STATE]
proof (prove)
using this:
zeroA \<in> I
f zeroA = zeroB

goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
zeroB \<in> f ` I

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
fix b1 b2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
assume "b1 \<in> f ` I" and "b2 \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b1 \<in> f ` I
b2 \<in> f ` I

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b1 \<in> f ` I
b2 \<in> f ` I
[PROOF STEP]
show "addB b1 b2 \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
b1 \<in> f ` I
b2 \<in> f ` I

goal (1 subgoal):
 1. addB b1 b2 \<in> f ` I
[PROOF STEP]
unfolding image_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>I. b1 = f x
\<exists>x\<in>I. b2 = f x

goal (1 subgoal):
 1. \<exists>x\<in>I. addB b1 b2 = f x
[PROOF STEP]
by (metis IA.additive.sub IA.additive.sub_composition_closed fepi.additive.commutes_with_composition)
[PROOF STATE]
proof (state)
this:
addB b1 b2 \<in> f ` I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
submonoid_axioms (f ` I) B addB zeroB

goal (3 subgoals):
 1. Group_Theory.monoid (f ` I) addB zeroB
 2. Group_Theory.group_axioms (f ` I) addB zeroB
 3. ideal_axioms (f ` I) B multB
[PROOF STEP]
show "Group_Theory.monoid (f ` I) addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (f ` I) addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
 3. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 5. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
 3. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 5. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
assume "a \<in> f ` I" "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
a \<in> f ` I
b \<in> f ` I

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

goal (1 subgoal):
 1. addB a b \<in> f ` I
[PROOF STEP]
by (meson sma submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
addB a b \<in> f ` I

goal (4 subgoals):
 1. zeroB \<in> f ` I
 2. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 3. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. zeroB \<in> f ` I
 2. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 3. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
show "zeroB \<in> f ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
using fepi.additive.commutes_with_unit
[PROOF STATE]
proof (prove)
using this:
f zeroA = zeroB

goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
zeroB \<in> f ` I

goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 2. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 3. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f ` I) addB zeroB

goal (2 subgoals):
 1. Group_Theory.group_axioms (f ` I) addB zeroB
 2. ideal_axioms (f ` I) B multB
[PROOF STEP]
show "Group_Theory.group_axioms (f ` I) addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms (f ` I) addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
assume "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b \<in> f ` I

goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> f ` I
[PROOF STEP]
obtain i where "b = f i" "i \<in> I"
[PROOF STATE]
proof (prove)
using this:
b \<in> f ` I

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>b = f i; i \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = f i
i \<in> I

goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = f i
i \<in> I
[PROOF STEP]
obtain j where "addA i j = zeroA" "j \<in> I"
[PROOF STATE]
proof (prove)
using this:
b = f i
i \<in> I

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>addA i j = zeroA; j \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using IA.additive.sub.invertible_right_inverse
[PROOF STATE]
proof (prove)
using this:
b = f i
i \<in> I
\<lbrakk>IA.additive.sub.invertible ?u; ?u \<in> I\<rbrakk> \<Longrightarrow> addA ?u (IA.additive.sub.inverse ?u) = zeroA

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>addA i j = zeroA; j \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
addA i j = zeroA
j \<in> I

goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
addA i j = zeroA
j \<in> I
[PROOF STEP]
show "monoid.invertible (f ` I) addB zeroB b"
[PROOF STATE]
proof (prove)
using this:
addA i j = zeroA
j \<in> I

goal (1 subgoal):
 1. monoid.invertible (f ` I) addB zeroB b
[PROOF STEP]
by (metis IA.additive.commutative IA.additive.sub \<open>Group_Theory.monoid (f ` I) addB zeroB\<close> \<open>b = f i\<close> \<open>i \<in> I\<close> fepi.additive.commutes_with_composition fepi.additive.commutes_with_unit image_eqI monoid.invertibleI)
[PROOF STATE]
proof (state)
this:
monoid.invertible (f ` I) addB zeroB b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (f ` I) addB zeroB

goal (1 subgoal):
 1. ideal_axioms (f ` I) B multB
[PROOF STEP]
show "ideal_axioms (f ` I) B multB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_axioms (f ` I) B multB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 2. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
fix b fi
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 2. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
assume "b \<in> B" and "fi \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b \<in> B
fi \<in> f ` I

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 2. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> B
fi \<in> f ` I
[PROOF STEP]
obtain i where i: "fi = f i" "i \<in> I"
[PROOF STATE]
proof (prove)
using this:
b \<in> B
fi \<in> f ` I

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>fi = f i; i \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fi = f i
i \<in> I

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 2. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
obtain a where a: "a \<in> A" "f a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; f a = b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>b \<in> B\<close> fepi.surjective
[PROOF STATE]
proof (prove)
using this:
b \<in> B
f ` A = B

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; f a = b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
f a = b

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 2. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
f a = b
[PROOF STEP]
show "multB b fi \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
f a = b

goal (1 subgoal):
 1. multB b fi \<in> f ` I
[PROOF STEP]
by (metis IA.additive.submonoid_axioms IA.ideal(1) \<open>fi = f i\<close> \<open>i \<in> I\<close> fepi.multiplicative.commutes_with_composition image_iff submonoid.sub)
[PROOF STATE]
proof (state)
this:
multB b fi \<in> f ` I

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multB b fi \<in> f ` I
[PROOF STEP]
show "multB fi b \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
multB b fi \<in> f ` I

goal (1 subgoal):
 1. multB fi b \<in> f ` I
[PROOF STEP]
by (metis IA.additive.sub IA.ideal(2) a i fepi.multiplicative.commutes_with_composition imageI)
[PROOF STATE]
proof (state)
this:
multB fi b \<in> f ` I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_axioms (f ` I) B multB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal (f ` I) B addB multB zeroB oneB

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma im_of_lideal_is_lideal:
  assumes I: "lideal I A addA multA zeroA oneA"
    and f: "ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "lideal (f ` I) B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
interpret IA: lideal I A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal I A addA multA zeroA oneA
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
lideal I A addA multA zeroA oneA

goal (1 subgoal):
 1. lideal I A addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
interpret fepi: ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ring_epimorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms (f ` I) B addB zeroB
 2. Group_Theory.monoid (f ` I) addB zeroB
 3. Group_Theory.group_axioms (f ` I) addB zeroB
 4. lideal_axioms (f ` I) B multB
[PROOF STEP]
show sma: "submonoid_axioms (f ` I) B addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms (f ` I) B addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f ` I \<subseteq> B
 2. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 3. zeroB \<in> f ` I
[PROOF STEP]
show "f ` I \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` I \<subseteq> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` I \<subseteq> B

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
[PROOF STEP]
have "zeroA \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroA \<in> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
zeroA \<in> I

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zeroA \<in> I
[PROOF STEP]
show "zeroB \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
zeroA \<in> I

goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
using fepi.additive.commutes_with_unit
[PROOF STATE]
proof (prove)
using this:
zeroA \<in> I
f zeroA = zeroB

goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
zeroB \<in> f ` I

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
fix b1 b2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
assume "b1 \<in> f ` I" and "b2 \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b1 \<in> f ` I
b2 \<in> f ` I

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b1 \<in> f ` I
b2 \<in> f ` I
[PROOF STEP]
show "addB b1 b2 \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
b1 \<in> f ` I
b2 \<in> f ` I

goal (1 subgoal):
 1. addB b1 b2 \<in> f ` I
[PROOF STEP]
unfolding image_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>I. b1 = f x
\<exists>x\<in>I. b2 = f x

goal (1 subgoal):
 1. \<exists>x\<in>I. addB b1 b2 = f x
[PROOF STEP]
by (metis IA.additive.sub IA.additive.sub_composition_closed fepi.additive.commutes_with_composition)
[PROOF STATE]
proof (state)
this:
addB b1 b2 \<in> f ` I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
submonoid_axioms (f ` I) B addB zeroB

goal (3 subgoals):
 1. Group_Theory.monoid (f ` I) addB zeroB
 2. Group_Theory.group_axioms (f ` I) addB zeroB
 3. lideal_axioms (f ` I) B multB
[PROOF STEP]
show "Group_Theory.monoid (f ` I) addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (f ` I) addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
 3. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 5. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 2. zeroB \<in> f ` I
 3. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 5. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
assume "a \<in> f ` I" "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
a \<in> f ` I
b \<in> f ` I

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

goal (1 subgoal):
 1. addB a b \<in> f ` I
[PROOF STEP]
by (meson sma submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
addB a b \<in> f ` I

goal (4 subgoals):
 1. zeroB \<in> f ` I
 2. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 3. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. zeroB \<in> f ` I
 2. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 3. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 4. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
show "zeroB \<in> f ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
using fepi.additive.commutes_with_unit
[PROOF STATE]
proof (prove)
using this:
f zeroA = zeroB

goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
zeroB \<in> f ` I

goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> f ` I; b \<in> f ` I; c \<in> f ` I\<rbrakk> \<Longrightarrow> addB (addB a b) c = addB a (addB b c)
 2. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 3. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f ` I) addB zeroB

goal (2 subgoals):
 1. Group_Theory.group_axioms (f ` I) addB zeroB
 2. lideal_axioms (f ` I) B multB
[PROOF STEP]
show "Group_Theory.group_axioms (f ` I) addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms (f ` I) addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
assume "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b \<in> f ` I

goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> f ` I
[PROOF STEP]
obtain i where "b = f i" "i \<in> I"
[PROOF STATE]
proof (prove)
using this:
b \<in> f ` I

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>b = f i; i \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = f i
i \<in> I

goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = f i
i \<in> I
[PROOF STEP]
obtain j where "addA i j = zeroA" "j \<in> I"
[PROOF STATE]
proof (prove)
using this:
b = f i
i \<in> I

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>addA i j = zeroA; j \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using IA.additive.sub.invertible_right_inverse
[PROOF STATE]
proof (prove)
using this:
b = f i
i \<in> I
\<lbrakk>IA.additive.sub.invertible ?u; ?u \<in> I\<rbrakk> \<Longrightarrow> addA ?u (IA.additive.sub.inverse ?u) = zeroA

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>addA i j = zeroA; j \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
addA i j = zeroA
j \<in> I

goal (1 subgoal):
 1. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
addA i j = zeroA
j \<in> I
[PROOF STEP]
show "monoid.invertible (f ` I) addB zeroB b"
[PROOF STATE]
proof (prove)
using this:
addA i j = zeroA
j \<in> I

goal (1 subgoal):
 1. monoid.invertible (f ` I) addB zeroB b
[PROOF STEP]
by (metis IA.additive.commutative IA.additive.sub \<open>Group_Theory.monoid (f ` I) addB zeroB\<close> \<open>b = f i\<close> \<open>i \<in> I\<close> fepi.additive.commutes_with_composition fepi.additive.commutes_with_unit image_eqI monoid.invertibleI)
[PROOF STATE]
proof (state)
this:
monoid.invertible (f ` I) addB zeroB b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (f ` I) addB zeroB

goal (1 subgoal):
 1. lideal_axioms (f ` I) B multB
[PROOF STEP]
show "lideal_axioms (f ` I) B multB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal_axioms (f ` I) B multB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> B; a \<in> f ` I\<rbrakk> \<Longrightarrow> multB r a \<in> f ` I
[PROOF STEP]
fix b fi
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> B; a \<in> f ` I\<rbrakk> \<Longrightarrow> multB r a \<in> f ` I
[PROOF STEP]
assume "b \<in> B" and "fi \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b \<in> B
fi \<in> f ` I

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> B; a \<in> f ` I\<rbrakk> \<Longrightarrow> multB r a \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> B
fi \<in> f ` I
[PROOF STEP]
obtain i where i: "fi = f i" "i \<in> I"
[PROOF STATE]
proof (prove)
using this:
b \<in> B
fi \<in> f ` I

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>fi = f i; i \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fi = f i
i \<in> I

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> B; a \<in> f ` I\<rbrakk> \<Longrightarrow> multB r a \<in> f ` I
[PROOF STEP]
obtain a where a: "a \<in> A" "f a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; f a = b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>b \<in> B\<close> fepi.surjective
[PROOF STATE]
proof (prove)
using this:
b \<in> B
f ` A = B

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; f a = b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
f a = b

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> B; a \<in> f ` I\<rbrakk> \<Longrightarrow> multB r a \<in> f ` I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
f a = b
[PROOF STEP]
show "multB b fi \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
f a = b

goal (1 subgoal):
 1. multB b fi \<in> f ` I
[PROOF STEP]
by (metis IA.additive.submonoid_axioms IA.lideal(1) \<open>fi = f i\<close> \<open>i \<in> I\<close> fepi.multiplicative.commutes_with_composition image_iff submonoid.sub)
[PROOF STATE]
proof (state)
this:
multB b fi \<in> f ` I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lideal_axioms (f ` I) B multB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lideal (f ` I) B addB multB zeroB oneB

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. max_lideal I A addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
interpret fiso: 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]
using f
[PROOF STATE]
proof (prove)
using this:
ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
interpret fIB: lideal "f ` I" B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms (f ` I) B addB zeroB
 2. Group_Theory.monoid (f ` I) addB zeroB
 3. Group_Theory.group_axioms (f ` I) addB zeroB
 4. lideal_axioms (f ` I) B multB
[PROOF STEP]
show "submonoid_axioms (f ` I) B addB zeroB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms (f ` I) B addB zeroB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f ` I \<subseteq> B
 2. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<in> f ` I
 3. zeroB \<in> f ` I
[PROOF STEP]
show "addB a b \<in> f ` I"
        if "a \<in> f ` I" "b \<in> f ` I" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addB a b \<in> f ` I
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> f ` I
b \<in> f ` I

goal (1 subgoal):
 1. addB a b \<in> f ` I
[PROOF STEP]
by (clarsimp simp: image_iff) (metis fiso.additive.commutes_with_composition maxI.additive.sub maxI.additive.sub_composition_closed)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a1 \<in> f ` I; ?b1 \<in> f ` I\<rbrakk> \<Longrightarrow> addB ?a1 ?b1 \<in> f ` I

goal (2 subgoals):
 1. f ` I \<subseteq> B
 2. zeroB \<in> f ` I
[PROOF STEP]
qed (use fiso.additive.commutes_with_unit in auto)
[PROOF STATE]
proof (state)
this:
submonoid_axioms (f ` I) B addB zeroB

goal (3 subgoals):
 1. Group_Theory.monoid (f ` I) addB zeroB
 2. Group_Theory.group_axioms (f ` I) addB zeroB
 3. lideal_axioms (f ` I) B multB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
submonoid_axioms (f ` I) B addB zeroB
[PROOF STEP]
show "Group_Theory.monoid (f ` I) addB zeroB"
[PROOF STATE]
proof (prove)
using this:
submonoid_axioms (f ` I) B addB zeroB

goal (1 subgoal):
 1. Group_Theory.monoid (f ` I) addB zeroB
[PROOF STEP]
using fiso.target.additive.monoid_axioms
[PROOF STATE]
proof (prove)
using this:
submonoid_axioms (f ` I) B addB zeroB
Group_Theory.monoid B addB zeroB

goal (1 subgoal):
 1. Group_Theory.monoid (f ` I) addB zeroB
[PROOF STEP]
unfolding submonoid_axioms_def monoid_def
[PROOF STATE]
proof (prove)
using this:
f ` I \<subseteq> B \<and> (\<forall>a b. a \<in> f ` I \<longrightarrow> b \<in> f ` I \<longrightarrow> addB a b \<in> f ` I) \<and> zeroB \<in> f ` I
((\<forall>a b. a \<in> B \<longrightarrow> b \<in> B \<longrightarrow> addB a b \<in> B) \<and> zeroB \<in> B) \<and> (\<forall>a b c. a \<in> B \<longrightarrow> b \<in> B \<longrightarrow> c \<in> B \<longrightarrow> addB (addB a b) c = addB a (addB b c)) \<and> (\<forall>a. a \<in> B \<longrightarrow> addB zeroB a = a) \<and> (\<forall>a. a \<in> B \<longrightarrow> addB a zeroB = a)

goal (1 subgoal):
 1. ((\<forall>a b. a \<in> f ` I \<longrightarrow> b \<in> f ` I \<longrightarrow> addB a b \<in> f ` I) \<and> zeroB \<in> f ` I) \<and> (\<forall>a b c. a \<in> f ` I \<longrightarrow> b \<in> f ` I \<longrightarrow> c \<in> f ` I \<longrightarrow> addB (addB a b) c = addB a (addB b c)) \<and> (\<forall>a. a \<in> f ` I \<longrightarrow> addB zeroB a = a) \<and> (\<forall>a. a \<in> f ` I \<longrightarrow> addB a zeroB = a)
[PROOF STEP]
by (meson subsetD)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f ` I) addB zeroB

goal (2 subgoals):
 1. Group_Theory.group_axioms (f ` I) addB zeroB
 2. lideal_axioms (f ` I) B multB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Group_Theory.monoid (f ` I) addB zeroB
[PROOF STEP]
show "Group_Theory.group_axioms (f ` I) addB zeroB"
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid (f ` I) addB zeroB

goal (1 subgoal):
 1. Group_Theory.group_axioms (f ` I) addB zeroB
[PROOF STEP]
apply (clarsimp simp:  Group_Theory.group_axioms_def image_iff monoid.invertible_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Group_Theory.monoid (f ` I) addB zeroB; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>v\<in>I. addB (f x) (f v) = zeroB \<and> addB (f v) (f x) = zeroB
[PROOF STEP]
by (metis fiso.additive.commutes_with_composition fiso.additive.commutes_with_unit maxI.additive.sub maxI.additive.sub.invertible maxI.additive.sub.invertible_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (f ` I) addB zeroB

goal (1 subgoal):
 1. lideal_axioms (f ` I) B multB
[PROOF STEP]
have "\<And>r x. \<lbrakk>r \<in> B; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>I. multB r (f x) = f xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>r \<in> B; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>I. multB r (f x) = f xa
[PROOF STEP]
by (metis (no_types, lifting) fiso.multiplicative.commutes_with_composition fiso.surjective image_iff maxI.additive.sub maxI.lideal)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?r1 \<in> B; ?x1 \<in> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>I. multB ?r1 (f ?x1) = f xa

goal (1 subgoal):
 1. lideal_axioms (f ` I) B multB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?r1 \<in> B; ?x1 \<in> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>I. multB ?r1 (f ?x1) = f xa
[PROOF STEP]
show "lideal_axioms (f ` I) B multB"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r1 \<in> B; ?x1 \<in> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>I. multB ?r1 (f ?x1) = f xa

goal (1 subgoal):
 1. lideal_axioms (f ` I) B multB
[PROOF STEP]
by (force intro!: lideal_axioms.intro)
[PROOF STATE]
proof (state)
this:
lideal_axioms (f ` I) B multB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
proof unfold_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` I \<noteq> B
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
show "f ` I \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` I \<noteq> B
[PROOF STEP]
using maxI.neq_ring fiso.bijective maxI.additive.submonoid_axioms
[PROOF STATE]
proof (prove)
using this:
I \<noteq> A
bij_betw f A B
submonoid I A addA zeroA

goal (1 subgoal):
 1. f ` I \<noteq> B
[PROOF STEP]
unfolding submonoid_axioms_def submonoid_def
[PROOF STATE]
proof (prove)
using this:
I \<noteq> A
bij_betw f A B
Group_Theory.monoid A addA zeroA \<and> I \<subseteq> A \<and> (\<forall>a b. a \<in> I \<longrightarrow> b \<in> I \<longrightarrow> addA a b \<in> I) \<and> zeroA \<in> I

goal (1 subgoal):
 1. f ` I \<noteq> B
[PROOF STEP]
by (metis bij_betw_imp_inj_on fiso.surjective inj_on_image_eq_iff subset_iff)
[PROOF STATE]
proof (state)
this:
f ` I \<noteq> B

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
fix J
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
assume "lideal J B addB multB zeroB oneB" and "J \<noteq> B" and fim: "f ` I \<subseteq> J"
[PROOF STATE]
proof (state)
this:
lideal J B addB multB zeroB oneB
J \<noteq> B
f ` I \<subseteq> J

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lideal J B addB multB zeroB oneB
J \<noteq> B
f ` I \<subseteq> J
[PROOF STEP]
interpret JB: lideal J B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
using this:
lideal J B addB multB zeroB oneB
J \<noteq> B
f ` I \<subseteq> J

goal (1 subgoal):
 1. lideal J B addB multB zeroB oneB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
have \<section>: "lideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA
 2. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
 3. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
 4. lideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show sma: "submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<^sup>\<inverse> A J \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> f \<^sup>\<inverse> A J; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> addA a b \<in> f \<^sup>\<inverse> A J
 3. zeroA \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "addA a b \<in> f \<^sup>\<inverse> A J" if "a \<in> f \<^sup>\<inverse> A J" and "b \<in> f \<^sup>\<inverse> A J" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addA a b \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> f \<^sup>\<inverse> A J
b \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. addA a b \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f a \<in> J; a \<in> A; f b \<in> J; b \<in> A\<rbrakk> \<Longrightarrow> f (addA a b) \<in> J
[PROOF STEP]
using JB.additive.sub_composition_closed fiso.additive.commutes_with_composition
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> J; ?b \<in> J\<rbrakk> \<Longrightarrow> addB ?a ?b \<in> J
\<lbrakk>?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> f (addA ?x ?y) = addB (f ?x) (f ?y)

goal (1 subgoal):
 1. \<lbrakk>f a \<in> J; a \<in> A; f b \<in> J; b \<in> A\<rbrakk> \<Longrightarrow> f (addA a b) \<in> J
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a1 \<in> f \<^sup>\<inverse> A J; ?b1 \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> addA ?a1 ?b1 \<in> f \<^sup>\<inverse> A J

goal (2 subgoals):
 1. f \<^sup>\<inverse> A J \<subseteq> A
 2. zeroA \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
qed blast+
[PROOF STATE]
proof (state)
this:
submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
 3. lideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show "Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
[PROOF STEP]
by (smt (verit, ccfv_threshold) Group_Theory.monoid.intro IntD2 sma maxI.additive.associative maxI.additive.left_unit maxI.additive.right_unit submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA

goal (2 subgoals):
 1. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
 2. lideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show "Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f \<^sup>\<inverse> A J \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA u
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f \<^sup>\<inverse> A J \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA u
[PROOF STEP]
assume "x \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (state)
this:
x \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. \<And>u. u \<in> f \<^sup>\<inverse> A J \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x"
[PROOF STATE]
proof (prove)
using this:
x \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> A; f x \<in> J\<rbrakk> \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x
[PROOF STEP]
by (smt (verit, best) JB.additive.sub.invertible JB.additive.submonoid_inverse_closed IntI \<open>Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA\<close> fiso.additive.invertible_commutes_with_inverse maxI.additive.inverse_equality maxI.additive.invertible maxI.additive.invertibleE monoid.invertible_def vimageI)
[PROOF STATE]
proof (state)
this:
monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA

goal (1 subgoal):
 1. lideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show "lideal_axioms (f \<^sup>\<inverse> A J) A multA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> A; a \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA r a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
fix a j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> A; a \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA r a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
assume \<section>: "a \<in> A" "j \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (state)
this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. \<And>r a. \<lbrakk>r \<in> A; a \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA r a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "multA a j \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
using JB.lideal(1) fiso.map_closed fiso.multiplicative.commutes_with_composition
[PROOF STATE]
proof (prove)
using this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J
\<lbrakk>?r \<in> B; ?a \<in> J\<rbrakk> \<Longrightarrow> multB ?r ?a \<in> J
?a \<in> A \<Longrightarrow> f ?a \<in> B
\<lbrakk>?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> f (multA ?x ?y) = multB (f ?x) (f ?y)

goal (1 subgoal):
 1. multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multA a j \<in> f \<^sup>\<inverse> A J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lideal_axioms (f \<^sup>\<inverse> A J) A multA

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
have "I = f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I = f \<^sup>\<inverse> A J
[PROOF STEP]
proof (rule maxI.is_max [OF \<section>])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<^sup>\<inverse> A J \<noteq> A
 2. I \<subseteq> f \<^sup>\<inverse> A J
[PROOF STEP]
show "f \<^sup>\<inverse> A J \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<^sup>\<inverse> A J \<noteq> A
[PROOF STEP]
using JB.additive.sub \<open>J \<noteq> B\<close> fiso.surjective
[PROOF STATE]
proof (prove)
using this:
?a \<in> J \<Longrightarrow> ?a \<in> B
J \<noteq> B
f ` A = B

goal (1 subgoal):
 1. f \<^sup>\<inverse> A J \<noteq> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<^sup>\<inverse> A J \<noteq> A

goal (1 subgoal):
 1. I \<subseteq> f \<^sup>\<inverse> A J
[PROOF STEP]
show "I \<subseteq> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> f \<^sup>\<inverse> A J
[PROOF STEP]
by (meson fim image_subset_iff_subset_vimage inf_greatest maxI.additive.sub subset_iff)
[PROOF STATE]
proof (state)
this:
I \<subseteq> f \<^sup>\<inverse> A J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
I = f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I = f \<^sup>\<inverse> A J
[PROOF STEP]
have "J \<subseteq> f ` I"
[PROOF STATE]
proof (prove)
using this:
I = f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. J \<subseteq> f ` I
[PROOF STEP]
using JB.additive.sub fiso.surjective
[PROOF STATE]
proof (prove)
using this:
I = f \<^sup>\<inverse> A J
?a \<in> J \<Longrightarrow> ?a \<in> B
f ` A = B

goal (1 subgoal):
 1. J \<subseteq> f ` I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
J \<subseteq> f ` I

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
with fim
[PROOF STATE]
proof (chain)
picking this:
f ` I \<subseteq> J
J \<subseteq> f ` I
[PROOF STEP]
show "f ` I = J"
[PROOF STATE]
proof (prove)
using this:
f ` I \<subseteq> J
J \<subseteq> f ` I

goal (1 subgoal):
 1. f ` I = J
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f ` I = J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max_lideal (f ` I) B addB multB zeroB oneB

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. max_ideal A I addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_ideal B (f ` I) addB multB zeroB oneB
[PROOF STEP]
interpret fiso: 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]
using f
[PROOF STATE]
proof (prove)
using this:
ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_ideal B (f ` I) addB multB zeroB oneB
[PROOF STEP]
interpret fIB: ideal "f ` I" B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
using maxI.ideal_axioms fiso.ring_homomorphism_axioms
[PROOF STATE]
proof (prove)
using this:
ideal I A addA multA zeroA oneA
ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ideal (f ` I) B addB multB zeroB oneB
[PROOF STEP]
by (meson fiso.ring_epimorphism_axioms im_of_ideal_is_ideal)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_ideal B (f ` I) addB multB zeroB oneB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal B (f ` I) addB multB zeroB oneB
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. comm_ring_axioms B multB
 2. max_ideal_axioms B (f ` I) addB multB zeroB oneB
[PROOF STEP]
show "comm_ring_axioms B multB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_ring_axioms B multB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> B\<rbrakk> \<Longrightarrow> multB a b = multB b a
[PROOF STEP]
fix b1 b2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> B\<rbrakk> \<Longrightarrow> multB a b = multB b a
[PROOF STEP]
assume "b1 \<in> B" and "b2 \<in> B"
[PROOF STATE]
proof (state)
this:
b1 \<in> B
b2 \<in> B

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> B\<rbrakk> \<Longrightarrow> multB a b = multB b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b1 \<in> B
b2 \<in> B
[PROOF STEP]
obtain a1 a2 where a1: "a1 \<in> A" "f a1 = b1" and a2: "a2 \<in> A" "f a2 = b2"
[PROOF STATE]
proof (prove)
using this:
b1 \<in> B
b2 \<in> B

goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>a1 \<in> A; f a1 = b1; a2 \<in> A; f a2 = b2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using fiso.surjective
[PROOF STATE]
proof (prove)
using this:
b1 \<in> B
b2 \<in> B
f ` A = B

goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>a1 \<in> A; f a1 = b1; a2 \<in> A; f a2 = b2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a1 \<in> A
f a1 = b1
a2 \<in> A
f a2 = b2

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> B\<rbrakk> \<Longrightarrow> multB a b = multB b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a1 \<in> A
f a1 = b1
a2 \<in> A
f a2 = b2
[PROOF STEP]
have "multA a1 a2 = multA a2 a1"
[PROOF STATE]
proof (prove)
using this:
a1 \<in> A
f a1 = b1
a2 \<in> A
f a2 = b2

goal (1 subgoal):
 1. multA a1 a2 = multA a2 a1
[PROOF STEP]
using maxI.comm_mult
[PROOF STATE]
proof (prove)
using this:
a1 \<in> A
f a1 = b1
a2 \<in> A
f a2 = b2
\<lbrakk>?a \<in> A; ?b \<in> A\<rbrakk> \<Longrightarrow> multA ?a ?b = multA ?b ?a

goal (1 subgoal):
 1. multA a1 a2 = multA a2 a1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
multA a1 a2 = multA a2 a1

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> B; b \<in> B\<rbrakk> \<Longrightarrow> multB a b = multB b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multA a1 a2 = multA a2 a1
[PROOF STEP]
show "multB b1 b2 = multB b2 b1"
[PROOF STATE]
proof (prove)
using this:
multA a1 a2 = multA a2 a1

goal (1 subgoal):
 1. multB b1 b2 = multB b2 b1
[PROOF STEP]
by (metis a1 a2 fiso.multiplicative.commutes_with_composition)
[PROOF STATE]
proof (state)
this:
multB b1 b2 = multB b2 b1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
comm_ring_axioms B multB

goal (1 subgoal):
 1. max_ideal_axioms B (f ` I) addB multB zeroB oneB
[PROOF STEP]
show "max_ideal_axioms B (f ` I) addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal_axioms B (f ` I) addB multB zeroB oneB
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` I \<noteq> B
 2. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
obtain i where "i \<in> A" "i \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> A; i \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using maxI.neq_ring
[PROOF STATE]
proof (prove)
using this:
I \<noteq> A

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> A; i \<notin> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> A
i \<notin> I

goal (2 subgoals):
 1. f ` I \<noteq> B
 2. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> A
i \<notin> I
[PROOF STEP]
have "f i \<notin> f ` I"
[PROOF STATE]
proof (prove)
using this:
i \<in> A
i \<notin> I

goal (1 subgoal):
 1. f i \<notin> f ` I
[PROOF STEP]
unfolding image_iff
[PROOF STATE]
proof (prove)
using this:
i \<in> A
i \<notin> I

goal (1 subgoal):
 1. \<not> (\<exists>x\<in>I. f i = f x)
[PROOF STEP]
by (metis fiso.injective inj_on_def maxI.additive.sub)
[PROOF STATE]
proof (state)
this:
f i \<notin> f ` I

goal (2 subgoals):
 1. f ` I \<noteq> B
 2. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f i \<notin> f ` I
[PROOF STEP]
show "f ` I \<noteq> B"
[PROOF STATE]
proof (prove)
using this:
f i \<notin> f ` I

goal (1 subgoal):
 1. f ` I \<noteq> B
[PROOF STEP]
using \<open>i \<in> A\<close> fiso.map_closed
[PROOF STATE]
proof (prove)
using this:
f i \<notin> f ` I
i \<in> A
?a \<in> A \<Longrightarrow> f ?a \<in> B

goal (1 subgoal):
 1. f ` I \<noteq> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` I \<noteq> B

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
fix J
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
assume "ideal J B addB multB zeroB oneB" and "J \<noteq> B" and fim: "f ` I \<subseteq> J"
[PROOF STATE]
proof (state)
this:
ideal J B addB multB zeroB oneB
J \<noteq> B
f ` I \<subseteq> J

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ideal J B addB multB zeroB oneB
J \<noteq> B
f ` I \<subseteq> J
[PROOF STEP]
interpret JB: ideal J B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
using this:
ideal J B addB multB zeroB oneB
J \<noteq> B
f ` I \<subseteq> J

goal (1 subgoal):
 1. ideal J B addB multB zeroB oneB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
have \<section>: "ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA
 2. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
 3. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
 4. ideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show sma: "submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<^sup>\<inverse> A J \<subseteq> A
 2. \<And>a b. \<lbrakk>a \<in> f \<^sup>\<inverse> A J; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> addA a b \<in> f \<^sup>\<inverse> A J
 3. zeroA \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "addA a b \<in> f \<^sup>\<inverse> A J" if "a \<in> f \<^sup>\<inverse> A J" and "b \<in> f \<^sup>\<inverse> A J" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addA a b \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> f \<^sup>\<inverse> A J
b \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. addA a b \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f a \<in> J; a \<in> A; f b \<in> J; b \<in> A\<rbrakk> \<Longrightarrow> f (addA a b) \<in> J
[PROOF STEP]
using JB.additive.sub_composition_closed fiso.additive.commutes_with_composition
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> J; ?b \<in> J\<rbrakk> \<Longrightarrow> addB ?a ?b \<in> J
\<lbrakk>?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> f (addA ?x ?y) = addB (f ?x) (f ?y)

goal (1 subgoal):
 1. \<lbrakk>f a \<in> J; a \<in> A; f b \<in> J; b \<in> A\<rbrakk> \<Longrightarrow> f (addA a b) \<in> J
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a1 \<in> f \<^sup>\<inverse> A J; ?b1 \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> addA ?a1 ?b1 \<in> f \<^sup>\<inverse> A J

goal (2 subgoals):
 1. f \<^sup>\<inverse> A J \<subseteq> A
 2. zeroA \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
qed blast+
[PROOF STATE]
proof (state)
this:
submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
 3. ideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show "Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
[PROOF STEP]
by (smt (verit, ccfv_threshold) Group_Theory.monoid.intro IntD2 sma maxI.additive.associative maxI.additive.left_unit maxI.additive.right_unit submonoid_axioms_def)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA

goal (2 subgoals):
 1. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
 2. ideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show "Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f \<^sup>\<inverse> A J \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA u
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> f \<^sup>\<inverse> A J \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA u
[PROOF STEP]
assume "x \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (state)
this:
x \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. \<And>u. u \<in> f \<^sup>\<inverse> A J \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x"
[PROOF STATE]
proof (prove)
using this:
x \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> A; f x \<in> J\<rbrakk> \<Longrightarrow> monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x
[PROOF STEP]
by (smt (verit, best) JB.additive.sub.invertible JB.additive.submonoid_inverse_closed IntI \<open>Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA\<close> fiso.additive.invertible_commutes_with_inverse maxI.additive.inverse_equality maxI.additive.invertible maxI.additive.invertibleE monoid.invertible_def vimageI)
[PROOF STATE]
proof (state)
this:
monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (f \<^sup>\<inverse> A J) addA zeroA

goal (1 subgoal):
 1. ideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
show "ideal_axioms (f \<^sup>\<inverse> A J) A multA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal_axioms (f \<^sup>\<inverse> A J) A multA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA a b \<in> f \<^sup>\<inverse> A J
 2. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA b a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
fix a j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA a b \<in> f \<^sup>\<inverse> A J
 2. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA b a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
assume \<section>: "a \<in> A" "j \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (state)
this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA a b \<in> f \<^sup>\<inverse> A J
 2. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA b a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "multA a j \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
using JB.ideal(1) fiso.map_closed fiso.multiplicative.commutes_with_composition
[PROOF STATE]
proof (prove)
using this:
a \<in> A
j \<in> f \<^sup>\<inverse> A J
\<lbrakk>?a \<in> B; ?b \<in> J\<rbrakk> \<Longrightarrow> multB ?a ?b \<in> J
?a \<in> A \<Longrightarrow> f ?a \<in> B
\<lbrakk>?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> f (multA ?x ?y) = multB (f ?x) (f ?y)

goal (1 subgoal):
 1. multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multA a j \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> A; b \<in> f \<^sup>\<inverse> A J\<rbrakk> \<Longrightarrow> multA b a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
show "multA j a \<in> f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
using this:
multA a j \<in> f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. multA j a \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
by (metis Int_iff \<section> maxI.comm_mult)
[PROOF STATE]
proof (state)
this:
multA j a \<in> f \<^sup>\<inverse> A J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal_axioms (f \<^sup>\<inverse> A J) A multA

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
have "I = f \<^sup>\<inverse> A J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I = f \<^sup>\<inverse> A J
[PROOF STEP]
by (metis "\<section>" JB.additive.sub \<open>J \<noteq> B\<close> fim fiso.surjective image_subset_iff_subset_vimage
            le_inf_iff maxI.is_max maxI.psubset_ring psubsetE subsetI subset_antisym)
[PROOF STATE]
proof (state)
this:
I = f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> B addB multB zeroB oneB; \<aa> \<noteq> B; f ` I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f ` I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I = f \<^sup>\<inverse> A J
[PROOF STEP]
show "f ` I = J"
[PROOF STATE]
proof (prove)
using this:
I = f \<^sup>\<inverse> A J

goal (1 subgoal):
 1. f ` I = J
[PROOF STEP]
using JB.additive.sub fiso.surjective
[PROOF STATE]
proof (prove)
using this:
I = f \<^sup>\<inverse> A J
?a \<in> J \<Longrightarrow> ?a \<in> B
f ` A = B

goal (1 subgoal):
 1. f ` I = J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` I = J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max_ideal_axioms B (f ` I) addB multB zeroB oneB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max_ideal B (f ` I) addB multB zeroB oneB

goal:
No subgoals!
[PROOF STEP]
qed