[STATEMENT]
lemma preim_of_ideal_is_ideal:
  fixes f :: "'a\<Rightarrow>'b"
  assumes J: "ideal J B addB multB zeroB oneB"
    and "ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "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 -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA
[PROOF STEP]
interpret JB: ideal J B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal J B addB multB zeroB oneB
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
ideal J B addB multB zeroB oneB

goal (1 subgoal):
 1. ideal J B addB multB zeroB oneB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA
[PROOF STEP]
interpret f: ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ideal J B addB multB zeroB oneB
ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ring_homomorphism 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 \<^sup>\<inverse> A J) A addA multA zeroA oneA
[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]
using f.ring_preimage
[PROOF STATE]
proof (prove)
using this:
ring (f \<^sup>\<inverse> A B) addA multA zeroA oneA

goal (1 subgoal):
 1. ring (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA
[PROOF STEP]
show ?thesis
[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 "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]
by (auto simp add: submonoid_axioms_def f.additive.commutes_with_composition f.additive.commutes_with_unit)
[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]
then
[PROOF STATE]
proof (chain)
picking this:
submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA
[PROOF STEP]
show grp_fAJ: "Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA"
[PROOF STATE]
proof (prove)
using this:
submonoid_axioms (f \<^sup>\<inverse> A J) A addA zeroA

goal (1 subgoal):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A J) addA zeroA
[PROOF STEP]
by (auto simp: submonoid_axioms_def Group_Theory.monoid_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]
unfolding group_def
[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: "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]
have "f x \<in> J" "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> f \<^sup>\<inverse> A J

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

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:
f x \<in> J
x \<in> A
[PROOF STEP]
obtain v where "f v \<in> J \<and> v \<in> A \<and> addA x v = zeroA"
[PROOF STATE]
proof (prove)
using this:
f x \<in> J
x \<in> A

goal (1 subgoal):
 1. (\<And>v. f v \<in> J \<and> v \<in> A \<and> addA x v = zeroA \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis JB.additive.sub.invertible JB.additive.submonoid_inverse_closed f.additive.invertible_commutes_with_inverse
              f.source.additive.invertible f.source.additive.invertible_inverse_closed f.source.additive.invertible_right_inverse)
[PROOF STATE]
proof (state)
this:
f v \<in> J \<and> v \<in> A \<and> addA x v = zeroA

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:
f v \<in> J \<and> v \<in> A \<and> addA x v = zeroA
[PROOF STEP]
show "monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x"
[PROOF STATE]
proof (prove)
using this:
f v \<in> J \<and> v \<in> A \<and> addA x v = zeroA

goal (1 subgoal):
 1. monoid.invertible (f \<^sup>\<inverse> A J) addA zeroA x
[PROOF STEP]
by (metis Int_iff f.source.additive.commutative grp_fAJ monoid.invertibleI vimageI x)
[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 j a \<in> f \<^sup>\<inverse> A J" "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 j a \<in> f \<^sup>\<inverse> A J &&& multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
using JB.ideal f.map_closed f.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
\<lbrakk>?a \<in> B; ?b \<in> J\<rbrakk> \<Longrightarrow> multB ?b ?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 j a \<in> f \<^sup>\<inverse> A J &&& multA a j \<in> f \<^sup>\<inverse> A J
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
multA j a \<in> f \<^sup>\<inverse> A J
multA a j \<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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma preim_of_max_ideal_is_max:
  fixes f:: "'a \<Rightarrow> 'b"
  assumes J: "max_ideal B J addB multB zeroB oneB"
    and f: "ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "max_ideal A (f\<^sup>\<inverse> A J) addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_ideal A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
interpret maxJ: max_ideal B J addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal B J addB multB zeroB oneB
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
max_ideal B J addB multB zeroB oneB

goal (1 subgoal):
 1. max_ideal B J addB multB zeroB oneB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_ideal A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[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 A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
interpret fAJ: 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]
using maxJ.ideal_axioms fiso.ring_homomorphism_axioms
[PROOF STATE]
proof (prove)
using this:
ideal J B addB multB zeroB oneB
ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ideal (f \<^sup>\<inverse> A J) A addA multA zeroA oneA
[PROOF STEP]
by (blast intro: preim_of_ideal_is_ideal)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_ideal A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. comm_ring_axioms A multA
 2. max_ideal_axioms A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
show "comm_ring_axioms A multA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_ring_axioms A multA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> multA a b = multA b a
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> multA a b = multA b a
[PROOF STEP]
assume "a \<in> A" and "b \<in> A"
[PROOF STATE]
proof (state)
this:
a \<in> A
b \<in> A

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

goal (1 subgoal):
 1. multB (f a) (f b) = multB (f b) (f a)
[PROOF STEP]
using fiso.map_closed maxJ.comm_mult
[PROOF STATE]
proof (prove)
using this:
a \<in> A
b \<in> A
?a \<in> A \<Longrightarrow> f ?a \<in> B
\<lbrakk>?a \<in> B; ?b \<in> B\<rbrakk> \<Longrightarrow> multB ?a ?b = multB ?b ?a

goal (1 subgoal):
 1. multB (f a) (f b) = multB (f b) (f a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
multB (f a) (f b) = multB (f b) (f a)

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

goal (1 subgoal):
 1. multA a b = multA b a
[PROOF STEP]
by (metis bij_betw_iff_bijections \<open>a \<in> A\<close> \<open>b \<in> A\<close> fiso.bijective fiso.multiplicative.commutes_with_composition fiso.source.multiplicative.composition_closed)
[PROOF STATE]
proof (state)
this:
multA a b = multA b a

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

goal (1 subgoal):
 1. max_ideal_axioms A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
show "max_ideal_axioms A (f \<^sup>\<inverse> A J) addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_ideal_axioms A (f \<^sup>\<inverse> A J) addA multA zeroA oneA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<^sup>\<inverse> A J \<noteq> A
 2. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[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 fiso.surjective maxJ.additive.sub maxJ.neq_ring
[PROOF STATE]
proof (prove)
using this:
f ` A = B
?a \<in> J \<Longrightarrow> ?a \<in> B
J \<noteq> 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. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[PROOF STEP]
fix I
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[PROOF STEP]
assume "ideal I A addA multA zeroA oneA"
        and "I \<noteq> A" and "f \<^sup>\<inverse> A J \<subseteq> I"
[PROOF STATE]
proof (state)
this:
ideal I A addA multA zeroA oneA
I \<noteq> A
f \<^sup>\<inverse> A J \<subseteq> I

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ideal I A addA multA zeroA oneA
I \<noteq> A
f \<^sup>\<inverse> A J \<subseteq> I
[PROOF STEP]
interpret IA: ideal I A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
using this:
ideal I A addA multA zeroA oneA
I \<noteq> A
f \<^sup>\<inverse> A J \<subseteq> I

goal (1 subgoal):
 1. ideal I A addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[PROOF STEP]
have mon_fI: "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]
unfolding image_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>I. a = f x
\<exists>x\<in>I. b = f x

goal (1 subgoal):
 1. \<exists>x\<in>I. addB a b = f x
[PROOF STEP]
by (metis IA.additive.sub IA.additive.sub_composition_closed fiso.additive.commutes_with_composition)
[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 fiso.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 blast+
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f ` I) addB zeroB

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[PROOF STEP]
have ideal_fI: "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 (9 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
 4. \<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)
 5. \<And>a. a \<in> f ` I \<Longrightarrow> addB zeroB a = a
 6. \<And>a. a \<in> f ` I \<Longrightarrow> addB a zeroB = a
 7. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 8. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 9. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<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 (8 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
 6. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 7. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 8. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
show "zeroB \<in> f ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroB \<in> f ` I
[PROOF STEP]
using fiso.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 (7 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<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
 5. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 7. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<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
 5. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 7. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<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
 5. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 7. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
assume "a \<in> f ` I" and "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
a \<in> f ` I
b \<in> f ` I

goal (7 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> f ` I; b \<in> f ` I\<rbrakk> \<Longrightarrow> addB a b \<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
 5. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 7. \<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> 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]
unfolding image_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>I. a = f x
\<exists>x\<in>I. b = f x

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

goal (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
assume "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
b \<in> f ` I

goal (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<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> f ` I
[PROOF STEP]
obtain i where i: "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 (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<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 = 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]
by (meson IA.additive.sub.invertible IA.additive.sub.invertibleE)
[PROOF STATE]
proof (state)
this:
addA i j = zeroA
j \<in> I

goal (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<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:
addA i j = zeroA
j \<in> I
[PROOF STEP]
have "addB b (f j) = zeroB"
[PROOF STATE]
proof (prove)
using this:
addA i j = zeroA
j \<in> I

goal (1 subgoal):
 1. addB b (f j) = zeroB
[PROOF STEP]
by (metis IA.additive.sub i fiso.additive.commutes_with_composition fiso.additive.commutes_with_unit)
[PROOF STATE]
proof (state)
this:
addB b (f j) = zeroB

goal (6 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
 4. \<And>u. u \<in> f ` I \<Longrightarrow> monoid.invertible (f ` I) addB zeroB u
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 6. \<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:
addB b (f j) = zeroB
[PROOF STEP]
show "monoid.invertible (f ` I) addB zeroB b"
[PROOF STATE]
proof (prove)
using this:
addB b (f j) = zeroB

goal (1 subgoal):
 1. monoid.invertible (f ` I) addB zeroB b
[PROOF STEP]
by (metis IA.additive.sub i \<open>j \<in> I\<close> fiso.map_closed imageI maxJ.additive.commutative mon_fI monoid.invertibleI)
[PROOF STATE]
proof (state)
this:
monoid.invertible (f ` I) addB zeroB b

goal (5 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
 4. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 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
 4. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (5 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
 4. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
assume "a \<in> B" and "b \<in> f ` I"
[PROOF STATE]
proof (state)
this:
a \<in> B
b \<in> f ` I

goal (5 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
 4. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB a b \<in> f ` I
 5. \<And>a b. \<lbrakk>a \<in> B; b \<in> f ` I\<rbrakk> \<Longrightarrow> multB b a \<in> f ` I
[PROOF STEP]
with IA.ideal
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a \<in> A; ?b \<in> I\<rbrakk> \<Longrightarrow> multA ?a ?b \<in> I
\<lbrakk>?a \<in> A; ?b \<in> I\<rbrakk> \<Longrightarrow> multA ?b ?a \<in> I
a \<in> B
b \<in> f ` I
[PROOF STEP]
show "multB a b \<in> f ` I" "multB b a \<in> f ` I"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> A; ?b \<in> I\<rbrakk> \<Longrightarrow> multA ?a ?b \<in> I
\<lbrakk>?a \<in> A; ?b \<in> I\<rbrakk> \<Longrightarrow> multA ?b ?a \<in> I
a \<in> B
b \<in> f ` I

goal (1 subgoal):
 1. multB a b \<in> f ` I &&& multB b a \<in> f ` I
[PROOF STEP]
by (smt (verit, best) IA.additive.sub fiso.multiplicative.commutes_with_composition fiso.surjective image_iff)+
[PROOF STATE]
proof (state)
this:
multB a b \<in> f ` I
multB b a \<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 blast+
[PROOF STATE]
proof (state)
this:
ideal (f ` I) B addB multB zeroB oneB

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>ideal \<aa> A addA multA zeroA oneA; \<aa> \<noteq> A; f \<^sup>\<inverse> A J \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A J = \<aa>
[PROOF STEP]
have "J = f ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J = f ` I
[PROOF STEP]
proof (rule maxJ.is_max [OF ideal_fI])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` I \<noteq> B
 2. J \<subseteq> f ` I
[PROOF STEP]
show "f ` I \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` I \<noteq> B
[PROOF STEP]
by (metis IA.additive.sub \<open>I \<noteq> A\<close> fiso.injective fiso.surjective inj_on_image_eq_iff subsetI)
[PROOF STATE]
proof (state)
this:
f ` I \<noteq> B

goal (1 subgoal):
 1. J \<subseteq> f ` I
[PROOF STEP]
show "J \<subseteq> f ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<subseteq> f ` I
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<subseteq> {y. \<exists>x\<in>I. y = f x}
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> J \<Longrightarrow> \<exists>xa\<in>I. x = f xa
[PROOF STEP]
by (smt (verit, ccfv_threshold) Int_iff \<open>f \<^sup>\<inverse> A J \<subseteq> I\<close> fiso.surjective imageE maxJ.additive.sub subset_eq vimageI)
[PROOF STATE]
proof (state)
this:
J \<subseteq> f ` I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
J = f ` I

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

goal (1 subgoal):
 1. f \<^sup>\<inverse> A J = I
[PROOF STEP]
using \<open>f \<^sup>\<inverse> A J \<subseteq> I\<close>
[PROOF STATE]
proof (prove)
using this:
J = f ` I
f \<^sup>\<inverse> A J \<subseteq> I

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma preim_of_lideal_is_lideal:
  assumes "lideal I B addB multB zeroB oneB"
    and "ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
interpret A: ring A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring A addA multA zeroA oneA
[PROOF STEP]
by (meson assms ring_homomorphism_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[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 ring_homomorphism_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
interpret f: ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lideal I B addB multB zeroB oneB
ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB

goal (1 subgoal):
 1. ring_homomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[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]
using f.ring_preimage
[PROOF STATE]
proof (prove)
using this:
ring (f \<^sup>\<inverse> A B) addA multA zeroA oneA

goal (1 subgoal):
 1. ring (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
interpret IB: lideal I B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal I B addB multB zeroB oneB
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. submonoid_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA zeroA
 2. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
 3. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 4. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
show "submonoid_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA zeroA
[PROOF STEP]
by (auto simp add: submonoid_axioms_def f.additive.commutes_with_composition f.additive.commutes_with_unit)
[PROOF STATE]
proof (state)
this:
submonoid_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA zeroA

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 3. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
have "(A.additive.inverse u) \<in> f \<^sup>\<inverse> A I" if "f u \<in> I" and "u \<in> A" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.additive.inverse u \<in> f \<^sup>\<inverse> A I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A.additive.inverse u \<in> f \<^sup>\<inverse> A I
[PROOF STEP]
have "f (A.additive.inverse u) = B.additive.inverse (f u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (A.additive.inverse u) = B.additive.inverse (f u)
[PROOF STEP]
using A.additive.invertible f.additive.invertible_commutes_with_inverse that
[PROOF STATE]
proof (prove)
using this:
?u \<in> A \<Longrightarrow> A.additive.invertible ?u
\<lbrakk>A.additive.invertible ?a; ?a \<in> A\<rbrakk> \<Longrightarrow> f (A.additive.inverse ?a) = B.additive.inverse (f ?a)
f u \<in> I
u \<in> A

goal (1 subgoal):
 1. f (A.additive.inverse u) = B.additive.inverse (f u)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
f (A.additive.inverse u) = B.additive.inverse (f u)

goal (1 subgoal):
 1. A.additive.inverse u \<in> f \<^sup>\<inverse> A I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (A.additive.inverse u) = B.additive.inverse (f u)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (A.additive.inverse u) = B.additive.inverse (f u)

goal (1 subgoal):
 1. A.additive.inverse u \<in> f \<^sup>\<inverse> A I
[PROOF STEP]
using A.additive.invertible_inverse_closed that
[PROOF STATE]
proof (prove)
using this:
f (A.additive.inverse u) = B.additive.inverse (f u)
\<lbrakk>A.additive.invertible ?u; ?u \<in> A\<rbrakk> \<Longrightarrow> A.additive.inverse ?u \<in> A
f u \<in> I
u \<in> A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>f ?u1 \<in> I; ?u1 \<in> A\<rbrakk> \<Longrightarrow> A.additive.inverse ?u1 \<in> f \<^sup>\<inverse> A I

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 3. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>f ?u1 \<in> I; ?u1 \<in> A\<rbrakk> \<Longrightarrow> A.additive.inverse ?u1 \<in> f \<^sup>\<inverse> A I

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 3. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
have "addA (A.additive.inverse u) u = zeroA"  "addA u (A.additive.inverse u) = zeroA" if "u \<in> A" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addA (A.additive.inverse u) u = zeroA &&& A.subtraction u u = zeroA
[PROOF STEP]
by (auto simp add: that)
[PROOF STATE]
proof (state)
this:
?u1 \<in> A \<Longrightarrow> addA (A.additive.inverse ?u1) ?u1 = zeroA
?u1 \<in> A \<Longrightarrow> A.subtraction ?u1 ?u1 = zeroA

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 3. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?u1 \<in> A \<Longrightarrow> addA (A.additive.inverse ?u1) ?u1 = zeroA
?u1 \<in> A \<Longrightarrow> A.subtraction ?u1 ?u1 = zeroA

goal (3 subgoals):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
 2. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 3. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
show "Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
[PROOF STEP]
by (auto simp: monoid_def f.additive.commutes_with_composition f.additive.commutes_with_unit)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA

goal (2 subgoals):
 1. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
 2. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>f ?u1 \<in> I; ?u1 \<in> A\<rbrakk> \<Longrightarrow> A.additive.inverse ?u1 \<in> f \<^sup>\<inverse> A I
?u1 \<in> A \<Longrightarrow> addA (A.additive.inverse ?u1) ?u1 = zeroA
?u1 \<in> A \<Longrightarrow> A.subtraction ?u1 ?u1 = zeroA
Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA
[PROOF STEP]
show "Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f ?u1 \<in> I; ?u1 \<in> A\<rbrakk> \<Longrightarrow> A.additive.inverse ?u1 \<in> f \<^sup>\<inverse> A I
?u1 \<in> A \<Longrightarrow> addA (A.additive.inverse ?u1) ?u1 = zeroA
?u1 \<in> A \<Longrightarrow> A.subtraction ?u1 ?u1 = zeroA
Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA

goal (1 subgoal):
 1. Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA
[PROOF STEP]
unfolding group_axioms_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f ?u1 \<in> I; ?u1 \<in> A\<rbrakk> \<Longrightarrow> A.additive.inverse ?u1 \<in> f \<^sup>\<inverse> A I
?u1 \<in> A \<Longrightarrow> addA (A.additive.inverse ?u1) ?u1 = zeroA
?u1 \<in> A \<Longrightarrow> A.subtraction ?u1 ?u1 = zeroA
Group_Theory.monoid (f \<^sup>\<inverse> A I) addA zeroA

goal (1 subgoal):
 1. \<forall>u. u \<in> f \<^sup>\<inverse> A I \<longrightarrow> monoid.invertible (f \<^sup>\<inverse> A I) addA zeroA u
[PROOF STEP]
by (metis IntE monoid.invertibleI vimage_eq)
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms (f \<^sup>\<inverse> A I) addA zeroA

goal (1 subgoal):
 1. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
show "lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA
[PROOF STEP]
unfolding lideal_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r a. r \<in> f \<^sup>\<inverse> A B \<longrightarrow> a \<in> f \<^sup>\<inverse> A I \<longrightarrow> multA r a \<in> f \<^sup>\<inverse> A I
[PROOF STEP]
using IB.lideal f.map_closed f.multiplicative.commutes_with_composition
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> B; ?a \<in> I\<rbrakk> \<Longrightarrow> multB ?r ?a \<in> I
?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. \<forall>r a. r \<in> f \<^sup>\<inverse> A B \<longrightarrow> a \<in> f \<^sup>\<inverse> A I \<longrightarrow> multA r a \<in> f \<^sup>\<inverse> A I
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) multA

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma preim_of_max_lideal_is_max:
  assumes "max_lideal I B addB multB zeroB oneB"
      and "ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "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]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[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]
using assms
[PROOF STATE]
proof (prove)
using this:
max_lideal I B addB multB zeroB oneB
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 blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
interpret MI: max_lideal I B addB multB zeroB oneB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal I B addB multB zeroB oneB
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
interpret pre: lideal "f \<^sup>\<inverse> A I" "f \<^sup>\<inverse> A B" addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by (meson preim_of_lideal_is_lideal MI.lideal_axioms f.ring_homomorphism_axioms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
show ?thesis
[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]
proof intro_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
show "max_lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal_axioms (f \<^sup>\<inverse> A I) (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<^sup>\<inverse> A I \<noteq> f \<^sup>\<inverse> A B
 2. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
show "f \<^sup>\<inverse> A I \<noteq> f \<^sup>\<inverse> A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<^sup>\<inverse> A I \<noteq> f \<^sup>\<inverse> A B
[PROOF STEP]
using MI.neq_ring MI.subset f.surjective
[PROOF STATE]
proof (prove)
using this:
I \<noteq> B
I \<subseteq> B
f ` A = B

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

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
fix \<aa>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
assume "lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA"
        and "\<aa> \<noteq> f \<^sup>\<inverse> A B"
        and "f \<^sup>\<inverse> A I \<subseteq> \<aa>"
[PROOF STATE]
proof (state)
this:
lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA
\<aa> \<noteq> f \<^sup>\<inverse> A B
f \<^sup>\<inverse> A I \<subseteq> \<aa>

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA
\<aa> \<noteq> f \<^sup>\<inverse> A B
f \<^sup>\<inverse> A I \<subseteq> \<aa>
[PROOF STEP]
interpret lideal \<aa> "f \<^sup>\<inverse> A B" addA multA zeroA oneA
[PROOF STATE]
proof (prove)
using this:
lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA
\<aa> \<noteq> f \<^sup>\<inverse> A B
f \<^sup>\<inverse> A I \<subseteq> \<aa>

goal (1 subgoal):
 1. lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
have "f ` \<aa> \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` \<aa> \<noteq> B
[PROOF STEP]
by (metis Int_absorb1 \<open>\<aa> \<noteq> f \<^sup>\<inverse> A B\<close> f.injective f.surjective image_subset_iff_subset_vimage inj_on_image_eq_iff subset subset_iff)
[PROOF STATE]
proof (state)
this:
f ` \<aa> \<noteq> B

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ` \<aa> \<noteq> B

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
have "I \<subseteq> f ` \<aa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> f ` \<aa>
[PROOF STEP]
by (smt (verit, ccfv_threshold) Int_iff MI.subset \<open>f \<^sup>\<inverse> A I \<subseteq> \<aa>\<close> f.surjective image_iff subset_iff vimageI)
[PROOF STATE]
proof (state)
this:
I \<subseteq> f ` \<aa>

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
I \<subseteq> f ` \<aa>

goal (1 subgoal):
 1. \<And>\<aa>. \<lbrakk>lideal \<aa> (f \<^sup>\<inverse> A B) addA multA zeroA oneA; \<aa> \<noteq> f \<^sup>\<inverse> A B; f \<^sup>\<inverse> A I \<subseteq> \<aa>\<rbrakk> \<Longrightarrow> f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
have "lideal (f ` \<aa>) B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lideal (f ` \<aa>) B addB multB zeroB oneB
[PROOF STEP]
by (metis f.multiplicative.image.subset f.ring_epimorphism_axioms im_of_lideal_is_lideal image_subset_iff_subset_vimage inf.orderE inf_sup_aci(1) lideal_axioms)
[PROOF STATE]
proof (state)
this:
lideal (f ` \<aa>) B addB multB zeroB oneB

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

goal (1 subgoal):
 1. f \<^sup>\<inverse> A I = \<aa>
[PROOF STEP]
by (metis MI.is_max \<open>f \<^sup>\<inverse> A I \<subseteq> \<aa>\<close> image_subset_iff_subset_vimage le_inf_iff subset subset_antisym)
[PROOF STATE]
proof (state)
this:
f \<^sup>\<inverse> A I = \<aa>

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isomorphic_to_local_is_local:
  assumes lring: "local_ring B addB multB zeroB oneB"
    and iso: "ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB"
  shows "local_ring A addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring A addA multA zeroA oneA
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. Group_Theory.monoid A addA zeroA
 2. Group_Theory.group_axioms A addA zeroA
 3. commutative_monoid_axioms A addA
 4. Group_Theory.monoid A multA oneA
 5. ring_axioms A addA multA
 6. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
interpret ring A addA multA zeroA oneA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring A addA multA zeroA oneA
[PROOF STEP]
by (meson iso ring_homomorphism.axioms(2) ring_isomorphism.axioms(1))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. Group_Theory.monoid A addA zeroA
 2. Group_Theory.group_axioms A addA zeroA
 3. commutative_monoid_axioms A addA
 4. Group_Theory.monoid A multA oneA
 5. ring_axioms A addA multA
 6. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
show "Group_Theory.monoid A addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid A addA zeroA
[PROOF STEP]
by (simp add: additive.monoid_axioms)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid A addA zeroA

goal (5 subgoals):
 1. Group_Theory.group_axioms A addA zeroA
 2. commutative_monoid_axioms A addA
 3. Group_Theory.monoid A multA oneA
 4. ring_axioms A addA multA
 5. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
show "Group_Theory.group_axioms A addA zeroA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group_axioms A addA zeroA
[PROOF STEP]
by (meson Group_Theory.group_def additive.group_axioms)
[PROOF STATE]
proof (state)
this:
Group_Theory.group_axioms A addA zeroA

goal (4 subgoals):
 1. commutative_monoid_axioms A addA
 2. Group_Theory.monoid A multA oneA
 3. ring_axioms A addA multA
 4. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
show "commutative_monoid_axioms A addA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. commutative_monoid_axioms A addA
[PROOF STEP]
by (simp add: additive.commutative commutative_monoid_axioms_def)
[PROOF STATE]
proof (state)
this:
commutative_monoid_axioms A addA

goal (3 subgoals):
 1. Group_Theory.monoid A multA oneA
 2. ring_axioms A addA multA
 3. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
show "Group_Theory.monoid A multA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid A multA oneA
[PROOF STEP]
by (simp add: multiplicative.monoid_axioms)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid A multA oneA

goal (2 subgoals):
 1. ring_axioms A addA multA
 2. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
show "ring_axioms A addA multA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_axioms A addA multA
[PROOF STEP]
by (meson local.ring_axioms ring.axioms(3))
[PROOF STATE]
proof (state)
this:
ring_axioms A addA multA

goal (1 subgoal):
 1. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
have hom: "monoid_homomorphism f A multA oneA B multB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism f A multA oneA B multB oneB
[PROOF STEP]
by (meson iso ring_homomorphism_def ring_isomorphism.axioms(1))
[PROOF STATE]
proof (state)
this:
monoid_homomorphism f A multA oneA B multB oneB

goal (1 subgoal):
 1. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
have "bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using iso map.graph
[PROOF STATE]
proof (prove)
using this:
ring_isomorphism f A addA multA zeroA oneA B addB multB zeroB oneB
Set_Theory.map ?\<alpha> ?S ?T \<Longrightarrow> ?\<alpha> \<in> ?S \<rightarrow>\<^sub>E ?T

goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
by (simp add: bijective.bijective ring_isomorphism_def bijective_map_def)
[PROOF STATE]
proof (state)
this:
bij_betw f A B

goal (1 subgoal):
 1. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
show "local_ring_axioms A addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring_axioms A addA multA zeroA oneA
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I A addA multA zeroA oneA; max_lideal J A addA multA zeroA oneA\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA
[PROOF STEP]
fix I J
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I A addA multA zeroA oneA; max_lideal J A addA multA zeroA oneA\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA
[PROOF STEP]
assume I: "max_lideal I A addA multA zeroA oneA" and J: "max_lideal J A addA multA zeroA oneA"
[PROOF STATE]
proof (state)
this:
max_lideal I A addA multA zeroA oneA
max_lideal J A addA multA zeroA oneA

goal (2 subgoals):
 1. \<And>I J. \<lbrakk>max_lideal I A addA multA zeroA oneA; max_lideal J A addA multA zeroA oneA\<rbrakk> \<Longrightarrow> I = J
 2. \<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA
[PROOF STEP]
show "I = J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I = J
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I = J
[PROOF STEP]
have "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]
by (meson I im_of_max_lideal_is_max iso)
[PROOF STATE]
proof (state)
this:
max_lideal (f ` I) B addB multB zeroB oneB

goal (1 subgoal):
 1. I = J
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
max_lideal (f ` I) B addB multB zeroB oneB

goal (1 subgoal):
 1. I = J
[PROOF STEP]
have "max_lideal (f ` J) B addB multB zeroB oneB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_lideal (f ` J) B addB multB zeroB oneB
[PROOF STEP]
by (meson J im_of_max_lideal_is_max iso)
[PROOF STATE]
proof (state)
this:
max_lideal (f ` J) B addB multB zeroB oneB

goal (1 subgoal):
 1. I = J
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
max_lideal (f ` I) B addB multB zeroB oneB
max_lideal (f ` J) B addB multB zeroB oneB
[PROOF STEP]
have "f ` I = f ` J"
[PROOF STATE]
proof (prove)
using this:
max_lideal (f ` I) B addB multB zeroB oneB
max_lideal (f ` J) B addB multB zeroB oneB

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

goal (1 subgoal):
 1. I = J
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` I = f ` J

goal (1 subgoal):
 1. I = J
[PROOF STEP]
using bij_betw_imp_inj_on [OF \<open>bij_betw f A B\<close>]
[PROOF STATE]
proof (prove)
using this:
f ` I = f ` J
inj_on f A

goal (1 subgoal):
 1. I = J
[PROOF STEP]
by (meson I J inj_on_image_eq_iff lideal.subset max_lideal.axioms(1))
[PROOF STATE]
proof (state)
this:
I = J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
I = J

goal (1 subgoal):
 1. \<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA
[PROOF STEP]
show "\<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA
[PROOF STEP]
by (meson im_of_max_lideal_is_max iso local_ring.has_max_lideal lring ring_isomorphism.inverse_ring_isomorphism)
[PROOF STATE]
proof (state)
this:
\<exists>\<ww>. max_lideal \<ww> A addA multA zeroA oneA

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local_ring_axioms A addA multA zeroA oneA

goal:
No subgoals!
[PROOF STEP]
qed