diff --git a/IsarMathLib/Group_ZF_5.thy b/IsarMathLib/Group_ZF_5.thy
index 8214b66..9aa9c5f 100644
--- a/IsarMathLib/Group_ZF_5.thy
+++ b/IsarMathLib/Group_ZF_5.thy
@@ -37,20 +37,30 @@ subsection\<open>Homomorphisms\<close>
 
 text\<open>A homomorphism is a function between groups that preserves the group operations.\<close>
 
-text\<open>Suppose we have two groups $G$ and $H$ with corresponding binary operations 
-  $P:G\times G \rightarrow G$ and $F:H\times H \rightarrow H$. Then $f$ is a homomorphism
-  if for all $g_1,g_2\in G$ we have $f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle$. \<close> 
+text\<open>In general we may have a homomorphism not only between groups, but also between various 
+  algebraic structures with one operation like magmas, semigroups, quasigroups, loops and monoids. 
+  In all cases the homomorphism is defined by using the morphism property. In the 
+  multiplicative notation we we will write that $f$ has a morphism property if 
+  $f(x\cdot_G y) = f(x)\cdot_H f(y)$ for all $x,y\in G$. Below we write this definition 
+  in raw set theory notation and use the expression \<open>IsMorphism\<close> instead of the possible, but longer
+  \<open>HasMorphismProperty\<close>. \<close>
+
+definition 
+  "IsMorphism(G,P,F,f) \<equiv> \<forall>g\<^sub>1\<in>G. \<forall>g\<^sub>2\<in>G. f`(P`\<langle>g\<^sub>1,g\<^sub>2\<rangle>) = F`\<langle>f`(g\<^sub>1),f`(g\<^sub>2)\<rangle>"
+
+text\<open>A function $f:G\rightarrow H$ between algebraic structures 
+  $(G,\cdot_G)$ and $(H,\cdot_H)$ with one operation (each) is a homomorphism is it has the morphism
+  property. \<close> 
 
 definition
-  Homomor where  "IsAgroup(G,P) \<Longrightarrow> IsAgroup(H,F) \<Longrightarrow> 
-    Homomor(f,G,P,H,F) \<equiv> \<forall>g\<^sub>1\<in>G. \<forall>g\<^sub>2\<in>G. f`(P`\<langle>g\<^sub>1,g\<^sub>2\<rangle>)=F`\<langle>f`(g\<^sub>1),f`(g\<^sub>2)\<rangle>"
+  "Homomor(f,G,P,H,F) \<equiv> f:G\<rightarrow>H \<and> IsMorphism(G,P,F,f)"
 
 text\<open>Now a lemma about the definition:\<close>
 
 lemma homomor_eq:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "g\<^sub>1\<in>G" "g\<^sub>2\<in>G"
-  shows "f`(P`\<langle>g\<^sub>1,g\<^sub>2\<rangle>)=F`\<langle>f`(g\<^sub>1),f`(g\<^sub>2)\<rangle>"
-  using assms Homomor_def by auto
+  assumes "Homomor(f,G,P,H,F)" "g\<^sub>1\<in>G" "g\<^sub>2\<in>G"
+  shows "f`(P`\<langle>g\<^sub>1,g\<^sub>2\<rangle>) = F`\<langle>f`(g\<^sub>1),f`(g\<^sub>2)\<rangle>"
+  using assms unfolding Homomor_def IsMorphism_def by auto
 
 text\<open>An endomorphism is a homomorphism from a group to the same group. In case
 the group is abelian, it has a nice structure.\<close>
@@ -62,7 +72,7 @@ text\<open>The defining property of an endomorphism written in notation used in
 
 lemma (in group0) endomor_eq: assumes "f \<in> End(G,P)" "g\<^sub>1\<in>G" "g\<^sub>2\<in>G"
   shows "f`(g\<^sub>1\<cdot>g\<^sub>2) = f`(g\<^sub>1)\<cdot>f`(g\<^sub>2)"
-  using groupAssum assms homomor_eq unfolding End_def by simp
+  using assms homomor_eq unfolding End_def by auto
 
 text\<open>A function that maps a group $G$ into itself and satisfies 
   $f(g_1\cdot g2) = f(g_1)\cdot f(g_2)$ is an endomorphism.\<close>
@@ -70,7 +80,7 @@ text\<open>A function that maps a group $G$ into itself and satisfies
 lemma (in group0) eq_endomor: 
   assumes "f:G\<rightarrow>G" and "\<forall>g\<^sub>1\<in>G. \<forall>g\<^sub>2\<in>G. f`(g\<^sub>1\<cdot>g\<^sub>2)=f`(g\<^sub>1)\<cdot>f`(g\<^sub>2)"
   shows "f \<in> End(G,P)"
-  using groupAssum assms Homomor_def unfolding End_def by auto
+  using assms  unfolding End_def Homomor_def IsMorphism_def by simp
 
 text\<open>The set of endomorphisms forms a submonoid of the monoid of function
 from a set to that set under composition.\<close>
@@ -149,7 +159,7 @@ lemma (in abelian_group) end_inverse_group:
   shows "GroupInv(G,P) \<in> End(G,P)"
   using inverse_in_group group_inv_of_two isAbelian IsCommutative_def 
     group0_2_T2 groupAssum Homomor_def 
-  unfolding End_def by simp
+  unfolding End_def IsMorphism_def by simp
 
 text\<open>The set of homomorphisms of an abelian group is an abelian subgroup of
   the group of functions from a set to a group, under pointwise multiplication.\<close>
@@ -294,17 +304,19 @@ text\<open>Now we will prove that any homomorphism $f:G\to H$ defines a bijectiv
 text\<open>A group homomorphism sends the neutral element to the neutral element.\<close>
 
 lemma image_neutral:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
   shows "f`(TheNeutralElement(G,P)) = TheNeutralElement(H,F)"
 proof -
   let ?e\<^sub>G = "TheNeutralElement(G,P)"
   let ?e\<^sub>H = "TheNeutralElement(H,F)"
+  from assms(3) have ff: "f:G\<rightarrow>H"
+    unfolding Homomor_def by simp
   have g: "?e\<^sub>G = P`\<langle>?e\<^sub>G,?e\<^sub>G\<rangle>" "?e\<^sub>G \<in> G"
     using assms(1) group0.group0_2_L2 unfolding group0_def by simp_all
   with assms have "f`(?e\<^sub>G) = F`\<langle>f`(?e\<^sub>G),f`(?e\<^sub>G)\<rangle>"
-    using Homomor_def by force 
+    unfolding Homomor_def IsMorphism_def by force
   moreover
-  from assms(4) g(2) have h: "f`(?e\<^sub>G) \<in> H" using apply_type 
+  from ff g(2) have h: "f`(?e\<^sub>G) \<in> H" using apply_type 
     by simp
   with assms(2) have "f`(?e\<^sub>G) = F`\<langle>f`(?e\<^sub>G),?e\<^sub>H\<rangle>"
     using group0.group0_2_L2 unfolding group0_def by simp 
@@ -324,44 +336,47 @@ qed
 text\<open>If $f:G\rightarrow H$ is a homomorphism, then it commutes with the inverse \<close>
 
 lemma image_inv:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H" "g\<in>G"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "g\<in>G"
   shows "f`(GroupInv(G,P)`(g)) = GroupInv(H,F)`(f`(g))"
-proof-
-  from assms(4,5) have im: "f`(g)\<in>H" using apply_type by simp
-  from assms(1,5) have inv: "GroupInv(G,P)`(g)\<in>G" 
+proof -
+  from assms(3) have ff: "f:G\<rightarrow>H"
+    unfolding Homomor_def by simp
+  with assms(4) have im: "f`(g)\<in>H" using apply_type by simp
+  from assms(1,4) have inv: "GroupInv(G,P)`(g)\<in>G" 
     using group0.inverse_in_group unfolding group0_def by simp
-  with assms(4) have inv2: "f`(GroupInv(G,P)`g)\<in>H" using apply_type by simp
-  from assms(1,5) have 
+  with ff have inv2: "f`(GroupInv(G,P)`g)\<in>H" using apply_type by simp
+  from assms(1,4) have 
     "f`(TheNeutralElement(G,P)) = f`(P`\<langle>g,GroupInv(G,P)`(g)\<rangle>)" 
     using group0.group0_2_L6 unfolding group0_def by simp
-  also from assms(1,2,3,5) inv have "\<dots> = F`\<langle>f`(g),f`(GroupInv(G,P)`(g))\<rangle>" 
-    using Homomor_def by simp
+  also from assms inv have "\<dots> = F`\<langle>f`(g),f`(GroupInv(G,P)`(g))\<rangle>" 
+    unfolding Homomor_def IsMorphism_def by simp
   finally have "f`(TheNeutralElement(G,P)) = F`\<langle>f`(g),f`(GroupInv(G,P)`(g))\<rangle>"
     by simp
-  with assms(1-4) im inv2 show ?thesis 
+  with assms im inv2 show ?thesis 
     using group0.group0_2_L9 image_neutral unfolding group0_def by simp
 qed
 
 text\<open>The preimage of a subgroup is a subgroup\<close>
 
 theorem preimage_sub:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
           "IsAsubgroup(K,F)"
   shows "IsAsubgroup(f-``(K),P)"
 proof -
+  from assms(3) have ff: "f:G\<rightarrow>H"
+    unfolding Homomor_def by simp
   from assms(2) have Hgr: "group0(H,F)" unfolding group0_def by simp
   from assms(1) have Ggr: "group0(G,P)" unfolding group0_def by simp
   moreover 
-  from assms Ggr Hgr have "TheNeutralElement(G,P) \<in> f-``(K)"
+  from assms ff Ggr Hgr have "TheNeutralElement(G,P) \<in> f-``(K)"
     using image_neutral group0.group0_3_L5 func1_1_L15 group0.group0_2_L2 
     by simp
   hence "f-``(K)\<noteq>0" by blast
-  moreover from assms(4) have "f-``(K) \<subseteq> G" using func1_1_L3 by simp
-  moreover from assms Ggr Hgr have "f-``(K) {is closed under} P"
-    using func1_1_L15 group0.group0_3_L6 Homomor_def 
-        group0.group_op_closed func1_1_L15
-    unfolding IsOpClosed_def by simp
-  moreover from assms Ggr Hgr have 
+  moreover from ff have "f-``(K) \<subseteq> G" using func1_1_L3 by simp
+  moreover from assms ff Ggr Hgr have "f-``(K) {is closed under} P"
+    using func1_1_L15 group0.group0_3_L6 group0.group_op_closed func1_1_L15
+    unfolding IsOpClosed_def Homomor_def IsMorphism_def by simp
+  moreover from assms ff Ggr Hgr have 
     "\<forall>x\<in>f-``(K). GroupInv(G, P)`(x) \<in> f-``(K)"
     using group0.group0_3_T3A image_inv func1_1_L15 
         group0.inverse_in_group by simp
@@ -371,13 +386,15 @@ qed
 text\<open>The preimage of a normal subgroup is normal\<close>
 
 theorem preimage_normal_subgroup:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
           "IsAnormalSubgroup(H,F,K)"
         shows "IsAnormalSubgroup(G,P,f-``(K))"
 proof -
+  from assms(3) have ff: "f:G\<rightarrow>H"
+    unfolding Homomor_def by simp
   from assms(2) have Hgr: "group0(H,F)" unfolding group0_def by simp
-  with assms(5) have "K\<subseteq>H" using group0.group0_3_L2 
-    unfolding IsAnormalSubgroup_def  by simp
+  with assms(4) have "K\<subseteq>H" using group0.group0_3_L2 
+    unfolding IsAnormalSubgroup_def by simp
   from assms(1) have Ggr: "group0(G,P)" unfolding group0_def by simp
   moreover from assms have "IsAsubgroup(f-``(K),P)" 
     using preimage_sub unfolding IsAnormalSubgroup_def by simp
@@ -388,14 +405,14 @@ proof -
         k: "h = P`\<langle>g,P`\<langle>k,GroupInv(G, P)`(g)\<rangle>\<rangle>" "k \<in> f-``(K)" 
         by auto
       from k(1) have "f`(h) = f`(P`\<langle>g,P`\<langle>k, GroupInv(G, P)`(g)\<rangle>\<rangle>)" by simp
-      moreover from assms(4) k(2) have "k\<in>G" using vimage_iff 
+      moreover from ff k(2) have "k\<in>G" using vimage_iff 
         unfolding Pi_def by blast
       ultimately have f: "f`(h) = F`\<langle>f`(g),F`\<langle>f`(k),GroupInv(H,F)`(f`(g))\<rangle>\<rangle>"
         using assms(1-4) Ggr gG group0.group_op_closed 
           group0.inverse_in_group image_inv homomor_eq by simp
-      from assms(1,4) Ggr \<open>g\<in>G\<close> k have "h\<in>G" using group0.group_op_closed
+      from assms(1) ff Ggr \<open>g\<in>G\<close> k have "h\<in>G" using group0.group_op_closed
         group0.inverse_in_group func1_1_L15 by simp
-      from assms(4,5) k(2) \<open>g\<in>G\<close> have "f`(k)\<in>K" "f`(g)\<in>H" and 
+      from assms(4) ff k(2) \<open>g\<in>G\<close> have "f`(k)\<in>K" "f`(g)\<in>H" and 
         "F`\<langle>F`\<langle>f`(g),f`(k)\<rangle>,GroupInv(H,F)`(f`(g))\<rangle> \<in> K"
         using func1_1_L15 apply_type unfolding IsAnormalSubgroup_def 
         by auto
@@ -403,7 +420,7 @@ proof -
         "f`(h) = F`\<langle>F`\<langle>f`(g),f`(k)\<rangle>,GroupInv(H,F)`(f`(g))\<rangle>"
         using group0.group_oper_assoc group0.inverse_in_group by auto
       ultimately have "f`(h) \<in> K" by simp
-      with assms(4) \<open>h\<in>G\<close> have "h \<in> f-``(K)" using func1_1_L15 by simp
+      with ff \<open>h\<in>G\<close> have "h \<in> f-``(K)" using func1_1_L15 by simp
     } hence "{P`\<langle>g,P`\<langle>h,GroupInv(G,P)`(g)\<rangle>\<rangle>. h\<in>f-``(K)} \<subseteq> f-``(K)" 
       by blast
   } hence "\<forall>g\<in>G. {P`\<langle>g, P`\<langle>h, GroupInv(G, P)`(g)\<rangle>\<rangle>. h\<in>f-``(K)} \<subseteq> f-``(K)" 
@@ -414,7 +431,7 @@ qed
 text\<open>The kernel of an homomorphism is a normal subgroup.\<close>
 
 corollary kernel_normal_sub:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
   shows "IsAnormalSubgroup(G,P,f-``{TheNeutralElement(H,F)})"
   using assms preimage_normal_subgroup group0.trivial_normal_subgroup 
   unfolding group0_def by auto
@@ -465,14 +482,14 @@ qed
 text\<open>The image of a group under a homomorphism is a subgroup of the target group.\<close>
 
 corollary image_group:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
   shows "IsAsubgroup(f``(G),F)"
 proof - 
   from assms(1) have "restrict(P,G\<times>G) = P" 
     using group0.group_oper_fun restrict_domain unfolding group0_def 
     by blast
-  with assms show ?thesis using image_subgroup unfolding IsAsubgroup_def
-    by simp
+  with assms show ?thesis using image_subgroup 
+    unfolding Homomor_def IsAsubgroup_def by simp
 qed
 
 text\<open>Now we are able to prove the first isomorphism theorem. This theorem states
@@ -480,16 +497,18 @@ text\<open>Now we are able to prove the first isomorphism theorem. This theorem
   and a subgroup of $H$.\<close>
 
 theorem isomorphism_first_theorem:
-  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G\<rightarrow>H"
+  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" 
   defines "r \<equiv> QuotientGroupRel(G,P,f-``{TheNeutralElement(H,F)})" and
   "\<P> \<equiv> QuotientGroupOp(G,P,f-``{TheNeutralElement(H,F)})"
   shows "\<exists>\<ff>. Homomor(\<ff>,G//r,\<P>,f``(G),restrict(F,(f``(G))\<times>(f``(G)))) \<and> \<ff>\<in>bij(G//r,f``(G))"
 proof-
   let ?\<ff> = "{\<langle>r``{g},f`(g)\<rangle>. g\<in>G}"
+  from assms(3) have ff: "f:G\<rightarrow>H"
+    unfolding Homomor_def by simp
   from assms(1-5) have "equiv(G,r)"
     using group0.Group_ZF_2_4_L3 kernel_normal_sub 
     unfolding group0_def IsAnormalSubgroup_def by simp
-  from assms(4,5) have "?\<ff> \<in> Pow((G//r)\<times>f``G)" 
+  from assms(4) ff have "?\<ff> \<in> Pow((G//r)\<times>f``(G))" 
     unfolding quotient_def using func_imagedef by auto
   moreover have "(G//r) \<subseteq> domain(?\<ff>)" unfolding domain_def quotient_def by auto 
   moreover
@@ -497,16 +516,16 @@ proof-
     then obtain g\<^sub>y g\<^sub>r where "\<langle>x, y\<rangle>=\<langle>r``{g\<^sub>y},f`(g\<^sub>y)\<rangle>" "\<langle>x, t\<rangle>=\<langle>r``{g\<^sub>r},f`(g\<^sub>r)\<rangle>" 
       and "g\<^sub>r\<in>G" "g\<^sub>y\<in>G" by auto
     hence B: "r``{g\<^sub>y}=r``{g\<^sub>r}" "y=f`(g\<^sub>y)" "t=f`(g\<^sub>r)" by auto
-    from assms(4) \<open>g\<^sub>y\<in>G\<close> \<open>g\<^sub>r\<in>G\<close> B(2,3) have "y\<in>H" "t\<in>H" 
+    from ff \<open>g\<^sub>y\<in>G\<close> \<open>g\<^sub>r\<in>G\<close> B(2,3) have "y\<in>H" "t\<in>H" 
       using apply_type by simp_all
     with \<open>equiv(G,r)\<close> \<open>g\<^sub>r\<in>G\<close> \<open>r``{g\<^sub>y}=r``{g\<^sub>r}\<close> have "\<langle>g\<^sub>y,g\<^sub>r\<rangle>\<in>r" 
       using same_image_equiv by simp
-    with assms(4,5) have 
+    with assms(4) ff have 
       "f`(P`\<langle>g\<^sub>y,GroupInv(G,P)`(g\<^sub>r)\<rangle>) = TheNeutralElement(H,F)"
       unfolding QuotientGroupRel_def using func1_1_L15 by simp
     with assms(1-4) B(2,3) \<open>g\<^sub>y\<in>G\<close> \<open>g\<^sub>r\<in>G\<close> \<open>y\<in>H\<close> \<open>t\<in>H\<close> have "y=t"
-      using image_inv Homomor_def group0.inverse_in_group group0.group0_2_L11A 
-      unfolding group0_def by auto
+      using image_inv group0.inverse_in_group group0.group0_2_L11A 
+      unfolding group0_def Homomor_def IsMorphism_def by auto
   } hence "\<forall>x y. \<langle>x,y\<rangle> \<in> ?\<ff> \<longrightarrow> (\<forall>z. \<langle>x,z\<rangle>\<in>?\<ff> \<longrightarrow> y=z)" by auto
   ultimately have ff_fun: "?\<ff>:G//r\<rightarrow>f``(G)" unfolding Pi_def function_def 
     by auto
@@ -520,19 +539,20 @@ proof-
       by simp
     from \<open>g\<^sub>1\<in>G\<close> \<open>g\<^sub>2\<in>G\<close> a have "\<langle>a\<^sub>1,f`(g\<^sub>1)\<rangle> \<in> ?\<ff>" and "\<langle>a\<^sub>2,f`(g\<^sub>2)\<rangle> \<in> ?\<ff>" by auto
     with assms(1,2,3) ff_fun \<open>g\<^sub>1\<in>G\<close> \<open>g\<^sub>2\<in>G\<close> eq have "F`\<langle>?\<ff>`(a\<^sub>1),?\<ff>`(a\<^sub>2)\<rangle> = ?\<ff>`(\<P>`\<langle>a\<^sub>1,a\<^sub>2\<rangle>)"
-      using apply_equality Homomor_def by simp
+      using apply_equality unfolding Homomor_def IsMorphism_def by simp
     moreover from AS ff_fun have "?\<ff>`(a\<^sub>1) \<in> f``(G)" "?\<ff>`(a\<^sub>2) \<in> f``(G)" 
       using apply_type by auto 
     ultimately have "restrict(F,f``(G)\<times>f``(G))`\<langle>?\<ff>`(a\<^sub>1),?\<ff>`(a\<^sub>2)\<rangle> = ?\<ff>`(\<P>`\<langle>a\<^sub>1,a\<^sub>2\<rangle>)" 
       by simp
-  } hence r: "\<forall>a\<^sub>1\<in>G//r. \<forall>a\<^sub>2\<in>G//r. restrict(F,f``G\<times>f``G)`\<langle>?\<ff>`a\<^sub>1,?\<ff>`a\<^sub>2\<rangle> = ?\<ff>`(\<P>`\<langle>a\<^sub>1,a\<^sub>2\<rangle>)" 
+  } hence 
+    r: "\<forall>a\<^sub>1\<in>G//r. \<forall>a\<^sub>2\<in>G//r. restrict(F,f``(G)\<times>f``(G))`\<langle>?\<ff>`(a\<^sub>1),?\<ff>`(a\<^sub>2)\<rangle> = ?\<ff>`(\<P>`\<langle>a\<^sub>1,a\<^sub>2\<rangle>)" 
     by simp
-  moreover from assms have G: "IsAgroup(G//r,\<P>)" 
-    using Group_ZF_2_4_T1 kernel_normal_sub by simp
-  moreover from assms(1-4) have H: "IsAgroup(f``(G), restrict(F,f``(G)\<times>f``(G)))" 
-    using image_group unfolding IsAsubgroup_def by simp
-  ultimately have HOM: "Homomor(?\<ff>,G//r,\<P>,f``(G),restrict(F,(f``(G))\<times>(f``(G))))" 
-    using Homomor_def by simp
+  with ff_fun have HOM: "Homomor(?\<ff>,G//r,\<P>,f``(G),restrict(F,(f``(G))\<times>(f``(G))))"
+    unfolding Homomor_def IsMorphism_def by simp
+  from assms have G: "IsAgroup(G//r,\<P>)" and 
+      H: "IsAgroup(f``(G), restrict(F,f``(G)\<times>f``(G)))"
+        using Group_ZF_2_4_T1 kernel_normal_sub image_group 
+        unfolding IsAsubgroup_def by simp_all
   { fix b\<^sub>1 b\<^sub>2 assume AS: "?\<ff>`(b\<^sub>1) = ?\<ff>`(b\<^sub>2)" "b\<^sub>1\<in>G//r" "b\<^sub>2\<in>G//r"
     from G AS(3) have invb2: "GroupInv(G//r,\<P>)`(b\<^sub>2)\<in>G//r" 
       using group0.inverse_in_group unfolding group0_def by simp
@@ -551,16 +571,18 @@ proof-
       EE: "F`\<langle>?\<ff>`(b\<^sub>1),?\<ff>`(GroupInv(G//r,\<P>)`(b\<^sub>2))\<rangle>=
           restrict(F,f``(G)\<times>f``(G))`\<langle>?\<ff>`(b\<^sub>1),?\<ff>`(GroupInv(G//r,\<P>)`(b\<^sub>2))\<rangle>"
       by auto
-    from assms(4) have "f``(G) \<subseteq> H" using func1_1_L6(2) by simp
+    from ff have "f``(G) \<subseteq> H" using func1_1_L6(2) by simp
     with fff have "?\<ff>`(b\<^sub>1)\<in>H" "?\<ff>`(b\<^sub>2)\<in>H" by auto
     with assms(1-4) G H HOM ff_fun AS(1,3) fff(2) EE have
-      "TheNeutralElement(H,F) = restrict(F,f``(G)\<times>f``(G))`\<langle>?\<ff>`(b\<^sub>1),?\<ff>`(GroupInv(G//r,\<P>)`(b\<^sub>2))\<rangle>"
+      "TheNeutralElement(H,F) = 
+        restrict(F,f``(G)\<times>f``(G))`\<langle>?\<ff>`(b\<^sub>1),?\<ff>`(GroupInv(G//r,\<P>)`(b\<^sub>2))\<rangle>"
       using group0.group0_2_L6(1) restrict image_inv group0.group0_3_T1 image_group 
       unfolding group0_def by simp
     also from G H HOM AS(2,3) E have "\<dots> = f`(g)"
-      using Homomor_def group0.inverse_in_group unfolding group0_def by simp
+      using group0.inverse_in_group unfolding group0_def IsMorphism_def Homomor_def
+      by simp
     finally have "TheNeutralElement(H,F) = f`(g)" by simp
-    with assms(4) \<open>g\<in>G\<close> have "g\<in>f-``{TheNeutralElement(H,F)}" using func1_1_L15 
+    with ff \<open>g\<in>G\<close> have "g\<in>f-``{TheNeutralElement(H,F)}" using func1_1_L15 
       by simp
     with assms \<open>g\<in>G\<close> gg have 
       "\<P>`\<langle>b\<^sub>1,GroupInv(G//r,\<P>)`(b\<^sub>2)\<rangle> = TheNeutralElement(G//r,\<P>)"
@@ -571,13 +593,13 @@ proof-
   } with ff_fun have "?\<ff> \<in> inj(G//r,f``(G))" unfolding inj_def by blast 
   moreover
   { fix m assume "m \<in> f``(G)"
-    with assms(4) obtain g where "g\<in>G" "m=f`(g)" using func_imagedef by auto
+    with ff obtain g where "g\<in>G" "m=f`(g)" using func_imagedef by auto
     hence "\<langle>r``{g},m\<rangle> \<in> ?\<ff>" by blast
     with ff_fun have "?\<ff>`(r``{g})=m" using apply_equality by auto
     with \<open>g\<in>G\<close> have "\<exists>A\<in>G//r. ?\<ff>`(A) = m" unfolding quotient_def by auto
   }
-  ultimately have "?\<ff> \<in> bij(G//r,f``G)" unfolding bij_def surj_def using ff_fun 
-    by blast
+  ultimately have "?\<ff> \<in> bij(G//r,f``G)" unfolding bij_def surj_def 
+    using ff_fun by blast
   with HOM show ?thesis by blast
 qed
 
@@ -585,21 +607,22 @@ text\<open>The inverse of a bijective homomorphism is an homomorphism.
   Meaning that in the previous result, the homomorphism we found is an isomorphism.\<close>
 
 theorem bij_homomor:
-  assumes "f\<in>bij(G,H)" "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
+  assumes "f\<in>bij(G,H)" "IsAgroup(G,P)" "Homomor(f,G,P,H,F)"
   shows "Homomor(converse(f),H,F,G,P)"
-proof-
+proof -
   { fix h\<^sub>1 h\<^sub>2 assume "h\<^sub>1\<in>H" "h\<^sub>2\<in>H"
     with assms(1) obtain g\<^sub>1 g\<^sub>2 where 
       g1: "g\<^sub>1\<in>G" "f`(g\<^sub>1)=h\<^sub>1" and g2: "g\<^sub>2\<in>G" "f`(g\<^sub>2)=h\<^sub>2"
       unfolding bij_def surj_def by blast
-    with assms(2,3,4) have  
+    with assms(2,3) have  
       "converse(f)`(f`(P`\<langle>g\<^sub>1,g\<^sub>2\<rangle>)) = converse(f)`(F`\<langle>h\<^sub>1,h\<^sub>2\<rangle>)"
       using homomor_eq by simp
     with assms(1,2) g1 g2 have
       "P`\<langle>converse(f)`(h\<^sub>1),converse(f)`(h\<^sub>2)\<rangle> = converse(f)`(F`\<langle>h\<^sub>1,h\<^sub>2\<rangle>)"
       using left_inverse group0.group_op_closed unfolding group0_def bij_def
       by auto
-  } with assms(2,3) show ?thesis using Homomor_def by simp
+  } with assms(1) show ?thesis using bij_converse_bij bij_is_fun 
+    unfolding Homomor_def IsMorphism_def by simp
 qed
 
 text\<open>A very important homomorphism is given by taking every element
@@ -612,8 +635,8 @@ lemma (in group0) quotient_map:
   defines "r \<equiv> QuotientGroupRel(G,P,H)" and "q \<equiv> \<lambda>x\<in>G. QuotientGroupRel(G,P,H)``{x}"
   shows "Homomor(q,G,P,G//r,QuotientGroupOp(G,P,H))"
   using groupAssum assms group_op_closed lam_funtype lamE EquivClass_1_L10 
-    Group_ZF_2_4_L3 Group_ZF_2_4_L5A Homomor_def Group_ZF_2_4_T1
-  unfolding IsAnormalSubgroup_def QuotientGroupOp_def
+    Group_ZF_2_4_L3 Group_ZF_2_4_L5A  Group_ZF_2_4_T1
+  unfolding IsAnormalSubgroup_def QuotientGroupOp_def Homomor_def IsMorphism_def
   by simp
 
 text\<open>In the context of \<open>group0\<close>, we may use all results of \<open>semigr0\<close>.\<close>
diff --git a/IsarMathLib/Ring_ZF_2.thy b/IsarMathLib/Ring_ZF_2.thy
index 56e664f..b5f1308 100644
--- a/IsarMathLib/Ring_ZF_2.thy
+++ b/IsarMathLib/Ring_ZF_2.thy
@@ -41,8 +41,9 @@ is actually a full ring.\<close>
 
 text\<open>An ideal is a subgroup of the additive group of the ring, which
 is closed by left and right multiplication by any ring element.\<close>
+
 definition (in ring0) Ideal ("_\<triangleleft>R") where
-"I \<triangleleft>R \<equiv> (\<forall>x\<in>I. \<forall>y\<in>R. y\<cdot>x\<in>I \<and> x\<cdot>y\<in>I) \<and> IsAsubgroup(I,A)"
+  "I \<triangleleft>R \<equiv> (\<forall>x\<in>I. \<forall>y\<in>R. y\<cdot>x\<in>I \<and> x\<cdot>y\<in>I) \<and> IsAsubgroup(I,A)"
 
 text\<open>To write less during proofs, we add this small definition\<close>
 abbreviation (in ring0) ideals ("\<I>") where
@@ -266,6 +267,18 @@ text\<open>Some times, we may need to sum an arbitrary number
 definition(in ring0) sumArbitraryIdeals ("\<oplus>\<^sub>I_" 90) where
   "\<J> \<subseteq> \<I> \<Longrightarrow> \<oplus>\<^sub>I\<J> \<equiv> \<langle>\<Union>\<J>\<rangle>\<^sub>I"
 
+text\<open>Each component of the sum of ideals is contained in the sum.\<close>
+
+lemma (in ring0) comp_in_sum_ideals:
+  assumes "I\<triangleleft>R" and "J\<triangleleft>R"
+  shows "I \<subseteq> I+\<^sub>IJ" and "J \<subseteq> I+\<^sub>IJ" and "I\<union>J \<subseteq> I+\<^sub>IJ"
+proof - 
+  from assms have "I\<union>J \<subseteq> R" using ideal_dest_subset
+    by auto
+  with assms show "I \<subseteq> I+\<^sub>IJ" "J \<subseteq> I+\<^sub>IJ" "I\<union>J \<subseteq> I+\<^sub>IJ"
+    using generated_ideal_contains_set sumIdeal_def by auto
+qed
+
 text\<open>Every element in the arbitrary sum of ideals
   is generated by only a finite subset of those ideals\<close>
 
diff --git a/IsarMathLib/Ring_ZF_3.thy b/IsarMathLib/Ring_ZF_3.thy
index 2808b90..82d13a4 100644
--- a/IsarMathLib/Ring_ZF_3.thy
+++ b/IsarMathLib/Ring_ZF_3.thy
@@ -35,21 +35,28 @@ theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_5
 begin
 
 text \<open>This section studies the ideals of quotient rings,
-and defines ring homomorphisms.\<close>
+  and defines ring homomorphisms.\<close>
+
+text\<open>A ring homomorphism is a function between rings that which has the
+  morphism property with respect to both addition and multiplication operation, 
+  and maps one (the neutral element of multiplication) in the first ring to one
+  in the second ring. \<close>
 
 definition
-  ringHomomor ("_{is a ring homomorphism}{_,_,_}\<rightarrow>{_,_,_}" 85)
-  where "IsAring(R,A,M) \<Longrightarrow> IsAring(S,U,V) \<Longrightarrow> ringHomomor(f,R,A,M,S,U,V) \<equiv> 
-    Homomor(f,R,A,S,U) 
-    \<and> (\<forall>x\<in>R. \<forall>y\<in>R. f`(M`\<langle>x,y\<rangle>) = V`\<langle>f`x,f`y\<rangle>) 
-    \<and> f`(TheNeutralElement(R,M)) = TheNeutralElement(S,V)"
+  "ringHomomor(f,R,A,M,S,U,V) \<equiv> f:R\<rightarrow>S \<and> IsMorphism(R,A,U,f) \<and> IsMorphism(R,M,V,f) 
+  \<and> f`(TheNeutralElement(R,M)) = TheNeutralElement(S,V)"
+
+text\<open>The next locale defines notation which we will use in this theory.
+  We assume that we have two rings, one (which we will call the origin ring) 
+  defined by the triple $(R,A,M)$  
+  and the second one (which we will call the target ring) by the triple $(S,U,V)$, 
+  and a homomorphism $f:R\rightarrow S$. \<close>
 
 locale ring_homo =
   fixes R A M S U V f
-  assumes origin:"IsAring(R,A,M)" 
-    and target:"IsAring(S,U,V)"
-    and fun:"f:R\<rightarrow>S"
-    and homomorphism:"f{is a ring homomorphism}{R,A,M}\<rightarrow>{S,U,V}"
+  assumes origin: "IsAring(R,A,M)" 
+    and target: "IsAring(S,U,V)"
+    and homomorphism: "ringHomomor(f,R,A,M,S,U,V)"
 
   fixes ringa (infixl "\<ra>\<^sub>R" 90)
   defines ringa_def [simp]: "x\<ra>\<^sub>Rb \<equiv> A`\<langle>x,b\<rangle>"
@@ -99,209 +106,300 @@ locale ring_homo =
   fixes ringsqs ("_\<^sup>2\<^sup>S" [96] 97)
   defines ringsqs_def [simp]: "x\<^sup>2\<^sup>S \<equiv> x\<cdot>\<^sub>Sx"
 
+text\<open>We will write \<open>I\<triangleleft>R\<^sub>o\<close> to denote that $I$ is an ideal
+  of the ring $R$. Note that in this notation the \<open>R\<^sub>o\<close> part by itself has no meaning,
+  only the whole \<open>\<triangleleft>R\<^sub>o\<close> serves as postfix operator. \<close>
+
 abbreviation (in ring_homo) ideal_origin ("_\<triangleleft>R\<^sub>o")
   where "I\<triangleleft>R\<^sub>o \<equiv> ring0.Ideal(R,A,M,I)"
 
-abbreviation (in ring_homo) prime_ideal_target ("_\<triangleleft>\<^sub>pR\<^sub>t")
-  where "I\<triangleleft>\<^sub>pR\<^sub>t \<equiv> ring0.primeIdeal(S,U,V,I)"
+text\<open>\<open>I\<triangleleft>R\<^sub>t\<close> means that $I$ is an ideal of $S$.\<close>
+
+abbreviation (in ring_homo) ideal_target ("_\<triangleleft>R\<^sub>t")
+  where "I\<triangleleft>R\<^sub>t \<equiv> ring0.Ideal(S,U,V,I)"
+
+text\<open> \<open>I\<triangleleft>\<^sub>pR\<^sub>o\<close> means that $I$ is a prime ideal of $R$.\<close>
 
 abbreviation (in ring_homo) prime_ideal_origin ("_\<triangleleft>\<^sub>pR\<^sub>o")
   where "I\<triangleleft>\<^sub>pR\<^sub>o \<equiv> ring0.primeIdeal(R,A,M,I)"
 
-abbreviation (in ring_homo) ideal_target ("_\<triangleleft>R\<^sub>t")
-  where "I\<triangleleft>R\<^sub>t \<equiv> ring0.Ideal(S,U,V,I)"
+text\<open>We will write \<open>I\<triangleleft>\<^sub>pR\<^sub>t\<close> to denote that $I$ is a prime ideal of the ring $S$. \<close>
+
+abbreviation (in ring_homo) prime_ideal_target ("_\<triangleleft>\<^sub>pR\<^sub>t")
+  where "I\<triangleleft>\<^sub>pR\<^sub>t \<equiv> ring0.primeIdeal(S,U,V,I)"
+
+text\<open> \<open>ker\<close> denotes the kernel of $f$ (which is assumed to be a homomorphism
+  between $R$ and $S$.\<close>
 
 abbreviation (in ring_homo) kernel ("ker" 90) where
   "ker \<equiv> f-``{\<zero>\<^sub>S}"
 
+text\<open>The theorems proven in the \<open>ring0\<close> context are valid in the \<open>ring_homo\<close> 
+  context when applied to the ring $R$.\<close>
+
 sublocale ring_homo < origin_ring:ring0
   using origin unfolding ring0_def by auto
 
-sublocale ring_homo < target_ring:ring0 S U V ringas
-  ringminuss ringsubs ringms ringzeros ringones ringtwos
-  ringsqs
+text\<open>The theorems proven in the \<open>ring0\<close> context are valid in the \<open>ring_homo\<close> 
+  context when applied to the ring $S$.\<close>
+
+sublocale ring_homo < target_ring:ring0 S U V ringas ringminuss 
+  ringsubs ringms ringzeros ringones ringtwos ringsqs
   using target unfolding ring0_def by auto
 
+text\<open>A ring homomorphism is a homomorphism both with respect to
+  addition and multiplication.\<close>
+
+lemma ringHomHom: assumes "ringHomomor(f,R,A,M,S,U,V)"
+  shows "Homomor(f,R,A,S,U)" and "Homomor(f,R,M,S,V)"
+  using assms unfolding ringHomomor_def Homomor_def 
+  by simp_all
+
+text\<open>Since in the \<open>ring_homo\<close> locale $f$ is a ring homomorphism it implies
+  that $f$ is a function from $R$ to $S$. \<close>
+
+lemma (in ring_homo) f_is_fun: shows "f:R\<rightarrow>S"
+  using homomorphism unfolding ringHomomor_def by simp
+
+text\<open>In the \<open>ring_homo\<close> context $A$ is the addition in the first (source) ring
+   $M$ is the multiplication there and $U,V$ are the addition and multiplication resp.
+  in the second (target) ring. The next lemma states the all these are binary
+  operations, a trivial, but frequently used fact.\<close>
+
+lemma (in ring_homo) AMUV_are_ops: 
+  shows "A:R\<times>R\<rightarrow>R" "M:R\<times>R\<rightarrow>R" "U:S\<times>S\<rightarrow>S" "V:S\<times>S\<rightarrow>S"
+  using origin target 
+  unfolding IsAring_def IsAgroup_def IsAmonoid_def IsAssociative_def
+  by auto
+
+text\<open>The kernel is a subset of $R$ on which the value of $f$ is zero 
+  (of the target ring)\<close>
+
+lemma (in ring_homo) kernel_def_alt: shows "ker = {r\<in>R. f`(r) = \<zero>\<^sub>S}"
+  using f_is_fun func1_1_L14 by simp  
+
+text\<open> the homomorphism $f$ maps each element of the kernel 
+  to zero of the target ring. \<close>
+
+lemma (in ring_homo) image_kernel:
+  assumes "x\<in>ker"
+  shows "f`(x) = \<zero>\<^sub>S"
+  using assms func1_1_L15 f_is_fun by simp
+
+text\<open> As a ring homomorphism $f$ preserves multiplication.\<close>
+
 lemma (in ring_homo) homomor_dest_mult:
   assumes "x\<in>R" "y\<in>R"
-  shows "f`(x\<cdot>\<^sub>Ry) = (f`x)\<cdot>\<^sub>S(f`y)"
-  using assms origin target homomorphism ringHomomor_def by auto
+  shows "f`(x\<cdot>\<^sub>Ry) = (f`(x))\<cdot>\<^sub>S(f`(y))"
+  using assms origin target homomorphism 
+  unfolding ringHomomor_def IsMorphism_def by simp
+
+text\<open> As a ring homomorphism $f$ preserves addition. \<close>
 
 lemma (in ring_homo) homomor_dest_add:
   assumes "x\<in>R" "y\<in>R"
-  shows "f`(x\<ra>\<^sub>Ry) = (f`x)\<ra>\<^sub>S(f`y)"
-  using homomor_eq[of R A S U f x y]
-  origin target homomorphism assms
-  unfolding IsAring_def ringHomomor_def[OF origin target]
-  by auto
+  shows "f`(x\<ra>\<^sub>Ry) = (f`(x))\<ra>\<^sub>S(f`(y))"
+  using homomor_eq origin target homomorphism assms
+  unfolding IsAring_def ringHomomor_def IsMorphism_def
+  by simp
+
+text\<open>For $x\in R$ the value of $f$ is in $S$.\<close>
+
+lemma (in ring_homo) homomor_val: assumes "x\<in>R"
+  shows "f`(x) \<in> S" 
+  using homomorphism assms apply_funtype unfolding ringHomomor_def 
+  by blast
+
+text\<open>A ring homomorphism preserves taking negative of an element.\<close>
 
 lemma (in ring_homo) homomor_dest_minus:
   assumes "x\<in>R"
-  shows "f`(\<rm>\<^sub>Rx) = \<rm>\<^sub>S(f`x)"
-  using image_inv[of R A S U f x]
-  origin target homomorphism assms fun
-  unfolding IsAring_def ringHomomor_def[OF origin target]
-  by auto
+  shows "f`(\<rm>\<^sub>Rx) = \<rm>\<^sub>S(f`(x))"
+  using origin target homomorphism assms ringHomHom image_inv
+  unfolding IsAring_def by auto
+
+text\<open>A ring homomorphism preserves substraction.\<close> 
 
 lemma (in ring_homo) homomor_dest_subs:
   assumes "x\<in>R" "y\<in>R"
-  shows "f`(x\<rs>\<^sub>Ry) = (f`x)\<rs>\<^sub>S(f`y)"
-  using assms homomor_dest_add[of x "\<rm>\<^sub>Ry"]
-    homomor_dest_minus[of y]
+  shows "f`(x\<rs>\<^sub>Ry) = (f`(x))\<rs>\<^sub>S(f`(y))"
+  using assms homomor_dest_add homomor_dest_minus
   using origin_ring.Ring_ZF_1_L3(1) by auto
 
+text\<open>A ring homomorphism maps zero to zero.\<close>
 
 lemma (in ring_homo) homomor_dest_zero:
   shows "f`(\<zero>\<^sub>R) = \<zero>\<^sub>S"
-proof-
-  have "f`(\<zero>\<^sub>R) = f`(\<zero>\<^sub>R\<rs>\<^sub>R\<zero>\<^sub>R)"
-    using origin_ring.Ring_ZF_1_L3(7) origin_ring.Ring_ZF_1_L2(1)
-    by auto
-  then have "f`(\<zero>\<^sub>R) = f`(\<zero>\<^sub>R)\<rs>\<^sub>S(f`\<zero>\<^sub>R)"
-    using homomor_dest_subs origin_ring.Ring_ZF_1_L2(1)
-    by auto
-  then show ?thesis using target_ring.Ring_ZF_1_L3(7)
-    origin_ring.Ring_ZF_1_L2(1) apply_type[OF fun] by auto
+  using origin target homomorphism ringHomHom(1) image_neutral
+  unfolding IsAring_def by auto
+
+text\<open>The kernel of a homomorphism is never empty.\<close>
+
+lemma (in ring_homo) kernel_non_empty: 
+  shows "\<zero>\<^sub>R \<in>ker" and "ker\<noteq>0"
+  using homomor_dest_zero origin_ring.Ring_ZF_1_L2(1)
+    func1_1_L15 f_is_fun by auto
+
+text\<open>The image of the kernel by $f$ is the singleton $\{ 0_R\}$.\<close>
+
+corollary (in ring_homo) image_kernel_2: shows "f``(ker) = {\<zero>\<^sub>S}"
+proof -
+  have "f:R\<rightarrow>S" "ker\<subseteq>R" "ker\<noteq>0" "\<forall>x\<in>ker. f`(x) = \<zero>\<^sub>S"
+    using f_is_fun kernel_def_alt kernel_non_empty by auto
+  then show  "f``(ker) = {\<zero>\<^sub>S}" using image_constant_singleton
+    by simp
 qed
-    
+
+text\<open>The inverse image of an ideal (in the target ring) is
+  a normal subgroup of the addition group and an ideal in the origin ring. 
+  The kernel of the homomorphism
+  is a subset of the inverse of image of every ideal. \<close>
 
 lemma (in ring_homo) preimage_ideal:
   assumes "J\<triangleleft>R\<^sub>t"
-  shows "(f-``J)\<triangleleft>R\<^sub>o" "ker \<subseteq> f-``J"
-proof-
-  have "IsAnormalSubgroup(R,A,f-``J)"
-    using preimage_normal_subgroup[OF _ _ _ fun]
-      target_ring.ideal_normal_add_subgroup origin assms
-      target homomorphism
-    unfolding IsAring_def ring0_def
-    ringHomomor_def[OF origin target] by auto
-  then have "IsAsubgroup(f-``J,A)" unfolding IsAnormalSubgroup_def
-    by auto moreover
-  {
-    fix x y assume xy:"x\<in>f-``J" "y\<in>R"
-    from xy(1) have "f`x \<in> J" "x\<in>R" using func1_1_L15 fun
-      by auto
-    moreover have "f`y\<in>S" using xy(2) apply_type fun
-      by auto
-    ultimately have "V`\<langle>f`x,f`y\<rangle>\<in>J" "V`\<langle>f`y,f`x\<rangle>\<in>J"
-      using target_ring.ideal_dest_mult assms
-      by auto
-    then have "f`(M`\<langle>x,y\<rangle>)\<in>J" "f`(M`\<langle>y,x\<rangle>)\<in>J"
-      using homomor_dest_mult xy(2) \<open>x\<in>R\<close>
-      by auto
-    moreover have "M`\<langle>x,y\<rangle>\<in>R" "M`\<langle>y,x\<rangle>\<in>R" using xy(2) \<open>x\<in>R\<close>
-      origin_ring.Ring_ZF_1_L4(3) by auto
-    ultimately have "M`\<langle>x,y\<rangle>\<in>f-``J" "M`\<langle>y,x\<rangle>\<in>f-``J"
-      using func1_1_L15 fun by auto
+  shows
+    "IsAnormalSubgroup(R,A,f-``(J))"
+    "(f-``(J))\<triangleleft>R\<^sub>o" "ker \<subseteq> f-``(J)"
+proof -
+  from origin target homomorphism assms 
+    show "IsAnormalSubgroup(R,A,f-``(J))"
+      using ringHomHom(1) preimage_normal_subgroup
+        target_ring.ideal_normal_add_subgroup
+      unfolding IsAring_def by blast
+  then have "IsAsubgroup(f-``(J),A)" unfolding IsAnormalSubgroup_def
+    by auto 
+  moreover
+  { fix x y assume "x \<in> f-``(J)" "y\<in>R"
+    from homomorphism have "f:R\<rightarrow>S"
+      unfolding ringHomomor_def by simp
+    with \<open>x \<in> f-``(J)\<close> have "x\<in>R" and "f`(x) \<in> J"
+      using func1_1_L15 unfolding ringHomomor_def
+      by simp_all
+    with assms \<open>y\<in>R\<close> \<open>f:R\<rightarrow>S\<close> have 
+      "V`\<langle>f`(x),f`(y)\<rangle> \<in> J" and "V`\<langle>f`(y),f`(x)\<rangle>\<in>J"
+      using apply_funtype target_ring.ideal_dest_mult by simp_all
+    with \<open>x\<in>R\<close> \<open>y\<in>R\<close> have "f`(M`\<langle>x,y\<rangle>) \<in> J" and "f`(M`\<langle>y,x\<rangle>) \<in> J"
+      using homomor_dest_mult by auto
+    with \<open>x\<in>R\<close> \<open>y\<in>R\<close> \<open>f:R\<rightarrow>S\<close> have 
+      "M`\<langle>x,y\<rangle> \<in> f-``(J)" and "M`\<langle>y,x\<rangle> \<in> f-``(J)"
+      using origin_ring.Ring_ZF_1_L4(3) func1_1_L15 by auto 
   }
-  ultimately show "(f-``J)\<triangleleft>R\<^sub>o" using origin_ring.Ideal_def by auto
-  have "\<zero>\<^sub>S\<in>J" using assms target_ring.ideal_dest_zero by auto
-  then show "ker \<subseteq> f-``J" by auto
+  ultimately show "(f-``(J))\<triangleleft>R\<^sub>o" using origin_ring.Ideal_def 
+    by auto
+  from assms show "ker \<subseteq> f-``(J)" using target_ring.ideal_dest_zero
+    by auto
+qed
+
+text\<open>Kernel of the homomorphism in an ideal.\<close>
+
+lemma (in ring_homo) kernel_ideal: shows "ker \<triangleleft>R\<^sub>o"
+  using target_ring.zero_ideal preimage_ideal(2) by simp
+
+text\<open>The inverse image of a prime ideal by a homomorphism is not the whole ring.
+  Proof by contradiction.\<close>
+
+lemma (in ring_homo) vimage_prime_ideal_not_all:
+  assumes "J\<triangleleft>\<^sub>pR\<^sub>t" shows "f-``(J) \<noteq> R"
+proof -
+  { assume "R = f-``(J)"
+    then have "R = {x\<in>R. f`(x)\<in>J}" using f_is_fun func1_1_L15 
+      by simp
+    then have "\<one>\<^sub>R \<in> {x\<in>R. f`(x)\<in>J}" using origin_ring.Ring_ZF_1_L2(2)
+      by simp
+    with origin_ring.ringAssum target_ring.ringAssum homomorphism assms
+      have False using target_ring.ideal_with_one
+        unfolding target_ring.primeIdeal_def ringHomomor_def by auto
+  } thus "f-``(J) \<noteq> R" by blast
 qed
 
 text\<open>Even more, if the target ring of the homomorphism is commutative
-or the homomorphism is surjective; we show that if the ideal es prime,
-then its preimage is also. Note that this is not true in general.\<close>
+  and the ideal is prime then its preimage is also. Note that this is 
+  not true in general.\<close>
 
 lemma (in ring_homo) preimage_prime_ideal_comm:
-  assumes "J\<triangleleft>\<^sub>pR\<^sub>t" "V{is commutative on}S"
-  shows "(f-``J)\<triangleleft>\<^sub>pR\<^sub>o" 
-proof(rule origin_ring.equivalent_prime_ideal_2)
-  show "(f-``J)\<triangleleft>R\<^sub>o" using preimage_ideal assms unfolding target_ring.primeIdeal_def by auto
-  {
-    assume "R = f-`` J"
-    then have "R = {x\<in>R. f`x \<in>J}"
-      using fun func1_1_L15 by auto
-    moreover have "\<one>\<^sub>R\<in>R" using origin_ring.Ring_ZF_1_L2(2).
-    ultimately have "\<one>\<^sub>R\<in>{x\<in>R. f`x \<in>J}" by auto
-    then have "f`(\<one>\<^sub>R) \<in>J" by auto
-    moreover have "f`\<one>\<^sub>R = \<one>\<^sub>S" using homomorphism
-      unfolding ringHomomor_def[OF origin_ring.ringAssum
-          target_ring.ringAssum] by auto
-    ultimately have "\<one>\<^sub>S \<in> J" by auto
-    then have False using target_ring.ideal_with_one
-      assms unfolding target_ring.primeIdeal_def by auto
-  }
-  then show "f -`` J \<noteq> R" by auto
-  show "\<forall>x\<in>R. \<forall>y\<in>R. (\<forall>z\<in>R. x \<cdot>\<^sub>R z \<cdot>\<^sub>R y \<in> f -`` J) \<longrightarrow>
-                 x \<in> f -`` J \<or> y \<in> f -`` J"
-  proof(safe)
-    fix x y assume as:"x\<in>R" "y\<in>R" "\<forall>z\<in>R. x \<cdot>\<^sub>R z \<cdot>\<^sub>R y \<in> f -`` J" "y \<notin> f -`` J"
-    {
-      fix s assume s:"s\<in>S"
-      then have "(f`x)\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`y) = s\<cdot>\<^sub>S((f`x)\<cdot>\<^sub>S(f`y))"
-        using assms(2) unfolding IsCommutative_def
-        using apply_type[OF fun as(1)] 
-          target_ring.Ring_ZF_1_L11(2) apply_type[OF fun as(2)]
-        by auto
-      then have "(f`x)\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`y) = s\<cdot>\<^sub>S(f`(x\<cdot>\<^sub>Ry))"
-        using homomor_dest_mult[OF as(1,2)]
-        by auto moreover
-      from as(3) have "x\<cdot>\<^sub>Ry : f-``J" using origin_ring.Ring_ZF_1_L2(2)
-        origin_ring.Ring_ZF_1_L3(5)[OF as(1)] by force
-      then have "f`(x\<cdot>\<^sub>Ry) : J" using func1_1_L15 fun by auto
-      with s have "s\<cdot>\<^sub>S(f`(x\<cdot>\<^sub>Ry)) :J" using assms(1)
-        unfolding target_ring.primeIdeal_def using target_ring.ideal_dest_mult(2)
-        by auto
-      ultimately have "(f`x)\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`y):J" by auto
-    }
-    then have "\<forall>z\<in>S. (f`x) \<cdot>\<^sub>S z \<cdot>\<^sub>S (f`y) \<in> J" by auto
-    with target_ring.equivalent_prime_ideal[OF assms(1)]
-    apply_type[OF fun] as(1,2) have "f`x:J\<or>f`y:J" by auto
-    with as(4,2) have "f`x:J" using func1_1_L15 fun by auto
-    then show "x:f-``J" using as(1) func1_1_L15 fun by auto
+  assumes "J\<triangleleft>\<^sub>pR\<^sub>t" "V {is commutative on} S"
+  shows "(f-``(J))\<triangleleft>\<^sub>pR\<^sub>o" 
+proof -
+  have "\<forall>x\<in>R. \<forall>y\<in>R. (\<forall>z\<in>R. x\<cdot>\<^sub>Rz\<cdot>\<^sub>Ry \<in> f-``(J)) \<longrightarrow> x\<in>f-``(J) \<or> y\<in>f-``( J)"
+  proof -
+    { fix x y assume "x\<in>R" "y\<in>R" and as: "\<forall>z\<in>R. x\<cdot>\<^sub>Rz\<cdot>\<^sub>Ry \<in> f-``(J)" 
+        and "y \<notin> f-``(J)"
+      { fix s assume "s\<in>S"
+        with assms(2) \<open>x\<in>R\<close> \<open>y\<in>R\<close> have 
+          "(f`(x))\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`(y)) = s\<cdot>\<^sub>S((f`(x))\<cdot>\<^sub>S(f`(y)))"
+          using f_is_fun apply_funtype target_ring.Ring_ZF_1_L11(2)
+          unfolding IsCommutative_def by auto
+        with \<open>x\<in>R\<close> \<open>y\<in>R\<close> have "(f`x)\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`y) = s\<cdot>\<^sub>S(f`(x\<cdot>\<^sub>Ry))"
+          using homomor_dest_mult by simp
+        with assms(1) \<open>s\<in>S\<close> \<open>x\<in>R\<close> as have "(f`(x))\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`(y)) \<in> J"
+          using origin_ring.Ring_ZF_1_L2(2) origin_ring.Ring_ZF_1_L3(5)
+            func1_1_L15 f_is_fun target_ring.ideal_dest_mult(2)
+          unfolding target_ring.primeIdeal_def by auto
+      } hence "\<forall>z\<in>S. (f`x) \<cdot>\<^sub>S z \<cdot>\<^sub>S (f`y) \<in> J" by simp
+      with assms(1) \<open>x\<in>R\<close> \<open>y\<in>R\<close>  have "f`(x)\<in> J \<or> f`(y)\<in>J" 
+        using target_ring.equivalent_prime_ideal f_is_fun apply_funtype 
+          by simp
+      with \<open>x\<in>R\<close> \<open>y\<in>R\<close> \<open>y \<notin> f-``(J)\<close> have "x\<in>f-``(J)"
+        using func1_1_L15 f_is_fun by simp
+    } thus ?thesis by blast
   qed
+  moreover from assms have "(f-``J)\<triangleleft>R\<^sub>o" using preimage_ideal 
+    unfolding target_ring.primeIdeal_def by auto
+  moreover from assms(1) have "f-``(J) \<noteq> R" using vimage_prime_ideal_not_all 
+    by simp
+  ultimately show "(f-``(J))\<triangleleft>\<^sub>pR\<^sub>o" 
+    by (rule origin_ring.equivalent_prime_ideal_2)
 qed
 
+text\<open>We can replace the assumption that the target ring of the homomorphism is commutative
+  with the assumption that homomorphism is surjective in \<open>preimage_prime_ideal_comm\<close>
+  above and we can show the same assertion that the preimage of a prime ideal prime. \<close>
+
 lemma (in ring_homo) preimage_prime_ideal_surj:
-  assumes "J\<triangleleft>\<^sub>pR\<^sub>t" "f:surj(R,S)"
-  shows "(f-``J)\<triangleleft>\<^sub>pR\<^sub>o" 
-proof(rule origin_ring.equivalent_prime_ideal_2)
-  show "(f-``J)\<triangleleft>R\<^sub>o" using preimage_ideal assms unfolding target_ring.primeIdeal_def by auto
-  {
-    assume "R = f-`` J"
-    then have "R = {x\<in>R. f`x \<in>J}"
-      using fun func1_1_L15 by auto
-    moreover have "\<one>\<^sub>R\<in>R" using origin_ring.Ring_ZF_1_L2(2).
-    ultimately have "\<one>\<^sub>R\<in>{x\<in>R. f`x \<in>J}" by auto
-    then have "f`(\<one>\<^sub>R) \<in>J" by auto
-    moreover have "f`\<one>\<^sub>R = \<one>\<^sub>S" using homomorphism
-      unfolding ringHomomor_def[OF origin_ring.ringAssum
-          target_ring.ringAssum] by auto
-    ultimately have "\<one>\<^sub>S \<in> J" by auto
-    then have False using target_ring.ideal_with_one
-      assms unfolding target_ring.primeIdeal_def by auto
-  }
-  then show "f -`` J \<noteq> R" by auto
-  show "\<forall>x\<in>R. \<forall>y\<in>R. (\<forall>z\<in>R. x \<cdot>\<^sub>R z \<cdot>\<^sub>R y \<in> f -`` J) \<longrightarrow>
-                 x \<in> f -`` J \<or> y \<in> f -`` J"
-  proof(safe)
-    fix x y assume as:"x\<in>R" "y\<in>R" "\<forall>z\<in>R. x \<cdot>\<^sub>R z \<cdot>\<^sub>R y \<in> f -`` J" "y \<notin> f -`` J"
-    {
-      fix s assume s:"s\<in>S"
-      with assms(2) obtain t where t:"s=f`t" "t:R"
-        unfolding surj_def by auto
-      then have "(f`x)\<cdot>\<^sub>S(f`t)\<cdot>\<^sub>S(f`y) = f`(x\<cdot>\<^sub>Rt\<cdot>\<^sub>Ry)"
-        using homomor_dest_mult as(1,2) t(2)
-        origin_ring.Ring_ZF_1_L4(3) by auto
-      moreover have "(x\<cdot>\<^sub>Rt\<cdot>\<^sub>Ry)\<in>f-``J" using as(3) t(2) by auto
-      ultimately have "(f`x)\<cdot>\<^sub>S(f`t)\<cdot>\<^sub>S(f`y)\<in>J" 
-        using func1_1_L15 fun by auto
-      with t(1) have "(f`x)\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`y)\<in>J" by auto
-    }
-    then have "\<forall>z\<in>S. (f`x) \<cdot>\<^sub>S z \<cdot>\<^sub>S (f`y) \<in> J" by auto
-    with target_ring.equivalent_prime_ideal[OF assms(1)]
-    apply_type[OF fun] as(1,2) have "f`x:J\<or>f`y:J" by auto
-    with as(4,2) have "f`x:J" using func1_1_L15 fun by auto
-    then show "x:f-``J" using as(1) func1_1_L15 fun by auto
+  assumes "J\<triangleleft>\<^sub>pR\<^sub>t" "f \<in> surj(R,S)"
+  shows "(f-``(J))\<triangleleft>\<^sub>pR\<^sub>o" 
+proof -
+  have "\<forall>x\<in>R. \<forall>y\<in>R. (\<forall>z\<in>R. x\<cdot>\<^sub>Rz\<cdot>\<^sub>Ry \<in> f-``(J)) \<longrightarrow> x\<in>f-``(J) \<or> y\<in>f-``(J)"
+  proof -
+    { fix x y assume "x\<in>R" "y\<in>R" and as: "\<forall>z\<in>R. x\<cdot>\<^sub>Rz\<cdot>\<^sub>Ry \<in> f-``(J)" 
+        and "y \<notin> f-``(J)"
+      { fix s assume s: "s\<in>S"
+        with assms(2) obtain t where "s=f`(t)" "t\<in>R"
+          unfolding surj_def by auto
+        with \<open>x\<in>R\<close> \<open>y\<in>R\<close> as have "(f`x)\<cdot>\<^sub>Ss\<cdot>\<^sub>S(f`y)\<in>J"
+          using homomor_dest_mult origin_ring.Ring_ZF_1_L4(3) 
+            func1_1_L15 f_is_fun by simp
+      } hence "\<forall>z\<in>S. (f`(x)) \<cdot>\<^sub>S z \<cdot>\<^sub>S (f`(y)) \<in> J" by simp
+      with target_ring.equivalent_prime_ideal assms(1) \<open>x\<in>R\<close> \<open>y\<in>R\<close>
+      have "f`(x)\<in>J\<or>f`(y)\<in>J" using f_is_fun apply_funtype 
+        by auto
+      with \<open>x\<in>R\<close> \<open>y\<in>R\<close> \<open>y \<notin> f-``(J)\<close> have "x\<in>f-``(J)" 
+        using func1_1_L15 f_is_fun by auto
+    } thus ?thesis by blast
   qed
+  moreover from assms have "(f-``(J))\<triangleleft>R\<^sub>o" using preimage_ideal 
+    unfolding target_ring.primeIdeal_def by auto
+  moreover from assms(1) have "f-``(J) \<noteq> R" using vimage_prime_ideal_not_all 
+    by simp
+  ultimately show "(f-``(J))\<triangleleft>\<^sub>pR\<^sub>o" 
+    by (rule origin_ring.equivalent_prime_ideal_2)
 qed
 
 section\<open>Quotient ring with quotient map\<close>
 
+text\<open>The notion of a quotient ring (a.k.a factor ring, difference ring or residue class) 
+  is analogous to the notion of quotient group from the group theory. \<close>
+
+text\<open>The next locale \<open>ring2\<close> extends the \<open>ring0\<close> locale (defined in the \<open>Ring_ZF\<close> theory)
+   with the assumption that some fixed set $I$ is an ideal. It also defines some notation
+  related to quotient rings, in particular we define the function (projection)
+  $f_I$ that maps each element $r$ of the ring $R$ to its class $r_I(\{ r\}$
+  where $r_I$ is the quotient group relation defined by $I$ as a (normal) subgroup 
+  of $R$ with addition. \<close> 
+
 locale ring2 = ring0 +
   fixes I
-  assumes idealAssum:"I\<triangleleft>R"
+  assumes idealAssum: "I\<triangleleft>R"
 
   fixes quot ("R\<^sub>I")
   defines quot_def [simp]: "R\<^sub>I \<equiv> QuotientBy(I)"
@@ -310,7 +408,7 @@ locale ring2 = ring0 +
   defines qrel_def [simp]: "r\<^sub>I \<equiv> QuotientGroupRel(R,A,I)"
 
   fixes qfun ("f\<^sub>I")
-  defines qfun_def [simp]: "f\<^sub>I \<equiv> \<lambda>r\<in>R. r\<^sub>I ``{r}"
+  defines qfun_def [simp]: "f\<^sub>I \<equiv> \<lambda>r\<in>R. r\<^sub>I``{r}"
 
   fixes qadd ("A\<^sub>I")
   defines qadd_def [simp]: "A\<^sub>I \<equiv> QuotientGroupOp(R, A, I)"
@@ -318,737 +416,558 @@ locale ring2 = ring0 +
   fixes qmul ("M\<^sub>I")
   defines qmul_def [simp]: "M\<^sub>I \<equiv> ProjFun2(R, qrel, M)"
 
+text\<open>The expression \<open>J\<triangleleft>R\<^sub>I\<close> will mean that $J$ is an ideal of the quotient ring $R_I$
+  (with the quotient addition and multiplication).\<close>
+
 abbreviation (in ring2) qideal ("_\<triangleleft>R\<^sub>I") where
   "J\<triangleleft>R\<^sub>I \<equiv> ring0.Ideal(R\<^sub>I,A\<^sub>I,M\<^sub>I,J)"
 
+text\<open>In the \<open>ring2\<close> The expression \<open>J\<triangleleft>\<^sub>pR\<^sub>I\<close> means that $J$ is a prime ideal of the quotient 
+  ring $R_I$. \<close>
+
 abbreviation (in ring2) qprimeIdeal ("_\<triangleleft>\<^sub>pR\<^sub>I") where
   "J\<triangleleft>\<^sub>pR\<^sub>I \<equiv> ring0.primeIdeal(R\<^sub>I,A\<^sub>I,M\<^sub>I,J)"
 
-lemma (in ring_homo) image_kernel:
-  assumes "x\<in>ker"
-  shows "f`x = \<zero>\<^sub>S"
-  using assms func1_1_L15 fun by auto
-
-corollary (in ring_homo) image_kernel_2:
-  shows "f``(ker) = {\<zero>\<^sub>S}"
-proof-
-  have "\<zero>\<^sub>R \<in>ker" using homomor_dest_zero origin_ring.Ring_ZF_1_L2(1)
-    func1_1_L15 fun by auto moreover
-  have "ker \<subseteq> R" using func1_1_L15[OF fun, of "{\<zero>\<^sub>S}"] by auto
-  then have "f `` (ker) = {f ` x . x \<in> ker}" 
-    using func_imagedef[OF fun, of ker] by auto
-  ultimately show ?thesis using image_kernel by auto
-qed
+text\<open>Theorems proven in the \<open>ring0\<close> context can be applied
+  to the quotient ring in the \<open>ring2\<close> context. \<close>
 
 sublocale ring2 < quotient_ring: ring0 quot qadd qmul
   "\<lambda>x y. ideal_radd(x,I,y)" "\<lambda>y. ideal_rmin(I,y)" 
   "\<lambda>x y. ideal_rsub(x,I,y)" "\<lambda>x y. ideal_rmult(x,I,y)"
-  "\<zero>\<^sub>I" "\<one>\<^sub>I" "\<two>\<^sub>I" "\<lambda>x. (x\<^sup>2\<^sup>I)" unfolding ring0_def quot_def
-  using quotientBy_is_ring[OF idealAssum] apply simp
-  unfolding ideal_radd_def ideal_rmin_def
-            ideal_rsub_def ideal_rmult_def
-         ideal_rzero_def ideal_rone_def
-         ideal_rtwo_def ideal_rsqr_def apply auto
-  using neutral_quotient[OF idealAssum] apply simp
-  using one_quotient[OF idealAssum] apply simp
-  using two_quotient[OF idealAssum] by simp
-
-text\<open>The quotient map is a homomorphism of rings\<close>
+  "\<zero>\<^sub>I" "\<one>\<^sub>I" "\<two>\<^sub>I" "\<lambda>x. (x\<^sup>2\<^sup>I)" 
+  using quotientBy_is_ring idealAssum neutral_quotient 
+    one_quotient two_quotient
+  unfolding ring0_def  ideal_radd_def ideal_rmin_def
+    ideal_rsub_def ideal_rmult_def ideal_rzero_def 
+    ideal_rone_def ideal_rtwo_def ideal_rsqr_def by auto
+
+text\<open>The quotient map is a homomorphism of rings. This is probably one of the
+  most sophisticated facts in IsarMathlib that Isabelle's simp method proves  
+  from 10 facts and 5 definitions. \<close>
 
 theorem (in ring2) quotient_fun_homomor:
-  shows "f\<^sub>I{is a ring homomorphism}{R,A,M}\<rightarrow>{R\<^sub>I,A\<^sub>I,M\<^sub>I}"
-  unfolding ringHomomor_def[OF ringAssum quotient_ring.ringAssum]
-proof(safe)
-  from add_group.quotient_map[OF ideal_normal_add_subgroup[OF idealAssum]]
-    show "Homomor(f\<^sub>I,R,A,R\<^sub>I,A\<^sub>I)"
-    unfolding qfun_def quot_def qadd_def QuotientBy_def[OF idealAssum] by auto
-  {
-    fix x y assume as:"x\<in>R" "y\<in>R"
-    have "f\<^sub>I ` (x\<cdot>y) = QuotientGroupRel(R,A,I)``{x\<cdot>y}" 
-      unfolding qfun_def using as Ring_ZF_1_L4(3)
-      lamE lam_funtype by auto
-    then have "f\<^sub>I ` (x\<cdot>y) = ((QuotientGroupRel(R,A,I)``{x}){\<cdot>I}(QuotientGroupRel(R,A,I)``{y}))"
-      using EquivClass_1_L10[OF equiv_rel[OF idealAssum]
-          quotientBy_mul_monoid(1)[OF idealAssum]] as by auto
-    then have "f\<^sub>I ` (x\<cdot>y) = ((f\<^sub>I `x){\<cdot>I}(f\<^sub>I `y))" unfolding qfun_def
-      using as lamE lam_funtype by auto
-    then show "f\<^sub>I ` (M ` \<langle>x, y\<rangle>) =M\<^sub>I `  \<langle>f\<^sub>I ` x, f\<^sub>I ` y\<rangle>" by auto
-  }
-  have "f\<^sub>I `\<one> = QuotientGroupRel(R,A,I)``{\<one>}"
-    unfolding qfun_def using lam_funtype lamE Ring_ZF_1_L2(2)
-    by auto
-  then have "f\<^sub>I `\<one> = TheNeutralElement(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R,A,I), M))"
-    using Group_ZF_2_2_L1[OF _ equiv_rel[OF idealAssum]
-          quotientBy_mul_monoid(1)[OF idealAssum]]
-          ringAssum unfolding IsAring_def QuotientBy_def[OF idealAssum]
-    by auto
-  then show "f\<^sub>I ` TheNeutralElement(R, M) = TheNeutralElement(R\<^sub>I, M\<^sub>I)"
-    unfolding quot_def by auto
-qed
+  shows "ringHomomor(f\<^sub>I,R,A,M,R\<^sub>I,A\<^sub>I,M\<^sub>I)"
+  using ringAssum idealAssum ideal_normal_add_subgroup add_group.quotient_map 
+      Ring_ZF_1_L4(3) EquivClass_1_L10 Ring_ZF_1_L2(2) Group_ZF_2_2_L1 equiv_rel 
+      quotientBy_mul_monoid(1) QuotientBy_def
+  unfolding IsAring_def Homomor_def IsMorphism_def ringHomomor_def
+  by simp
 
 text\<open>The quotient map is surjective\<close>
 
 lemma (in ring2) quot_fun:
-  shows "f\<^sub>I\<in>surj(R,R\<^sub>I)" unfolding qfun_def using lam_funtype unfolding quot_def QuotientBy_def[OF idealAssum]
-    quotient_def qrel_def surj_def by auto
+  shows "f\<^sub>I\<in>surj(R,R\<^sub>I)" 
+  using lam_funtype idealAssum QuotientBy_def 
+  unfolding quotient_def surj_def by auto
+
+text\<open>The theorems proven in the  \<open>ring_homo\<close> context are valid in the 
+  \<open>ring_homo\<close> context when applied to the quotient ring as the second (target) 
+  ring and the quotient map as the ring homomorphism.\<close>
 
 sublocale ring2 < quot_homomorphism: ring_homo R A M quot qadd qmul qfun
   _ _ _ _ _ _ _ _ "\<lambda>x y. ideal_radd(x,I,y)" "\<lambda>y. ideal_rmin(I,y)" 
   "\<lambda>x y. ideal_rsub(x,I,y)" "\<lambda>x y. ideal_rmult(x,I,y)"
   "\<zero>\<^sub>I" "\<one>\<^sub>I" "\<two>\<^sub>I" "\<lambda>x. (x\<^sup>2\<^sup>I)"
-  unfolding ring_homo_def using ringAssum quotient_ring.ringAssum
-    quotient_fun_homomor quot_fun unfolding surj_def by auto
+  using ringAssum quotient_ring.ringAssum quotient_fun_homomor
+  unfolding ring_homo_def by simp_all
+
+text\<open>The ideal we divide by is the kernel of the quotient map.\<close>
 
-lemma (in ring2) quotient_kernel:
+lemma (in ring2) quotient_kernel: 
   shows "quot_homomorphism.kernel = I"
 proof
-  {
-    fix t assume t:"t\<in>quot_homomorphism.kernel"
-    then have t:"f\<^sub>I`t = \<zero>\<^sub>I" "t\<in>R" using quot_homomorphism.image_kernel
-      func1_1_L15[OF surj_is_fun[OF quot_fun]] by auto
-    then have "r\<^sub>I``{t} = \<zero>\<^sub>I" using beta by auto
-    then have "t\<in>I" using add_group.Group_ZF_2_4_L5E[OF
-      ideal_normal_add_subgroup[OF idealAssum] t(2)]
-      neutral_quotient[OF idealAssum] unfolding
-      ideal_rzero_def QuotientBy_def[OF idealAssum]
-      by auto
-  }
-  then show "quot_homomorphism.kernel \<subseteq> I" by auto
-  {
-    fix t assume t:"t\<in>I"
-    then have tt:"t\<in>R" using ideal_dest_subset idealAssum by auto
-    then have "r\<^sub>I``{t} = \<zero>\<^sub>I" using add_group.Group_ZF_2_4_L5E[OF
-      ideal_normal_add_subgroup[OF idealAssum] tt] t
-      neutral_quotient[OF idealAssum] unfolding
-      ideal_rzero_def QuotientBy_def[OF idealAssum]
-      by auto
-    then have "f\<^sub>I`t = \<zero>\<^sub>I" using beta tt by auto
-    with tt have "t\<in>f\<^sub>I-``{\<zero>\<^sub>I}" using func1_1_L15
-      surj_is_fun quot_fun by auto
-  }
-  then show "I \<subseteq> quot_homomorphism.kernel" by auto
+  from idealAssum show "quot_homomorphism.kernel \<subseteq> I"
+    using add_group.Group_ZF_2_4_L5E ideal_normal_add_subgroup
+        neutral_quotient QuotientBy_def 
+        quot_homomorphism.image_kernel func1_1_L15
+    unfolding  ideal_rzero_def QuotientBy_def by auto  
+  { fix t assume "t\<in>I"
+    then have "t\<in>R" using ideal_dest_subset idealAssum by auto
+    with idealAssum \<open>t\<in>I\<close> have "t \<in> f\<^sub>I-``{\<zero>\<^sub>I}"
+      using add_group.Group_ZF_2_4_L5E ideal_normal_add_subgroup
+        neutral_quotient QuotientBy_def func1_1_L15 surj_is_fun
+      unfolding ideal_rzero_def by auto          
+  } thus "I \<subseteq> quot_homomorphism.kernel" by blast
 qed
-  
+
+text\<open>The theorems proven in the \<open>ring0\<close> context are valid in the 
+  \<open>ring 2\<close> context when applied to the quotient ring.\<close>
+
 sublocale ring2 < quotient_ring: ring0 quot qadd qmul
   "\<lambda>x y. ideal_radd(x,I,y)" "\<lambda>y. ideal_rmin(I,y)" 
   "\<lambda>x y. ideal_rsub(x,I,y)" "\<lambda>x y. ideal_rmult(x,I,y)"
-  "\<zero>\<^sub>I" "\<one>\<^sub>I" "\<two>\<^sub>I" "\<lambda>x. (x\<^sup>2\<^sup>I)" unfolding ring0_def quot_def
-  using quotientBy_is_ring[OF idealAssum] apply simp
-  unfolding ideal_radd_def ideal_rmin_def
-            ideal_rsub_def ideal_rmult_def
-         ideal_rzero_def ideal_rone_def
-         ideal_rtwo_def ideal_rsqr_def apply auto
-  using neutral_quotient[OF idealAssum] apply simp
-  using one_quotient[OF idealAssum] apply simp
-  using two_quotient[OF idealAssum] by simp
-
-sublocale ring2 < quot_homomorphism: ring_homo R A M quot qadd qmul qfun
-  _ _ _ _ _ _ _ _ "\<lambda>x y. ideal_radd(x,I,y)" "\<lambda>y. ideal_rmin(I,y)" 
-  "\<lambda>x y. ideal_rsub(x,I,y)" "\<lambda>x y. ideal_rmult(x,I,y)"
-  "\<zero>\<^sub>I" "\<one>\<^sub>I" "\<two>\<^sub>I" "\<lambda>x. (x\<^sup>2\<^sup>I)"
-  unfolding ring_homo_def using ringAssum quotient_ring.ringAssum
-    quotient_fun_homomor quot_fun unfolding surj_def by auto
+  "\<zero>\<^sub>I" "\<one>\<^sub>I" "\<two>\<^sub>I" "\<lambda>x. (x\<^sup>2\<^sup>I)" 
+  using idealAssum quotientBy_is_ring neutral_quotient
+    one_quotient two_quotient 
+  unfolding ring0_def by simp_all
+
+text\<open>If an ideal $I$ is a subset of the kernel of the homomorphism
+  then the image of the ideal generated by $I\cup J$, where $J$ is another ideal,
+  is the same as the image of $J$. Note that \<open>J+\<^sub>II\<close> notation means
+  the ideal generated by the union of ideals $J$ and $J$, see the definitions
+  of \<open>sumIdeal\<close> and \<open>generatedIdeal\<close> in the \<open>Ring_ZF_2\<close> theory, and also
+  corollary \<open>sum_ideals_is_sum_elements\<close> for an alternative definition.  \<close>
 
 theorem (in ring_homo) kernel_empty_image:
   assumes "J\<triangleleft>R" "I \<subseteq> ker" "I\<triangleleft>R"
-  shows "f``(J+\<^sub>II) = f``J" "f``(I+\<^sub>IJ) = f``J"
+  shows "f``(J+\<^sub>II) = f``(J)" "f``(I+\<^sub>IJ) = f``(J)"
 proof-
-  have sub:"J+\<^sub>II \<subseteq> R" using assms
-    origin_ring.sum_ideals_is_ideal[THEN origin_ring.ideal_dest_subset]
-    origin_ring.ideal_dest_subset by auto
-  {
-    fix t assume "t\<in>f``(J+\<^sub>II)"
-    then obtain q where q:"q\<in>J+\<^sub>II" "t=f`q"
-      using func_imagedef fun sub(1) by auto
-    from q(1) have "q\<in>A``(J\<times>I)" "J\<times>I \<subseteq> R\<times>R" 
-      using origin_ring.sum_ideals_is_sum_elements
-      assms(1,3) origin_ring.ideal_dest_subset by auto
-    then obtain qj qi where qji:"qj\<in>J" "qi\<in>I"
-      "q=qj\<ra>\<^sub>Rqi" using func_imagedef[of A "R\<times>R" R]
-      origin_ring.add_group.groupAssum unfolding IsAgroup_def
-      IsAmonoid_def IsAssociative_def by auto
-    from qji(3) have "f`q = f`(qj\<ra>\<^sub>Rqi)" by auto
-    with qji(1,2) assms(1,3) have "(f`q) = ((f`qj)\<ra>\<^sub>S(f`qi))"
-      using homomor_dest_add[of qj qi] origin_ring.ideal_dest_subset
-      by auto
-    moreover from qji(2) assms(2) have "qi\<in>ker" by auto
-    ultimately have "f ` q = ((f ` qj)\<ra>\<^sub>S\<zero>\<^sub>S)" using image_kernel
-      by auto
-    then have "f ` qj \<in>S \<Longrightarrow> f ` q = (f ` qj)"
-      using target_ring.Ring_ZF_1_L3(3) by auto
-    moreover have "qj\<in>R" using assms qji(1)
+  from assms(1,3) have "J+\<^sub>II \<subseteq> R" 
+    using origin_ring.sum_ideals_is_ideal 
       origin_ring.ideal_dest_subset by auto
-    then have "f ` qj \<in>S" using apply_type[OF fun]
-      by auto
-    ultimately have "f ` q = (f ` qj)" by auto
-    with q(2) have "t = f` qj" by auto
-    then have "t\<in> f``J" using qji(1) func_imagedef
-      fun assms origin_ring.ideal_dest_subset by auto
-  }
-  then have "f `` (J +\<^sub>I I) \<subseteq> f `` J" by auto
-  moreover
-  {
-    fix t assume t:"t\<in>f``J"
-    then obtain q where q:"q\<in>J" "t=f`q"
-      using func_imagedef fun
-      assms(1) origin_ring.ideal_dest_subset by auto
-    from q(1) have "q\<in>J\<union>I" by auto moreover
-    have "J\<union>I \<subseteq> R" using assms(1,3) origin_ring.ideal_dest_subset by auto
-    ultimately have "q\<in>\<langle>J\<union>I\<rangle>\<^sub>I" using origin_ring.generated_ideal_contains_set by auto
-    then have "q\<in>J+\<^sub>II" unfolding origin_ring.sumIdeal_def[OF assms(1,3)].
-    with q(2) have "t\<in>f``(J+\<^sub>II)" using func_imagedef
-      fun sub by auto
-  }
-  then have "f``J \<subseteq> f `` (J +\<^sub>I I)" by auto
-  ultimately show "f `` (J +\<^sub>I I) = f``J" "f `` (I +\<^sub>I J) = f``J"
-    using origin_ring.sum_ideals_commute assms(1,3) by auto
+  show "f``(J+\<^sub>II) = f``(J)"
+  proof
+    { fix t assume "t\<in>f``(J+\<^sub>II)"
+      with \<open>J+\<^sub>II \<subseteq> R\<close> obtain q where q: "q \<in> J+\<^sub>II" "t=f`(q)"
+        using func_imagedef f_is_fun by auto
+      with assms(1,3) \<open>q \<in> J+\<^sub>II\<close> have "q\<in>A``(J\<times>I)" "J\<times>I \<subseteq> R\<times>R" 
+        using origin_ring.sum_ideals_is_sum_elements
+        assms(1,3) origin_ring.ideal_dest_subset by auto
+      from origin_ring.add_group.groupAssum \<open>J\<times>I \<subseteq> R\<times>R\<close>
+      have "A``(J\<times>I) = {A`(p). p\<in>J\<times>I}"
+        unfolding IsAgroup_def IsAmonoid_def IsAssociative_def
+        using func_imagedef by auto
+      with \<open>q\<in>A``(J\<times>I)\<close> obtain q\<^sub>j q\<^sub>i where "q\<^sub>j\<in>J" "q\<^sub>i\<in>I" "q=q\<^sub>j\<ra>\<^sub>Rq\<^sub>i" 
+        by auto
+      with assms have "f`(q) = (f`(q\<^sub>j)) \<ra>\<^sub>S \<zero>\<^sub>S"
+        using homomor_dest_add origin_ring.ideal_dest_subset image_kernel
+        by blast
+      moreover from assms(1) \<open>q\<^sub>j\<in>J\<close> have "f`(q\<^sub>j) \<in> S"
+        using origin_ring.ideal_dest_subset f_is_fun apply_funtype by blast
+      ultimately have "f`(q) = f`(q\<^sub>j)" using target_ring.Ring_ZF_1_L3(3) 
+        by auto    
+      with assms \<open>t=f`(q)\<close> \<open>q\<^sub>j\<in>J\<close> have "t \<in> f``(J)"
+        using func_imagedef f_is_fun origin_ring.ideal_dest_subset by auto    
+    } thus "f``(J+\<^sub>II) \<subseteq> f``(J)" by blast
+    { fix t assume "t\<in>f``(J)"
+      with assms(1) obtain q where q:"q\<in>J" "t=f`(q)"
+        using func_imagedef f_is_fun origin_ring.ideal_dest_subset 
+        by auto
+      from \<open>q\<in>J\<close> have "q\<in>J\<union>I" by auto 
+      moreover from assms(1,3) have "J\<union>I \<subseteq> R" 
+        using origin_ring.ideal_dest_subset by auto
+      ultimately have "q\<in>\<langle>J\<union>I\<rangle>\<^sub>I" using origin_ring.generated_ideal_contains_set 
+        by auto
+      with assms(1,3) \<open>J+\<^sub>II \<subseteq> R\<close> \<open>t=f`(q)\<close> have "t\<in>f``(J+\<^sub>II)"
+        using origin_ring.sumIdeal_def f_is_fun func_imagedef by auto
+    } thus "f``(J) \<subseteq> f``(J+\<^sub>II)" by auto
+  qed
+  with assms(1,3) show "f ``(I+\<^sub>IJ) = f``(J)"
+    using origin_ring.sum_ideals_commute by auto
 qed
 
 subsection\<open>Quotient ideals\<close>
 
+text\<open>If we have an ideal $J$ in a ring $R$, and another ideal $I$ contained in J, 
+  then we can form the quotient ideal J/I whose elements are of the form $a + I$
+  where $a$ is an element of $J$.\<close>
+
 text\<open>The preimage of an ideal is an ideal, so it applies to the
-quotient map; but the preimage ideal contains the quotient ideal.\<close>
+  quotient map; but the preimage ideal contains the quotient ideal.\<close>
 
 lemma (in ring2) ideal_quot_preimage:
   assumes "J\<triangleleft>R\<^sub>I"
-  shows "(f\<^sub>I-``J) \<triangleleft>R" "I \<subseteq> f\<^sub>I-``J"
-proof-
-  from quot_homomorphism.preimage_ideal[OF assms]
-  show "(f\<^sub>I-``J) \<triangleleft>R" by auto
-  {
-    fix x assume x:"x\<in>I"
-    with quot_fun have "f\<^sub>I`x = r\<^sub>I``{x}"
-      using lamI[of x R] ideal_dest_subset[OF idealAssum]
-      apply_equality[of x "r\<^sub>I``{x}" "f\<^sub>I"] unfolding qfun_def
-      by auto
-    then have "f\<^sub>I`x = \<zero>\<^sub>I" using add_group.Group_ZF_2_4_L5E[OF
-          ideal_normal_add_subgroup[OF idealAssum], of x
-          "r\<^sub>I" "\<zero>\<^sub>I"] x ideal_dest_subset[OF idealAssum]
-      unfolding qrel_def ideal_rzero_def using
-        Group_ZF_2_4_L5B[OF _ ideal_normal_add_subgroup[OF idealAssum]]
-      using ringAssum unfolding IsAring_def by auto
-    then have "f\<^sub>I`x \<in> J" using quotient_ring.ideal_dest_zero
-      assms by auto
-    then have "x\<in>f\<^sub>I-``J" using x ideal_dest_subset[OF idealAssum]
-      quot_fun func1_1_L15 by auto
-  }
-  then show "I \<subseteq> f\<^sub>I-``J" by auto
+  shows "(f\<^sub>I-``(J)) \<triangleleft>R" "I \<subseteq> f\<^sub>I-``(J)"
+proof -
+  from assms quot_homomorphism.preimage_ideal show "(f\<^sub>I-``(J)) \<triangleleft>R" 
+    by simp
+  { fix x assume x: "x\<in>I"
+    with idealAssum have "x\<in>R" using ideal_dest_subset by auto
+    from assms \<open>x\<in>I\<close> have "f\<^sub>I`(x) \<in> J"
+      using quotient_kernel quot_homomorphism.image_kernel 
+        quotient_ring.ideal_dest_zero by simp
+    with \<open>x\<in>R\<close> have "x\<in>f\<^sub>I-``(J)" using quot_homomorphism.f_is_fun func1_1_L15 
+      by simp
+  } thus "I \<subseteq> f\<^sub>I-``(J)" by auto
 qed
 
 text\<open>Since the map is surjective, the image is also an ideal\<close>
 
 lemma (in ring_homo) image_ideal_surj:
   assumes "J\<triangleleft>R\<^sub>o" "f\<in>surj(R,S)"
-  shows "(f``J) \<triangleleft>R\<^sub>t" unfolding target_ring.Ideal_def
-proof
-  show "IsAsubgroup(f``J,U)"
-  proof (rule image_subgroup)
-    show "IsAgroup(R,A)" using origin_ring.ringAssum unfolding IsAring_def by auto
-    show "f : R \<rightarrow> S" using fun .
-    show "IsAsubgroup(J,A)" using assms unfolding origin_ring.Ideal_def by auto
-    show "Homomor(f,R,A,S,U)" using homomorphism
-      unfolding ringHomomor_def[OF origin target]
+  shows "(f``(J)) \<triangleleft>R\<^sub>t" 
+proof -
+  from assms homomorphism target_ring.ringAssum origin_ring.ringAssum 
+  have "IsAsubgroup(f``(J),U)"
+    using ringHomHom(1) image_subgroup f_is_fun
+    unfolding IsAring_def origin_ring.Ideal_def by blast
+  moreover
+  { fix x y assume "x\<in>f``(J)" "y\<in>S"
+    from assms(1) \<open>x\<in>f``(J)\<close> obtain j where "x=f`(j)" "j\<in>J" 
+      using func_imagedef f_is_fun origin_ring.ideal_dest_subset 
       by auto
-    show "IsAgroup(S,U)" using target_ring.ringAssum
-      unfolding IsAring_def by auto
-  qed
-  {
-    fix x y assume xy:"x\<in>f``J" "y\<in>S"
-    from xy(1) obtain j where x:"x=f`j" "j\<in>J" using func_imagedef
-      fun origin_ring.ideal_dest_subset[OF assms(1)] by auto
-    from xy(2) have "y\<in>f``R" using assms(2) surj_range_image_domain
+    from assms \<open>y\<in>S\<close> \<open>j\<in>J\<close> have "j\<in>R" and "y\<in>f``(R)"
+      using origin_ring.ideal_dest_subset surj_range_image_domain
       by auto
-    then obtain s where y:"y=f`s" "s\<in>R" using func_imagedef
-      origin_ring.ideal_dest_subset[OF assms(1)] 
-      fun by auto
-    from x(1) y(1) have "V`\<langle>x,y\<rangle> = V`\<langle>f`j,f`s\<rangle>"
-      "V`\<langle>y,x\<rangle> = V`\<langle>f`s,f`j\<rangle>" by auto
-    then have "V`\<langle>x,y\<rangle> = f`(M`\<langle>j,s\<rangle>)" "V`\<langle>y,x\<rangle> = f`(M`\<langle>s,j\<rangle>)"
-      using homomor_dest_mult[of s j]
-        homomor_dest_mult[of j s]
-        x(2) y(2) origin_ring.ideal_dest_subset[OF assms(1)] by auto
-    moreover have "j\<cdot>\<^sub>Rs\<in>J" "s\<cdot>\<^sub>Rj\<in>J" using origin_ring.ideal_dest_mult[OF assms(1)]
-      x(2) y(2) by auto
-    ultimately have "(x\<cdot>\<^sub>Sy)\<in>f``J" "(y\<cdot>\<^sub>Sx)\<in>f``J"
-      using func_imagedef fun origin_ring.ideal_dest_subset[OF assms(1)]
+    with assms(1) obtain s where "y=f`(s)" "s\<in>R" 
+      using func_imagedef origin_ring.ideal_dest_subset f_is_fun 
       by auto
-  }
-  then show "\<forall>x\<in>f `` J. \<forall>y\<in>S. (y\<cdot>\<^sub>Sx) \<in> f `` J \<and> (x\<cdot>\<^sub>Sy) \<in> f `` J"
+    with assms(1) \<open>j\<in>R\<close> \<open>x=f`(j)\<close> \<open>x\<in>f``(J)\<close> have 
+      "V`\<langle>x,y\<rangle> = f`(M`\<langle>j,s\<rangle>)" and "V`\<langle>y,x\<rangle> = f`(M`\<langle>s,j\<rangle>)"
+      using homomor_dest_mult origin_ring.ideal_dest_subset by auto
+    with assms(1) \<open>j\<in>J\<close> \<open>s\<in>R\<close> have "(x\<cdot>\<^sub>Sy)\<in>f``(J)" and "(y\<cdot>\<^sub>Sx)\<in>f``J"
+      using origin_ring.ideal_dest_mult func_imagedef f_is_fun 
+        origin_ring.ideal_dest_subset by auto
+  } hence "\<forall>x\<in>f``(J). \<forall>y\<in>S. (y\<cdot>\<^sub>Sx) \<in> f``(J) \<and> (x\<cdot>\<^sub>Sy) \<in> f``(J)"
     by auto
+  ultimately show ?thesis unfolding target_ring.Ideal_def by simp
 qed
+  
+text\<open>If the homomorphism is a surjection and given two ideals in the target ring 
+  the inverse image of their product ideal is the sum ideal of the product
+  ideal of their inverse images and the kernel of the homomorphism.\<close>
 
 corollary (in ring_homo) prime_ideal_quot:
-  assumes "J\<triangleleft>R\<^sub>t" "K\<triangleleft>R\<^sub>t" "f:surj(R,S)"
-  shows "f-``(target_ring.productIdeal(J, K)) = origin_ring.sumIdeal(origin_ring.productIdeal((f-``J),(f-``K)), ker)"
+  assumes "J\<triangleleft>R\<^sub>t" "K\<triangleleft>R\<^sub>t" "f\<in>surj(R,S)"
+  shows "f-``(target_ring.productIdeal(J, K)) = 
+  origin_ring.sumIdeal(origin_ring.productIdeal((f-``(J)),(f-``(K))), ker)"
 proof
-  let ?P = "origin_ring.sumIdeal(origin_ring.productIdeal((f-``J),(f-``K)), f-``{\<zero>\<^sub>S})"
-  have qRI:"target_ring.productIdeal(J, K)\<triangleleft>R\<^sub>t"
-    using target_ring.product_in_intersection(2)
-    assms by auto
-  from assms(1,2) have ideals:"(f-``J) \<triangleleft>R\<^sub>o" "(f-``K) \<triangleleft>R\<^sub>o"
+  let ?P = "origin_ring.sumIdeal(origin_ring.productIdeal((f-``(J)),(f-``(K))), f-``{\<zero>\<^sub>S})"
+  let ?Q = "target_ring.productIdeal(J, K)"
+  from assms(1,2) have ideals: "(f-``(J)) \<triangleleft>R\<^sub>o" "(f-``(K)) \<triangleleft>R\<^sub>o"
     using preimage_ideal by auto
-  then have idealJK:"((f-``J) \<cdot>\<^sub>I (f-``K)) \<triangleleft>R\<^sub>o"
+  then have idealJK: "((f-``(J))\<cdot>\<^sub>I(f-``(K))) \<triangleleft>R\<^sub>o"
     using origin_ring.product_in_intersection(2) by auto
-  have idealSum:"?P \<triangleleft>R"
-    using origin_ring.sum_ideals_is_sum_elements[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]]
-      origin_ring.sum_elements_is_ideal[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]]
-    by auto
-  then have ideal:"(f``?P) \<triangleleft>R\<^sub>t"
-    using image_ideal_surj assms(3)
+  then have "?P \<triangleleft>R\<^sub>o" and "?P\<subseteq>R" 
+    using kernel_ideal origin_ring.sum_ideals_is_ideal 
+      origin_ring.ideal_dest_subset by simp_all
+  with assms(3) have  "(f``(?P)) \<triangleleft>R\<^sub>t" using  image_ideal_surj
+    by simp
+  let ?X = "((f-``(J)) \<cdot>\<^sub>I (f-``(K)))\<union>(f-``{\<zero>\<^sub>S})"
+  from assms(3) idealJK have "?X \<subseteq> R" 
+      using func1_1_L6A surj_is_fun origin_ring.ideal_dest_subset 
+      by blast
+  with idealJK have "?X \<subseteq> ?P"
+      using kernel_ideal origin_ring.sumIdeal_def 
+        origin_ring.generated_ideal_contains_set by simp
+  { fix t assume "t\<in>V ``(J\<times>K)"
+    moreover from assms have "J\<times>K \<subseteq> S\<times>S" 
+      using target_ring.ideal_dest_subset by blast 
+    ultimately obtain j k where "j\<in>J" "k\<in>K" "t=V`\<langle>j,k\<rangle>"
+      using func_imagedef AMUV_are_ops(4) by auto
+    from assms(1) \<open>j\<in>J\<close> have "j\<in>S" 
+      using target_ring.ideal_dest_subset by blast
+    with assms(3) obtain j\<^sub>0 where  "j\<^sub>0\<in>R" "f`(j\<^sub>0) = j"
+      unfolding surj_def by auto
+    with assms(2,3) \<open>k\<in>K\<close> obtain k\<^sub>0 where "k\<^sub>0\<in>R" "f`(k\<^sub>0) = k"
+      using target_ring.ideal_dest_subset unfolding surj_def 
+      by blast
+    with \<open>t=V`\<langle>j,k\<rangle>\<close> \<open>f`(j\<^sub>0) = j\<close>  \<open>j\<^sub>0\<in>R\<close> have "t=f`(M`\<langle>j\<^sub>0,k\<^sub>0\<rangle>)" 
+      using homomor_dest_mult by simp
+    from assms(3) have "(f-``(J))\<times>(f-``(K)) \<subseteq> R\<times>R"
+      using func1_1_L6A  f_is_fun by blast
+    moreover from assms(3) \<open>j\<^sub>0\<in>R\<close> \<open>f`(j\<^sub>0) = j\<close> \<open>j\<in>J\<close> \<open>k\<in>K\<close> \<open>k\<^sub>0\<in>R\<close> \<open>f`(k\<^sub>0) = k\<close>
+      have "\<langle>j\<^sub>0,k\<^sub>0\<rangle> \<in> (f-``J)\<times>(f-``K)"
+      using func1_1_L15 unfolding surj_def by auto
+    ultimately have "M`\<langle>j\<^sub>0,k\<^sub>0\<rangle> \<in> M``((f-``(J))\<times>(f-``(K)))"
+      using AMUV_are_ops func_imagedef by auto
+    with ideals \<open>?X \<subseteq> ?P\<close> have "M`\<langle>j\<^sub>0,k\<^sub>0\<rangle> \<in> ?P"
+      using origin_ring.product_in_intersection(3) 
+      by blast
+    with \<open>?P\<subseteq>R\<close> \<open>t=f`(M`\<langle>j\<^sub>0,k\<^sub>0\<rangle>)\<close> have "t\<in>(f``(?P))"
+      using f_is_fun func1_1_L15D by simp
+  } hence "V``(J \<times> K) \<subseteq> f``(?P)" by blast
+  with assms(1,2) \<open>(f``(?P)) \<triangleleft>R\<^sub>t\<close> have "?Q\<subseteq>f``(?P)"
+    using target_ring.generated_ideal_small target_ring.productIdeal_def
+    by simp
+  then have R: "f-``(?Q) \<subseteq> f-``(f``?P)"
+    unfolding vimage_def by blast
+  from \<open>?X \<subseteq> ?P\<close> \<open>?P \<triangleleft>R\<^sub>o\<close> \<open>?P\<subseteq>R\<close> have P_ideal: "?P \<in> {N\<in>\<I>. f-``{\<zero>\<^sub>S} \<subseteq> N}" 
     by auto
-  {
-    fix t assume "t\<in>V ``(J\<times>K)" moreover
-    have "J\<times>K \<subseteq> S\<times>S" using assms
-      target_ring.ideal_dest_subset by auto moreover
-    have "V:S\<times>S \<rightarrow> S" using target_ring.ringAssum
-      unfolding IsAring_def IsAmonoid_def
-      IsAssociative_def by auto
-    ultimately obtain j k where jk:"j\<in>J" "k\<in>K" "t=V`\<langle>j,k\<rangle>"
-      using func_imagedef by auto
-    from jk(1) have "j\<in>S" using assms(1)
-      target_ring.ideal_dest_subset by auto
-    then obtain jj where jj:"jj\<in>R" "f`jj = j" using
-      assms(3) unfolding surj_def by auto
-    from jk(2) have "k\<in>S" using assms(2)
-      target_ring.ideal_dest_subset by auto
-    then obtain kk where kk:"kk\<in>R" "f`kk = k" using
-      assms(3) unfolding surj_def by auto
-    from jk(3) jj(2) kk(2)
-    have "t=V`\<langle>f`jj,f`kk\<rangle>" by auto
-    then have t:"t=f`(M`\<langle>jj,kk\<rangle>)" using
-      homomor_dest_mult[OF jj(1) kk(1)] by auto
-    have "f-``J \<subseteq> R" using assms(3)
-      using func1_1_L6A[OF surj_is_fun] by auto moreover
-    have "f-``K \<subseteq> R" using assms(3)
-      using func1_1_L6A[OF surj_is_fun] by auto ultimately
-    have sub:"(f-``J)\<times>(f-``K) \<subseteq> R\<times>R" by auto moreover
-    have "M:R\<times>R \<rightarrow> R" using origin_ring.ringAssum
-      unfolding IsAring_def IsAmonoid_def
-      IsAssociative_def by auto moreover
-    {
-      from jj have "jj\<in>f-``J" using func1_1_L15
-        assms(3) jk(1) unfolding surj_def by auto moreover
-      from kk have "kk\<in>f-``K" using func1_1_L15
-        assms(3) jk(2) unfolding surj_def by auto ultimately
-      have "\<langle>jj,kk\<rangle>\<in>(f-``J)\<times>(f-``K)" by auto
-    } ultimately
-    have "M`\<langle>jj,kk\<rangle> \<in> M``((f-``J)\<times>(f-``K))"
-      using func_imagedef by auto
-    then have "M`\<langle>jj,kk\<rangle> \<in> (f-``J) \<cdot>\<^sub>I (f-``K)"
-      using preimage_ideal
-      assms origin_ring.product_in_intersection(3) by blast
-    then have "M`\<langle>jj,kk\<rangle> \<in> ((f-``J) \<cdot>\<^sub>I (f-``K))\<union>(f-``{\<zero>\<^sub>S})"
-      by auto moreover
-    have "((f-``J) \<cdot>\<^sub>I (f -`` K))\<union>(f-``{\<zero>\<^sub>S})\<subseteq>R" using 
-      func1_1_L6A[OF surj_is_fun[OF assms(3)]]
-      origin_ring.ideal_dest_subset[OF idealJK] by auto
-    ultimately have "M`\<langle>jj,kk\<rangle> \<in> ?P"
-      unfolding origin_ring.sumIdeal_def[OF idealJK 
-          preimage_ideal(1)[OF target_ring.zero_ideal]]
-      using origin_ring.generated_ideal_contains_set[of
-          "((f-`` J) \<cdot>\<^sub>I (f-`` K)) \<union> (f-``{\<zero>\<^sub>S})"] by blast
-    then have "f`(M`\<langle>jj,kk\<rangle>) \<in> f``?P"
-      using func1_1_L15D[OF surj_is_fun[OF assms(3)] _
-       idealSum[THEN origin_ring.ideal_dest_subset]] by auto
-    moreover note t ultimately
-    have "t\<in>(f``?P)"
+  { fix t assume "t\<in>f-``(f``(?P))"
+    then have "f`(t) \<in> f``(?P)" and "t\<in>R" 
+      using func1_1_L15 f_is_fun by simp_all
+    with P_ideal obtain s where "f`(t) = f`(s)" "s\<in>?P" 
+      using func_imagedef f_is_fun by auto
+    from P_ideal \<open>s\<in>?P\<close> have "s\<in>R" by blast
+    from \<open>t\<in>R\<close> \<open>s\<in>R\<close> \<open>f`(t) = f`(s)\<close> have "f`(t\<rs>\<^sub>Rs) = \<zero>\<^sub>S"
+      using f_is_fun apply_funtype target_ring.Ring_ZF_1_L3(7) 
+        homomor_dest_subs by simp
+    with \<open>t\<in>R\<close> \<open>s\<in>R\<close> \<open>?X\<subseteq>?P\<close> have "t\<rs>\<^sub>Rs \<in> ?P"
+      using origin_ring.Ring_ZF_1_L4(2) func1_1_L15 f_is_fun 
       by auto
-  }
-  then have "V `` (J \<times> K) \<subseteq> f``?P" by blast
-  then have "target_ring.generatedIdeal(V `` (J \<times> K)) \<subseteq> f``?P"
-    using ideal target_ring.generated_ideal_small by auto
-  then have "target_ring.productIdeal(J, K) \<subseteq> f``(?P)"
-    unfolding target_ring.productIdeal_def[OF assms(1,2)].
-  then have R:"f-``target_ring.productIdeal(J, K) \<subseteq> f-``(f``?P)"
-    unfolding vimage_def by blast
-  have "((f-``J) \<cdot>\<^sub>I (f-``K)) \<union> (f -`` {\<zero>\<^sub>S}) \<subseteq> R" using idealJK
-    origin_ring.ideal_dest_subset func1_1_L6A[OF surj_is_fun] 
-    assms(3) by blast
-  then have p:"(f -`` {\<zero>\<^sub>S}) \<subseteq> ?P"
-    unfolding origin_ring.sumIdeal_def[OF idealJK 
-        preimage_ideal(1)[OF target_ring.zero_ideal]]
-    using origin_ring.generated_ideal_contains_set 
-      by blast
-    moreover 
-  from idealSum origin_ring.ideal_dest_subset
-    have "?P \<subseteq>R" by auto
-  moreover note idealSum
-  ultimately have P_ideal:"?P \<in> {N\<in>\<I>. f-``{\<zero>\<^sub>S} \<subseteq> N}"
+    with P_ideal \<open>s\<in>?P\<close> have "s\<ra>\<^sub>R(t\<rs>\<^sub>Rs) \<in> ?P" 
+      using origin_ring.ideal_dest_sum by auto
+    with \<open>t\<in>R\<close> \<open>s\<in>R\<close> have "t\<in>?P" 
+      using origin_ring.Ring_ZF_2_L1A(5) by auto
+  } with R show "f-``(?Q) \<subseteq> ?P" 
     by auto
-  have P:"f``?P \<subseteq> S"
-    using ideal P_ideal
-    assms(3) target_ring.ideal_dest_subset by auto
-  {
-    fix t assume "t\<in>f-``(f``?P)"
-    then have t:"f`t\<in>f``?P" "t\<in>R" using func1_1_L15
-      surj_is_fun[OF assms(3)] by auto
-    then obtain s where s:"f`t = f`s" "s\<in>?P" using
-      func_imagedef[OF surj_is_fun[OF assms(3)]] P_ideal by auto
-    from s(2) have ss:"s\<in>R" using P_ideal by auto
-    from s(1) have "(f`t) \<rs>\<^sub>S (f`s) = \<zero>\<^sub>S" using
-      target_ring.Ring_ZF_1_L3(7)[OF apply_type[OF surj_is_fun[OF assms(3)]
-      t(2)]] by auto
-    then have "f`(t\<rs>\<^sub>Rs) = \<zero>\<^sub>S" using homomor_dest_subs
-      t(2) ss by auto moreover
-    from t(2) ss have "t\<rs>\<^sub>Rs \<in>R" using origin_ring.Ring_ZF_1_L4(2) by auto
-    ultimately have "t\<rs>\<^sub>Rs \<in> f-``{\<zero>\<^sub>S}" using func1_1_L15
-      surj_is_fun[OF assms(3)] by auto
-    then have "t\<rs>\<^sub>Rs \<in> ?P" using p by auto
-    then have "s\<ra>\<^sub>R(t\<rs>\<^sub>Rs) \<in> ?P" using origin_ring.ideal_dest_sum
-      P_ideal s(2) by auto
-    then have "t\<in>?P" using origin_ring.Ring_ZF_2_L1A(5)
-      ss t(2) by auto
-  }
-  then have "f-``(f``?P) \<subseteq> ?P" by auto
-  with R show "f-``target_ring.productIdeal(J, K) \<subseteq> ?P" by auto
-  {
-    fix t assume as:"t\<in>M``((f-``J)\<times>(f-``K))"
-    moreover have "(f-``J)\<times>(f-``K) \<subseteq> R\<times>R" using func1_1_L15[OF surj_is_fun[OF assms(3)]] by auto
-    ultimately obtain tj tk where jk:"t=tj\<cdot>\<^sub>Rtk" "tj\<in>f-``J" "tk\<in>f-``K"
-      using func_imagedef[of M "R\<times>R" R] origin_ring.ringAssum unfolding IsAring_def IsAmonoid_def
-      IsAssociative_def by auto
-    from as have tR:"t\<in>R" using func1_1_L6(2)[of M "R\<times>R" R]
-      origin_ring.ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def
+  { fix t assume as: "t \<in> M``((f-``(J))\<times>(f-``(K)))"
+    have "(f-``(J))\<times>(f-``(K)) \<subseteq> R\<times>R" 
+      using func1_1_L15 f_is_fun by auto
+    with as obtain t\<^sub>j t\<^sub>k where 
+      jk: "t=t\<^sub>j\<cdot>\<^sub>Rt\<^sub>k" "t\<^sub>j\<in>f-``(J)" "t\<^sub>k\<in>f-``(K)"
+      using AMUV_are_ops(2) func_imagedef IsAssociative_def 
       by auto
-    from jk(2) have j:"tj\<in>R" "f`tj \<in>J" using func1_1_L15 surj_is_fun[OF
-      assms(3)] by auto
-    from jk(3) have k:"tk\<in>R" "f`tk \<in>K" using func1_1_L15 surj_is_fun[OF
-      assms(3)] by auto
-    from jk(1) have "f`t = f`(tj\<cdot>\<^sub>Rtk)" by auto
-    then have ft:"f`t = ((f`tj)\<cdot>\<^sub>S(f`tk))" using homomor_dest_mult
-      using j(1) k(1) by auto
-    from j(2) k(2) have "\<langle>f`tj,f`tk\<rangle>\<in>J\<times>K" by auto
-    moreover have "V:S\<times>S\<rightarrow>S" using target_ring.ringAssum unfolding IsAring_def
-      IsAmonoid_def IsAssociative_def by auto
-    moreover have "J\<times>K \<subseteq> S\<times>S" using assms using target_ring.ideal_dest_subset
+    from as have "t\<in>R" using AMUV_are_ops(2) func1_1_L6(2) by blast
+    from jk(2,3) have "t\<^sub>j\<in>R" "f`(t\<^sub>j)\<in>J" and "t\<^sub>k\<in>R" "f`(t\<^sub>k)\<in>K" 
+      using func1_1_L15 f_is_fun by simp_all
+    from jk(1) \<open>t\<^sub>j\<in>R\<close> \<open>t\<^sub>k\<in>R\<close> have ft: "f`(t) = ((f`(t\<^sub>j))\<cdot>\<^sub>S(f`(t\<^sub>k)))"
+      using homomor_dest_mult by simp
+    from \<open>f`(t\<^sub>j)\<in>J\<close> \<open>f`(t\<^sub>k) \<in>K\<close> have "\<langle>f`(t\<^sub>j),f`(t\<^sub>k)\<rangle> \<in> J\<times>K" 
+      by simp
+    moreover from assms have "V:S\<times>S\<rightarrow>S" and "J\<times>K \<subseteq> S\<times>S" 
+      using AMUV_are_ops(4) target_ring.ideal_dest_subset 
       by auto
-    ultimately have "V`\<langle>f ` tj, f ` tk\<rangle> \<in>V``(J\<times>K)"
-      using func_imagedef[of V "S\<times>S" S "J\<times>K"] by force
-    with ft have "f`t\<in>V``(J\<times>K)" by auto
-    then have "f`t\<in>target_ring.productIdeal(J, K)"
-      using target_ring.product_in_intersection(3) assms
-      by blast
-    then have "t\<in>f-``target_ring.productIdeal(J, K)"
-      using func1_1_L15 surj_is_fun[OF assms(3)] tR
-      by auto
-  }
-  then have "M `` (f -`` J \<times> f -`` K) \<subseteq> f -`` target_ring.productIdeal(J, K)" by auto
-  moreover have id:"(f -``target_ring.productIdeal(J, K)) \<triangleleft>R\<^sub>o"
-    apply (rule preimage_ideal) apply (rule target_ring.product_in_intersection(2))
-    using assms(1,2) .
-  ultimately have "(f -`` J) \<cdot>\<^sub>I (f -`` K) \<subseteq> f -``target_ring.productIdeal(J, K)"
-    using origin_ring.generated_ideal_small origin_ring.productIdeal_def[OF ideals]
+    ultimately have "V`\<langle>f`(t\<^sub>j), f`(t\<^sub>k)\<rangle> \<in>V``(J\<times>K)"
+      using func_imagedef by force
+    with assms ft \<open>t\<in>R\<close> have "t \<in> f-``(?Q)"
+      using target_ring.product_in_intersection(3) func1_1_L15 f_is_fun 
+      by auto  
+  } hence "M``(f-``(J)\<times>f-``(K))\<subseteq>f-``(?Q)" 
     by auto
-  moreover have "\<zero>\<^sub>S \<in> target_ring.productIdeal(J, K)"
-    using target_ring.product_in_intersection(2) assms(1,2)
-    target_ring.ideal_dest_zero by auto
-  then have "(f -`` {\<zero>\<^sub>S}) \<subseteq> f -``target_ring.productIdeal(J, K)"
-     by auto
-  ultimately have "((f -`` J) \<cdot>\<^sub>I (f -`` K))\<union>(f -`` {\<zero>\<^sub>S}) \<subseteq> f -``target_ring.productIdeal(J, K)"
+  moreover from assms(1,2) have 
+    id: "(f-``(?Q)) \<triangleleft>R\<^sub>o"
+    using preimage_ideal target_ring.product_in_intersection(2)
+    by simp
+  ultimately have "(f -`` J) \<cdot>\<^sub>I (f -`` K)\<subseteq>f-``(?Q)"
+    using ideals origin_ring.generated_ideal_small origin_ring.productIdeal_def
     by auto
-  then show "((f -`` J) \<cdot>\<^sub>I (f -`` K))+\<^sub>I(f -`` {\<zero>\<^sub>S}) \<subseteq> f -``target_ring.productIdeal(J, K)"
-    using origin_ring.generated_ideal_small id 
-      origin_ring.sumIdeal_def[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]]
+  with assms(1,2) have "?X \<subseteq> f-``(?Q)"
+    using target_ring.product_in_intersection(2) target_ring.ideal_dest_zero 
     by auto
+  with idealJK id show 
+    "((f-``(J))\<cdot>\<^sub>I(f-``(K)))+\<^sub>I(f-``{\<zero>\<^sub>S}) \<subseteq> f-``(?Q)"
+    using origin_ring.generated_ideal_small kernel_ideal origin_ring.sumIdeal_def
+    by simp
 qed
 
+text\<open>If the homomorphism is surjective then the product ideal of ideals $J,K$ 
+  in the target ring is the image of the product ideal (in the source ring) 
+  of the inverse images of $J,K$. \<close>
+
 corollary (in ring_homo) prime_ideal_quot_2:
   assumes "J\<triangleleft>R\<^sub>t" "K\<triangleleft>R\<^sub>t" "f\<in>surj(R,S)"
-  shows "target_ring.productIdeal(J, K) = f``origin_ring.productIdeal((f-`` J), (f-`` K))"
-proof-
-  have "f-`` target_ring.productIdeal(J, K) =
- ((f-`` J) \<cdot>\<^sub>I (f-`` K)) +\<^sub>I (ker)" using prime_ideal_quot assms beta by auto
-  then have "f``(f-`` target_ring.productIdeal(J, K))
-  = f``(((f -`` J) \<cdot>\<^sub>I (f -`` K)) +\<^sub>I (ker))"
-    by auto
-  moreover have "target_ring.productIdeal(J, K)\<triangleleft>R\<^sub>t"
-    using target_ring.product_in_intersection(2)
-    assms(1,2) by auto
-  then have "target_ring.productIdeal(J, K) \<subseteq> S" using
-    target_ring.ideal_dest_subset by auto
-  ultimately have A:"target_ring.productIdeal(J, K) = 
-    f``(((f-`` J) \<cdot>\<^sub>I (f-`` K)) +\<^sub>I(f-``{\<zero>\<^sub>S}))"
-    using surj_image_vimage assms(3) 
-    by auto
-  have idealJK:"((f-``J) \<cdot>\<^sub>I (f-``K)) \<triangleleft>R"
-    using origin_ring.product_in_intersection(2) 
-    preimage_ideal assms(1,2) by auto
-  with A show "target_ring.productIdeal(J, K) = 
-    f``((f-`` J) \<cdot>\<^sub>I (f-`` K))" using kernel_empty_image(1)
-    preimage_ideal[OF target_ring.zero_ideal] by auto
+  shows "target_ring.productIdeal(J, K) = 
+    f``(origin_ring.productIdeal((f-``(J)), (f-``(K))))"      
+proof -
+  from assms have "f``(f-``(target_ring.productIdeal(J, K)))
+      = f``(((f-``(J)) \<cdot>\<^sub>I (f-``(K))) +\<^sub>I (ker))"
+    using prime_ideal_quot by simp
+  with assms show ?thesis
+    using target_ring.product_in_intersection(2) 
+      target_ring.ideal_dest_subset surj_image_vimage
+      origin_ring.product_in_intersection(2) preimage_ideal
+      kernel_empty_image(1) target_ring.zero_ideal
+    by simp
 qed
 
+text\<open>If the homomorphism is surjective and an ideal in the source ring
+  contains the kernel, then the image of that ideal is a prime ideal in the 
+  target ring.\<close>
+
 lemma (in ring_homo) preimage_ideal_prime:
   assumes "J\<triangleleft>\<^sub>pR\<^sub>o" "ker \<subseteq> J" "f\<in>surj(R,S)"
-  shows "(f``J)\<triangleleft>\<^sub>pR\<^sub>t"
-proof-
-  from assms(1,3) have "(f``J)\<triangleleft>R\<^sub>t" using image_ideal_surj
-    unfolding origin_ring.primeIdeal_def by auto moreover
-  from assms(1) have JT:"J \<subseteq> R" "J \<noteq> R" 
+  shows "(f``(J))\<triangleleft>\<^sub>pR\<^sub>t"
+proof -
+  from assms(1) have "J \<subseteq> R" "J \<noteq> R" 
     unfolding origin_ring.primeIdeal_def 
     using origin_ring.ideal_dest_subset by auto
-  {
-    assume full:"f``J = S"
-    from JT obtain t where t:"t\<in>R-J" by auto
-    with assms(3) have "f`t\<in>S" 
-      using apply_type[OF surj_is_fun] by auto
-    with full have "f`t\<in>f``J" by auto
-    with assms(3) JT(1) obtain j where j:"j\<in>J" "f`t= f`j"
-      using func_imagedef[OF surj_is_fun] by auto
-    from j(1) have jt:"j\<in>R" using JT(1) by auto
-    then have fj:"f`j\<in>S" using apply_type assms(3)
-      unfolding surj_def by auto
-    from j(2) have "(f`t)\<rs>\<^sub>S(f`j) = \<zero>\<^sub>S" using
-      target_ring.Ring_ZF_1_L3(7) fj by auto
-    then have "f`(t\<rs>\<^sub>Rj) =\<zero>\<^sub>S" using homomor_dest_subs
-      t jt by auto moreover
-    have "t\<rs>\<^sub>Rj \<in>R" using origin_ring.Ring_ZF_1_L4(2)
-      t jt by auto
-    ultimately have "t\<rs>\<^sub>Rj\<in>f-``{\<zero>\<^sub>S}" using func1_1_L15[OF surj_is_fun]
-      assms(3) by auto
-    with assms(2) have tjJ:"t\<rs>\<^sub>Rj\<in>J" by auto
-    with j(1) have "j\<ra>\<^sub>R(t\<rs>\<^sub>Rj) \<in>J" using assms(1)
+  from assms(1,3) have "(f``(J))\<triangleleft>R\<^sub>t" 
+    using image_ideal_surj  unfolding origin_ring.primeIdeal_def 
+    by auto 
+  moreover 
+  { assume "f``(J) = S"
+    from \<open>J \<subseteq> R\<close> \<open>J \<noteq> R\<close> obtain t where "t\<in>R-J" by auto
+    with assms(3) have "f`(t)\<in>S" 
+      using apply_funtype f_is_fun by auto
+    with assms(3) \<open>J \<subseteq> R\<close> \<open>f``(J) = S\<close> obtain j 
+      where j: "j\<in>J" "f`(t)= f`(j)"
+      using func_imagedef f_is_fun by auto   
+    from \<open>j\<in>J\<close> \<open>J \<subseteq> R\<close> have "j\<in>R" by auto
+    with assms(3) \<open>f`(t)= f`(j)\<close> \<open>t\<in>R-J\<close> have "t\<rs>\<^sub>Rj\<in>f-``{\<zero>\<^sub>S}"
+      using apply_type target_ring.Ring_ZF_1_L3(7) f_is_fun 
+        homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15
+        by auto
+    with assms(1,2) j(1) have "j\<ra>\<^sub>R(t\<rs>\<^sub>Rj) \<in>J"
       unfolding origin_ring.primeIdeal_def
       using origin_ring.ideal_dest_sum by auto
-    then have False using origin_ring.Ring_ZF_2_L1A(5)
-      using jt t by auto
-  }
-  then have "f``J \<noteq> S" by auto moreover
-  {
-    fix I K assume as:"I\<in>target_ring.ideals" "K\<in>target_ring.ideals"
-           "target_ring.productIdeal(I, K) \<subseteq> f``J"
-    then have "f `` ((f -`` I) \<cdot>\<^sub>I (f -`` K)) \<subseteq> f``J" 
-      using prime_ideal_quot_2 assms(3) by auto
-    then have "f-``(f `` ((f -`` I) \<cdot>\<^sub>I (f -`` K))) \<subseteq> f-``(f``J)"
-      by blast
-    moreover have "((f -`` I) \<cdot>\<^sub>I (f -`` K)) \<triangleleft>R"
-      using origin_ring.product_in_intersection(2)[OF preimage_ideal(1)
- preimage_ideal(1)]
-      as(1,2) by auto
-    then have "((f -`` I) \<cdot>\<^sub>I (f -`` K)) \<subseteq> R" using origin_ring.ideal_dest_subset
+    with \<open>j\<in>R\<close> \<open>t\<in>R-J\<close> have False using origin_ring.Ring_ZF_2_L1A(5)
       by auto
-    ultimately have "(f -`` I) \<cdot>\<^sub>I (f -`` K) \<subseteq> f-``(f``J)" 
-      using func1_1_L9[OF fun, of "(f -`` I) \<cdot>\<^sub>I (f -`` K)"] by auto
+  } hence "f``(J) \<noteq> S" by auto 
+  moreover
+  { fix I K assume as: "I\<in>target_ring.ideals" "K\<in>target_ring.ideals"
+           "target_ring.productIdeal(I, K) \<subseteq> f``(J)"
+    let ?A = "(f-``(I)) \<cdot>\<^sub>I (f-``(K))"
+    from as(1,2) have "?A \<subseteq> f-``(f``(?A))"
+      using origin_ring.product_in_intersection(2) preimage_ideal(2)
+        origin_ring.ideal_dest_subset func1_1_L9 f_is_fun by auto
+    with assms(3) as have "?A \<subseteq> f-``(f``(J))"
+      using prime_ideal_quot_2 vimage_mono by force
+    moreover from assms(1) have "J \<subseteq> f-``(f``(J))" 
+      using func1_1_L9 f_is_fun origin_ring.ideal_dest_subset 
+      unfolding origin_ring.primeIdeal_def by auto 
     moreover
-    have "J \<subseteq> f-``(f``J)" using func1_1_L9 fun assms(1)
-      origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def
-      by auto moreover
-    {
-      fix t assume "t\<in>f-``(f``J)"
-      then have t:"f`t\<in>f``J" "t\<in>R" using func1_1_L15 fun by auto
-      from t(1) obtain s where s:"f`t = f`s" "s\<in>J"
-        using func_imagedef fun assms(1)
-        origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def
+    { fix t assume "t \<in> f-``(f``(J))"
+      then have "f`(t)\<in>f``(J)" "t\<in>R" using func1_1_L15 f_is_fun 
         by auto
-      from s(2) assms(1) have ss:"s\<in>R" unfolding origin_ring.primeIdeal_def
+      from assms(1) \<open>f`(t)\<in>f``(J)\<close> obtain s where "f`(t)=f`(s)" "s\<in>J"
+        using func_imagedef f_is_fun origin_ring.ideal_dest_subset 
+        unfolding origin_ring.primeIdeal_def by auto
+      from assms(1) \<open>s\<in>J\<close> have "s\<in>R" 
+        unfolding origin_ring.primeIdeal_def
         using origin_ring.ideal_dest_subset by auto
-      from s(1) have "f`t \<rs>\<^sub>S (f`s) = \<zero>\<^sub>S" using target_ring.Ring_ZF_1_L3(7)[
-        OF apply_type[OF fun t(2)]] by auto
-      then have "f`(t\<rs>\<^sub>Rs) = \<zero>\<^sub>S" using homomor_dest_subs
-        t(2) ss by auto
-      moreover have "t\<rs>\<^sub>Rs \<in>R" using ss t(2)
-        origin_ring.Ring_ZF_1_L4(2) by auto
-      ultimately have "t\<rs>\<^sub>Rs \<in> f-``{\<zero>\<^sub>S}" using func1_1_L15
-        fun by auto
-      with assms(2) have "t\<rs>\<^sub>Rs \<in> J" by auto
-      with s(2) have "s\<ra>\<^sub>R(t\<rs>\<^sub>Rs)\<in>J"
-        using assms(1) origin_ring.ideal_dest_sum
+      with assms(2) \<open>f`(t)=f`(s)\<close> \<open>t\<in>R\<close> have "t\<rs>\<^sub>Rs \<in> J"
+        using target_ring.Ring_ZF_1_L3(7) apply_funtype f_is_fun
+          homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15
+        by auto
+      with assms(1) \<open>s\<in>J\<close> have "s\<ra>\<^sub>R(t\<rs>\<^sub>Rs)\<in>J"
+        using origin_ring.ideal_dest_sum
         unfolding origin_ring.primeIdeal_def by auto
-      then have "t: J" using origin_ring.Ring_ZF_2_L1A(5)
-        ss t(2) by auto
-    }
-    then have "f-``(f``J) \<subseteq> J" by auto
-    ultimately have "(f -`` I) \<cdot>\<^sub>I (f -`` K) \<subseteq> J" by auto
-    moreover have "(f -`` I) \<in>\<I>" "(f -`` K) \<in>\<I>"
-      using as(1,2) preimage_ideal
-        origin_ring.ideal_dest_subset by auto
-    ultimately have "(f -`` I) \<subseteq> J \<or> (f -`` K) \<subseteq> J"
-      using assms(1) unfolding origin_ring.primeIdeal_def by auto
-    then have "f``(f -`` I) \<subseteq> f``J \<or> f``(f -`` K) \<subseteq> f``J"
+      with \<open>s\<in>R\<close> \<open>t\<in>R\<close> have "t\<in>J" using origin_ring.Ring_ZF_2_L1A(5)
+        by auto
+    } hence "f-``(f``J) \<subseteq> J" by auto
+    ultimately have "?A \<subseteq> J" by auto    
+    with assms(1) as(1,2) have "(f-``(I)) \<subseteq> J \<or> (f-``(K)) \<subseteq> J"
+      using preimage_ideal origin_ring.ideal_dest_subset
+      unfolding origin_ring.primeIdeal_def
+      by auto
+    hence "f``(f-``(I)) \<subseteq> f``J \<or> f``(f-``(K)) \<subseteq> f``(J)"
       by auto
-    with assms(3) have "I \<subseteq> f``J \<or> K \<subseteq> f``J"
-      using surj_image_vimage as(1,2) by auto
+    with assms(3) as(1,2) have "I \<subseteq> f``(J) \<or> K \<subseteq> f``(J)"
+      using surj_image_vimage by auto
   }
   ultimately show ?thesis unfolding target_ring.primeIdeal_def by auto
 qed
 
 text\<open>The ideals of the quotient ring are in bijection
-with the ideals of the original ring that contain the ideal
-by which we made the quotient.\<close>
+  with the ideals of the original ring that contain the ideal
+  by which we made the quotient.\<close>
 
 theorem (in ring_homo) ideal_quot_bijection:
   assumes "f\<in>surj(R,S)"
-  defines "idealFun \<equiv> \<lambda>J\<in>target_ring.ideals. f-``J"
+  defines "idealFun \<equiv> \<lambda>J\<in>target_ring.ideals. f-``(J)"
   shows "idealFun \<in> bij(target_ring.ideals,{K\<in>\<I>. ker \<subseteq> K})"
-  unfolding bij_def inj_def surj_def
-proof(safe)
-  have "idealFun \<in> target_ring.ideals \<rightarrow> {f-``J. J\<in>target_ring.ideals}"
-    unfolding idealFun_def
-    using lam_funtype by auto moreover
-  {
-    fix t assume "t\<in>{f-``J. J\<in>target_ring.ideals}"
-    then obtain K where "K\<in>target_ring.ideals" "f-``K = t" by auto
-    then have "ker \<subseteq> t" "t\<triangleleft>R" "t \<subseteq> R" using preimage_ideal[of K]
-      using func1_1_L3[OF surj_is_fun[OF assms(1)], of K]
-      by auto
-    then have "t\<in>{K\<in>\<I>. ker \<subseteq> K}" by auto
-  }
-  then have "{f-``J. J\<in>target_ring.ideals} \<subseteq> {K\<in>\<I>. ker \<subseteq> K}" by blast
-  ultimately show "idealFun \<in> target_ring.ideals \<rightarrow> {K\<in>\<I>. ker \<subseteq> K}"
+proof -
+  let ?\<I>\<^sub>t = "target_ring.ideals"
+  have "idealFun : ?\<I>\<^sub>t \<rightarrow> {f-``(J). J\<in>?\<I>\<^sub>t}"
+    unfolding idealFun_def using lam_funtype by simp 
+  moreover
+  { fix t assume "t \<in> {f-``(J). J\<in>?\<I>\<^sub>t}"
+    then obtain K where "K \<in> ?\<I>\<^sub>t" "f-``(K) = t" by auto
+    then have "K\<triangleleft>R\<^sub>t" by simp
+    then have "(f-``(K))\<triangleleft>R" "ker \<subseteq> f-``(K)" using preimage_ideal(2,3)
+      by simp_all
+    with \<open>f-``(K) = t\<close> have "ker \<subseteq> t" "t\<triangleleft>R" by simp_all
+    with \<open>f-``(K) = t\<close> have "t\<in>{K\<in>\<I>. ker \<subseteq> K}" using func1_1_L3 f_is_fun 
+      by blast
+  } hence "{f-``(J). J\<in>?\<I>\<^sub>t} \<subseteq> {K\<in>\<I>. ker \<subseteq> K}" by blast
+  ultimately have I: "idealFun : ?\<I>\<^sub>t \<rightarrow> {K\<in>\<I>. ker \<subseteq> K}"
     using func1_1_L1B by auto
-  then show "idealFun \<in> target_ring.ideals \<rightarrow> {K\<in>\<I>. ker \<subseteq> K}".
-  {
-    fix w x assume as:"w\<triangleleft>R\<^sub>t" "x\<triangleleft>R\<^sub>t" "w\<subseteq>S" "x\<subseteq>S" "idealFun ` w = idealFun ` x"
-    then have "f-``w = f-``x" unfolding idealFun_def
-      using beta by auto
-    then have "f``(f-``w) = f``(f-``x)" by auto
-    then show "w = x" using surj_image_vimage assms(1) as
-      by auto
+  { fix w x assume 
+      as: "w\<triangleleft>R\<^sub>t" "x\<triangleleft>R\<^sub>t" "w\<subseteq>S" "x\<subseteq>S" "idealFun`(w) = idealFun`(x)"
+    then have "f``(f-``(w)) = f``(f-``(x))" unfolding idealFun_def by simp
+    with assms(1) as have "w = x" using surj_image_vimage
+      by simp
   }
-  {
-    fix y assume y:"y\<triangleleft>R" "y\<subseteq>R" "ker \<subseteq> y"
-    from y(2) have "y \<subseteq> f-``(f``y)" using func1_1_L9[OF surj_is_fun] 
-        assms(1) by auto
+  with I have "idealFun \<in>  inj(?\<I>\<^sub>t,{K\<in>\<I>. ker \<subseteq> K})"
+    unfolding inj_def by auto
+  moreover
+  { fix y assume "y\<triangleleft>R" "y\<subseteq>R" "ker \<subseteq> y"
+    from \<open>y\<subseteq>R\<close> have "y \<subseteq> f-``(f``y)" using func1_1_L9 f_is_fun 
+      by auto
     moreover
-    {
-      fix t assume "t\<in>f-``(f``y)"
-      then have t:"f`t\<in>f``y" "t\<in>R" using func1_1_L15[OF surj_is_fun] 
-            assms(1) by auto
-      from t(1) y(2) obtain s where s:"s\<in>y" "f`t = f`s" 
-        using func_imagedef[of f R S y, OF surj_is_fun] assms(1) 
+    { fix t assume "t\<in>f-``(f``(y))"
+      then have "f`(t) \<in> f``(y)" "t\<in>R" using func1_1_L15 f_is_fun 
         by auto
-      from s(1) have "s\<in>R" using y(2) by auto
-      with t(2) have E:"f`t : S" "f`s: S" using apply_type[of f R "\<lambda>u. S", OF surj_is_fun]
-        assms(1) by auto
-      from E(1) s(2) have "(f`t)\<rs>\<^sub>S(f`s) = \<zero>\<^sub>S"
-        using target_ring.Ring_ZF_1_L3(7) by auto
-      then have "f`(t\<rs>\<^sub>Rs) = \<zero>\<^sub>S" using homomor_dest_subs
-        t(2) `s:R` by auto
-      moreover from \<open>s\<in>R\<close> have "t\<rs>\<^sub>Rs \<in>R" 
-        using origin_ring.Ring_ZF_1_L4(2) t(2) by auto
-      ultimately have "t\<rs>\<^sub>Rs \<in> f-``{\<zero>\<^sub>S}"
-        using func1_1_L15[OF surj_is_fun] assms(1) by auto
-      with y(3) have "t\<rs>\<^sub>Rs \<in> y" by auto
-      with s(1) have "s\<ra>\<^sub>R(t\<rs>\<^sub>Rs) \<in> y" using 
-        origin_ring.ideal_dest_sum y(1) by auto
-      then have "t\<in>y" using origin_ring.Ring_ZF_2_L1A(5)
-        using `s\<in>R` t(2) by auto
-    }
-    ultimately have "f-``(f``y) = y" by blast moreover
-    have "f``y \<subseteq> S" using func1_1_L6(2)[of f R S] assms(1)
-      unfolding surj_def by auto moreover
-    have "(f``y)\<triangleleft>R\<^sub>t" using image_ideal_surj
-      assms(1) y(1) by auto
-    ultimately show "\<exists>x\<in>target_ring.ideals. idealFun ` x = y"
-      unfolding idealFun_def
-      by auto
+      from \<open>f`(t) \<in> f``(y)\<close> \<open>y\<subseteq>R\<close> obtain s where "s\<in>y" "f`(t) = f`(s)" 
+        using func_imagedef f_is_fun by auto
+      from \<open>s\<in>y\<close>  \<open>y\<subseteq>R\<close> have "s\<in>R" by auto
+      with \<open>t\<in>R\<close> \<open>f`(t) = f`(s)\<close> \<open>ker \<subseteq> y\<close> have "t\<rs>\<^sub>Rs \<in> y"
+        using target_ring.Ring_ZF_1_L3(7) homomor_dest_subs 
+          origin_ring.Ring_ZF_1_L4(2) func1_1_L15 f_is_fun
+        by auto
+      with \<open>s\<in>y\<close> \<open>y\<triangleleft>R\<close> \<open>s\<in>R\<close> \<open>t\<in>R\<close> have "t\<in>y"
+        using origin_ring.ideal_dest_sum origin_ring.Ring_ZF_2_L1A(5)
+        by force
+    } 
+    ultimately have "f-``(f``(y)) = y" by blast 
+    moreover have "f``(y) \<subseteq> S" using func1_1_L6(2) f_is_fun
+      unfolding surj_def by auto 
+    moreover from assms(1) \<open>y\<triangleleft>R\<close> have "(f``(y))\<triangleleft>R\<^sub>t" using image_ideal_surj
+       by auto
+    ultimately have "\<exists>x\<in>?\<I>\<^sub>t. idealFun`(x) = y"
+      unfolding idealFun_def by auto
   }
+  with I have "idealFun \<in> surj(?\<I>\<^sub>t,{K\<in>\<I>. ker \<subseteq> K})"
+    unfolding surj_def by auto
+  ultimately show ?thesis unfolding bij_def by blast
 qed
 
+text\<open>Assume the homomorphism $f$ is surjective and consider the function
+  that maps an ideal $J$ in the target ring to its inverse image
+  $f^{-1}(J)$ (in the source ring). Then the value of the converse
+  of that function on any ideal containing the kernel of $f$ is the image
+  of that ideal under the homomorphism $f$.  \<close>
+
 theorem (in ring_homo) quot_converse:
-  defines "idealFun \<equiv> \<lambda>J\<in>target_ring.ideals. f-``J"
-  assumes "J\<triangleleft>R" "ker\<subseteq>J" "f:surj(R,S)"
-  shows "converse(idealFun)`J = f``J"
+  defines "F \<equiv> \<lambda>J\<in>target_ring.ideals. f-``(J)"
+  assumes "J\<triangleleft>R" "ker\<subseteq>J" "f\<in>surj(R,S)"
+  shows "converse(F)`(J) = f``(J)"
 proof-
-  let ?g="\<lambda>J\<in>{K\<in>\<I>. ker\<subseteq>K}. f``J"
-  have "?g\<in>{K\<in>\<I>. ker\<subseteq>K} \<rightarrow> {f``J. J\<in>{K\<in>\<I>. ker\<subseteq>K}}"
-    using lam_funtype by auto moreover
-  have "{f``J. J\<in>{K\<in>\<I>. ker\<subseteq>K}} \<subseteq> target_ring.ideals"
-    using image_ideal_surj target_ring.ideal_dest_subset
-    assms(4) by auto
-  ultimately have "?g\<in>{K\<in>\<I>. ker\<subseteq>K} \<rightarrow> target_ring.ideals" 
-    using func1_1_L1B by auto
-  have "converse(idealFun)\<in>bij({K\<in>\<I>. ker\<subseteq>K}, target_ring.ideals)" 
-    using bij_converse_bij ideal_quot_bijection assms(4)
-    unfolding idealFun_def by auto
-  then have confun:"converse(idealFun):{K\<in>\<I>. ker\<subseteq>K} \<rightarrow> target_ring.ideals"
-    unfolding bij_def inj_def by auto
-  moreover have J:"J\<in>{K\<in>\<I>. ker\<subseteq>K}" using assms(2,3) 
-    origin_ring.ideal_dest_subset by auto
-  ultimately have ideal:"converse(idealFun)`J \<in> target_ring.ideals"
-    using apply_type[of "converse(idealFun)" "{K\<in>\<I>. ker\<subseteq>K}" "\<lambda>q. target_ring.ideals" J]
-    by auto
-  then have "?g`(idealFun`(converse(idealFun)`J)) = ?g`(f-``(converse(idealFun)`J))"
-    using beta unfolding idealFun_def
-    by auto moreover
-  from preimage_ideal ideal
-    have "(f-``(converse(idealFun)`J))\<triangleleft>R" "ker \<subseteq> (f-``(converse(idealFun)`J))" by auto
-  then have "?g`(f-``(converse(idealFun)`J)) = f``(f-``(converse(idealFun)`J))"
-    using beta origin_ring.ideal_dest_subset by auto
-  ultimately have "?g`(idealFun`(converse(idealFun)`J)) = f``(f-``(converse(idealFun)`J))"
+  let ?g="\<lambda>J\<in>{K\<in>\<I>. ker\<subseteq>K}. f``(J)"
+  let ?\<I>\<^sub>t = "target_ring.ideals"
+  let ?C\<^sub>F = "converse(F)"
+  from assms(1,4) have "?C\<^sub>F \<in> bij({K\<in>\<I>. ker\<subseteq>K}, ?\<I>\<^sub>t)" 
+    using bij_converse_bij ideal_quot_bijection 
     by auto
-  then have "?g`(idealFun`(converse(idealFun)`J)) = converse(idealFun)`J"
-    using surj_image_vimage assms(4) ideal by auto
-  then have "?g`J = converse(idealFun)`J"
-    using right_inverse_lemma[of idealFun target_ring.ideals
-        "{K \<in> \<I> . ker \<subseteq> K}" "{K \<in> \<I> . ker \<subseteq> K}" J ] J
-    confun bij_is_fun[OF ideal_quot_bijection] assms(4)
-    unfolding idealFun_def by auto
-  then show ?thesis using beta J by auto
+  then have I: "?C\<^sub>F:{K\<in>\<I>. ker\<subseteq>K} \<rightarrow> ?\<I>\<^sub>t"
+    unfolding bij_def inj_def by auto
+  moreover from assms(2,3) have J: "J \<in> {K\<in>\<I>. ker\<subseteq>K}" 
+    using origin_ring.ideal_dest_subset by auto
+  ultimately have ideal: "?C\<^sub>F`(J) \<in> ?\<I>\<^sub>t"
+    using apply_funtype by blast
+  with assms(1,4) ideal have "?g`(F`(?C\<^sub>F`(J))) = ?C\<^sub>F`(J)"
+    using preimage_ideal origin_ring.ideal_dest_subset
+      surj_image_vimage by auto
+  moreover
+  from assms(1) have "F: ?\<I>\<^sub>t \<rightarrow> {f-``(J). J\<in>?\<I>\<^sub>t}"
+    using lam_funtype by simp
+  with I J have "F`(?C\<^sub>F`(J)) = J"
+    using right_inverse_lemma by simp
+  ultimately have "?g`(J) = ?C\<^sub>F`(J)" by simp
+  with J show ?thesis by simp
 qed
   
 text\<open>Since the map is surjective, this bijection
-restricts to prime ideals on both sides.\<close>
+  restricts to prime ideals on both sides.\<close>
 
 corollary (in ring_homo) prime_ideal_quot_3:
-  assumes "K\<triangleleft>R\<^sub>t" "f:surj(R,S)"
-  shows "K\<triangleleft>\<^sub>pR\<^sub>t \<longleftrightarrow> ((f-``K)\<triangleleft>\<^sub>pR\<^sub>o)"
+  assumes "K\<triangleleft>R\<^sub>t" "f \<in> surj(R,S)"
+  shows "K\<triangleleft>\<^sub>pR\<^sub>t \<longleftrightarrow> ((f-``(K))\<triangleleft>\<^sub>pR)"
 proof
-  {
-    assume as:"K\<triangleleft>\<^sub>pR\<^sub>t"
-    then have "(f-``K)\<triangleleft>\<^sub>pR\<^sub>o" using preimage_prime_ideal_surj
-      assms(2) by auto
-    then show "(f-``K)\<triangleleft>\<^sub>pR\<^sub>o"
-      using beta[of K target_ring.ideals]
-      using target_ring.ideal_dest_subset[of K] as
+  { assume "K\<triangleleft>\<^sub>pR\<^sub>t"
+    with assms(2) show "(f-``(K))\<triangleleft>\<^sub>pR"
+      using preimage_prime_ideal_surj target_ring.ideal_dest_subset
       unfolding target_ring.primeIdeal_def by auto
-  } moreover
-  {
-    assume as:"(f-``K)\<triangleleft>\<^sub>pR\<^sub>o"
-    from assms(1) have "K\<triangleleft>R\<^sub>t". moreover
-    {
-      assume "K=S"
-      then have "f-``K = f-``S" by auto
-      then have "f-``K = R" using func1_1_L4
-        assms(2) unfolding surj_def by auto
-      with as have False unfolding origin_ring.primeIdeal_def by auto
-    }
-    then have "K\<noteq>S" by auto moreover
-    {
-      fix J P assume jp:"J\<in>target_ring.ideals"
+  }
+  { assume "(f-``(K))\<triangleleft>\<^sub>pR"
+    with assms(1,2) have "K\<triangleleft>R\<^sub>t" and "K\<noteq>S"
+      using func1_1_L4 unfolding origin_ring.primeIdeal_def surj_def 
+      by auto    
+    moreover
+    { fix J P assume jp: "J\<in>target_ring.ideals"
         "P\<in>target_ring.ideals"
         "target_ring.productIdeal(J, P) \<subseteq> K"
-      have sub:"((f -`` J) \<cdot>\<^sub>I (f -`` P)) \<union> ker \<subseteq> R"
-        using origin_ring.ideal_dest_subset
-        origin_ring.product_in_intersection(2) 
-        preimage_ideal target_ring.zero_ideal
-        jp by auto
-      from jp(3) have "f -``target_ring.productIdeal(J, P) \<subseteq> f -``K"
+      from jp(3) have "f-``(target_ring.productIdeal(J, P)) \<subseteq> f-``(K)"
         by auto
-      with jp(1,2) have A:"((f -`` J) \<cdot>\<^sub>I (f -`` P)) +\<^sub>I (ker) \<subseteq> f -``K" 
-        using prime_ideal_quot assms(2)
-        by auto moreover
-      have j:"J\<triangleleft>R\<^sub>t" and p:"P\<triangleleft>R\<^sub>t" using jp(1,2) by auto
-      then have "(f -`` J) \<cdot>\<^sub>I (f -`` P) \<union> ker \<subseteq> R"
-        using origin_ring.ideal_dest_subset[OF origin_ring.product_in_intersection(2)
-            [OF preimage_ideal(1) preimage_ideal(1)]]
-            origin_ring.ideal_dest_subset[OF preimage_ideal(1)[OF target_ring.zero_ideal]]
-        by auto
-      with A have "((f -`` J) \<cdot>\<^sub>I (f -`` P)) \<subseteq> f -``K" 
-        unfolding origin_ring.sumIdeal_def[OF origin_ring.product_in_intersection(2)
-            [OF preimage_ideal(1)[OF j] preimage_ideal(1)[OF p]]   
-            preimage_ideal(1)[OF target_ring.zero_ideal]] using
-            origin_ring.generated_ideal_contains_set[of "(f -`` J) \<cdot>\<^sub>I (f -`` P) \<union> ker"]
-            by auto
-      moreover have "f -`` J \<in>\<I>" "f -`` P \<in>\<I>"
-        using preimage_ideal
-        origin_ring.ideal_dest_subset jp(1,2) by auto
-      ultimately have "f -`` J \<subseteq> f -`` K \<or> f -`` P \<subseteq> f -`` K"
-        using as unfolding origin_ring.primeIdeal_def by auto
-      then have "f``(f -`` J) \<subseteq> f``(f -`` K) \<or> f``(f -`` P) \<subseteq> f``(f -`` K)"
+      with assms(2) jp(1,2) have 
+        A: "((f-``(J)) \<cdot>\<^sub>I (f-``(P))) +\<^sub>I (ker) \<subseteq> f-``(K)" 
+        using prime_ideal_quot by auto 
+      from jp(1,2) have 
+        "(f-``(J))\<cdot>\<^sub>I(f-``(P)) \<union> ker \<subseteq> ((f-``(J))\<cdot>\<^sub>I(f-``(P))) +\<^sub>I (ker)"
+        using preimage_ideal origin_ring.product_in_intersection(2) 
+          kernel_ideal origin_ring.comp_in_sum_ideals(3) by simp
+      with A have "((f -`` J) \<cdot>\<^sub>I (f -`` P)) \<subseteq> f-``(K)" by auto
+      with \<open>(f-``(K))\<triangleleft>\<^sub>pR\<close> jp(1,2) have 
+        "f-``(J) \<subseteq> f-``(K) \<or> f-``(P) \<subseteq> f-``(K)"
+        using preimage_ideal origin_ring.ideal_dest_subset
+        unfolding origin_ring.primeIdeal_def by auto
+      then have 
+        "f``(f-``(J)) \<subseteq> f``(f-``(K)) \<or> f``(f-``(P)) \<subseteq> f``(f-``(K))"
         by blast
-      then have "J \<subseteq> K \<or> P \<subseteq> K" using assms(2)
-        surj_image_vimage jp(1,2) assms target_ring.ideal_dest_subset
+      with assms jp(1,2) have "J \<subseteq> K \<or> P \<subseteq> K" 
+        using surj_image_vimage target_ring.ideal_dest_subset
         by auto
     }
     ultimately show "K\<triangleleft>\<^sub>pR\<^sub>t"
@@ -1056,67 +975,61 @@ proof
   }
 qed
 
+text\<open>If the homomorphism is surjective then the function
+  that maps ideals in the target ring to their inverse images (in the source ring)
+  is a bijection between prime ideals in the target ring and the prime ideals
+  containing the kernel in the source ring. \<close>
+
 corollary (in ring_homo) bij_prime_ideals:
-  defines "idealFun \<equiv> \<lambda>J\<in>target_ring.ideals. f-``J"
-  assumes "f:surj(R,S)"
-  shows "restrict(idealFun,{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t})\<in>bij({J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}, {J\<in>Pow(R). ker\<subseteq>J \<and> (J\<triangleleft>\<^sub>pR)})"
-proof-
-  have "{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t} \<subseteq> target_ring.ideals"
+  defines "F \<equiv> \<lambda>J\<in>target_ring.ideals. f-``(J)"
+  assumes "f \<in> surj(R,S)"
+  shows "restrict(F,{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}) \<in> 
+    bij({J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}, {J\<in>Pow(R). ker\<subseteq>J \<and> (J\<triangleleft>\<^sub>pR)})"
+proof -
+  let ?\<I>\<^sub>t = "target_ring.ideals"
+  from assms have I: "F:?\<I>\<^sub>t \<rightarrow> {K\<in>\<I>. ker \<subseteq> K}"
+    using ideal_quot_bijection bij_is_fun by simp 
+  have II: "{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t} \<subseteq> ?\<I>\<^sub>t"
     unfolding target_ring.primeIdeal_def by auto
-  then have rest_bij:"restrict(idealFun,{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t})\<in>bij({J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}, idealFun``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t})"
-    using restrict_bij assms(2)
-    ideal_quot_bijection unfolding bij_def
-    idealFun_def by auto
-  {
-    fix t assume t:"t\<in>idealFun``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}"
-    have sub:"{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t} \<subseteq> target_ring.ideals"
-      unfolding target_ring.primeIdeal_def by auto
-    from t obtain q where q:"q\<in>{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}" "t=idealFun`q"
-      using assms(2) func_imagedef[OF bij_is_fun[OF ideal_quot_bijection] sub]
-      unfolding idealFun_def by auto
-    note q(1) moreover
-    then have "q\<in>target_ring.ideals" unfolding
-      target_ring.primeIdeal_def by auto moreover
-    with q(2) have "t = f-``q" "ker\<subseteq>t" "t\<triangleleft>R" unfolding idealFun_def 
-      using beta
-      apply_type[OF ideal_quot_bijection[THEN bij_is_fun], of q] assms(2) by auto
-    ultimately have "t\<triangleleft>R" "t\<triangleleft>\<^sub>pR" "ker\<subseteq>t" using assms(2) prime_ideal_quot_3
-      by auto
-  }
-  then have "idealFun `` Collect(Pow(S), prime_ideal_target) \<subseteq> {t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)}"
-    using origin_ring.ideal_dest_subset by blast moreover
-  {
-    fix t assume "t\<in>{t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)}"
-    then have t:"t\<in>Pow(R)" "ker\<subseteq>t" "t\<triangleleft>\<^sub>pR" by auto
-    then have tSet:"t\<in>{t\<in>\<I>. ker \<subseteq> t}" unfolding origin_ring.primeIdeal_def by auto
-    have "converse(idealFun)\<in>bij({t\<in>\<I>. ker \<subseteq> t}, target_ring.ideals)"
-      using ideal_quot_bijection[OF assms(2)] bij_converse_bij unfolding idealFun_def
-      by auto
-    with tSet have cont:"converse(idealFun)`t \<in> target_ring.ideals"
-      using apply_type[OF bij_is_fun] by blast moreover
-    from tSet have eq:"idealFun`(converse(idealFun)`t) = t"
-      using ideal_quot_bijection assms(2) unfolding idealFun_def
-      using right_inverse_bij by blast
-    ultimately have "f-``(converse(idealFun)`t) = t"
-      using beta unfolding idealFun_def by auto
-    with t(3) have "(converse(idealFun)`t) \<triangleleft>\<^sub>pR\<^sub>t"
-      using prime_ideal_quot_3 cont assms(2) by auto
-    then have "(converse(idealFun)`t) \<triangleleft>\<^sub>pR\<^sub>t" "(converse(idealFun)`t) \<subseteq> S"
-      unfolding target_ring.primeIdeal_def
-      using target_ring.ideal_dest_subset by auto
-    then have elem:"converse(idealFun)`t\<in>{q\<in>Pow(S). q\<triangleleft>\<^sub>pR\<^sub>t}"
-      by auto
-    have sub:"{q\<in>Pow(S). q\<triangleleft>\<^sub>pR\<^sub>t} \<subseteq> target_ring.ideals"
-      unfolding target_ring.primeIdeal_def by auto
-    have "t\<in>idealFun``Collect(Pow(S), prime_ideal_target)"
-      using assms(2) func_imagedef[OF ideal_quot_bijection[THEN bij_is_fun] sub] unfolding idealFun_def
-      using eq elem unfolding idealFun_def by auto
-  }
-  then have "{t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)} \<subseteq> idealFun``Collect(Pow(S), prime_ideal_target)" by auto
-  ultimately
-  have "{t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)} = idealFun``Collect(Pow(S), prime_ideal_target)"
+  have III: "{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t} \<subseteq> ?\<I>\<^sub>t" 
+    unfolding target_ring.primeIdeal_def by auto
+  with assms have "restrict(F,{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}) \<in> 
+    bij({J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}, F``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t})"
+    using restrict_bij ideal_quot_bijection unfolding bij_def 
     by auto
-  with rest_bij show ?thesis by auto
+  moreover have "{t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)} = F``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}"
+  proof 
+    { fix t assume "t \<in> F``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}"
+      with I III obtain q where "q\<in>Pow(S)" "q\<triangleleft>\<^sub>pR\<^sub>t" "t=F`(q)"
+        using func_imagedef by auto 
+      from \<open>q\<in>Pow(S)\<close> \<open>q\<triangleleft>\<^sub>pR\<^sub>t\<close> have "q\<in>?\<I>\<^sub>t" 
+        unfolding target_ring.primeIdeal_def by auto
+      with I have "F`(q) \<in> {K\<in>\<I>. ker \<subseteq> K}" using apply_funtype 
+        by blast
+      with assms \<open>q\<triangleleft>\<^sub>pR\<^sub>t\<close> \<open>t=F`(q)\<close> \<open>q\<in>?\<I>\<^sub>t\<close> \<open>t=F`(q)\<close> have 
+        "t\<triangleleft>R" "t\<triangleleft>\<^sub>pR" "ker\<subseteq>t"
+        using prime_ideal_quot_3 by simp_all
+    } then show "F``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t} \<subseteq> {t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)}"
+      using origin_ring.ideal_dest_subset by blast
+    { fix t assume "t\<in>{t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)}"
+      then have "t\<in>Pow(R)" "ker\<subseteq>t" "t\<triangleleft>\<^sub>pR" by auto
+      then have tSet: "t \<in> {t\<in>\<I>. ker \<subseteq> t}" 
+        unfolding origin_ring.primeIdeal_def by auto
+      with assms have cont: "converse(F)`(t) \<in> ?\<I>\<^sub>t"
+        using ideal_quot_bijection bij_converse_bij 
+          apply_funtype bij_is_fun by blast
+      moreover from assms tSet have "F`(converse(F)`(t)) = t"
+        using ideal_quot_bijection right_inverse_bij by blast
+      ultimately have "f-``(converse(F)`(t)) = t"
+        using assms(1) by simp
+      with assms II tSet \<open>t\<triangleleft>\<^sub>pR\<close> cont have "t \<in> F``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}"
+        using prime_ideal_quot_3 target_ring.ideal_dest_subset
+          bij_val_image_vimage ideal_quot_bijection
+        unfolding target_ring.primeIdeal_def by auto
+    } thus "{t\<in>Pow(R). ker\<subseteq>t \<and> (t\<triangleleft>\<^sub>pR)} \<subseteq> F``{J\<in>Pow(S). J\<triangleleft>\<^sub>pR\<^sub>t}" 
+      by auto
+  qed
+  ultimately show ?thesis by auto
 qed
     
 end
\ No newline at end of file
diff --git a/IsarMathLib/Ring_Zariski_ZF_3.thy b/IsarMathLib/Ring_Zariski_ZF_3.thy
index 3c221fe..58fa680 100644
--- a/IsarMathLib/Ring_Zariski_ZF_3.thy
+++ b/IsarMathLib/Ring_Zariski_ZF_3.thy
@@ -320,8 +320,8 @@ proof
       assms(2) by auto
     with t have p:"t\<in>origin_ring.Spec" "\<not>(f-``I \<subseteq> t)"
       using origin_ring.openBasic_def by auto
-    from t(2) have kt:"ker \<subseteq> t" using origin_ring.closeBasic_def[OF
-      func1_1_L3[OF fun]] by auto
+    from t(2) have kt:"ker \<subseteq> t" using origin_ring.closeBasic_def
+      func1_1_L3 f_is_fun by auto
     {
       fix x assume "x\<in>f-``(f``t)"
       then have t:"f`x\<in>f``t" "x\<in>R" using func1_1_L15
@@ -383,11 +383,10 @@ proof
     spectrum_surj_bij[OF assms(2)]],of U] 
     unfolding g_def by blast
   moreover
-  have "D(f -`` I) \<in>\<tau>\<^sub>o" unfolding top_origin_def
-    using preimage_ideal(1)[OF I(1)]
-      origin_ring.ideal_dest_subset by auto
-  then have "V(ker)\<inter>D(f -`` I) \<in> {V(ker) \<inter> A . A \<in> \<tau>\<^sub>o}"
-    by auto
+  from I(1) have "(f-``(I)) \<triangleleft>R" and "(f-``(I)) \<subseteq> R" 
+    using preimage_ideal(2)  origin_ring.ideal_dest_subset by simp_all
+  then have "V(ker)\<inter>D(f-``(I)) \<in> {V(ker) \<inter> A . A \<in> \<tau>\<^sub>o}"
+    unfolding top_origin_def by auto
   ultimately show "g``U:  \<tau>\<^sub>o{restricted to}V(ker)"
     unfolding RestrictedTo_def by auto
 qed
@@ -406,8 +405,8 @@ proof-
     top_origin_def RestrictedTo_def using origin_ring.total_spec
     by auto
   then have "\<Union>(\<tau>\<^sub>o{restricted to}V(ker)) = V(ker)"
-    using origin_ring.closeBasic_def[OF func1_1_L3[OF fun,
-    of "{\<zero>\<^sub>S}"]] by auto moreover
+    using origin_ring.closeBasic_def func1_1_L3 f_is_fun
+     by auto moreover
   have "\<Union>\<tau>\<^sub>t = target_ring.Spec" unfolding top_target_def
     using target_ring.total_spec by auto
   ultimately show ?thesis using bij_cont_open_homeo[of g \<tau>\<^sub>t "\<tau>\<^sub>o{restricted to}V(ker)"]
diff --git a/IsarMathLib/func1.thy b/IsarMathLib/func1.thy
index ee97f2b..af3bfda 100644
--- a/IsarMathLib/func1.thy
+++ b/IsarMathLib/func1.thy
@@ -560,7 +560,7 @@ lemma func1_1_L13A: assumes A1: "f``(A)\<noteq>0" shows "A\<noteq>0"
 
 text\<open>What is the inverse image of a singleton?\<close>
 
-lemma func1_1_L14: assumes "f\<in>X\<rightarrow>Y" 
+lemma func1_1_L14: assumes "f:X\<rightarrow>Y" 
   shows "f-``({y}) = {x\<in>X. f`(x) = y}" 
   using assms func1_1_L6A vimage_singleton_iff apply_iff by auto
 
@@ -652,6 +652,14 @@ proof
   qed
 qed  
 
+text\<open>If all elements of a nonempty set map to the same element of the codomain,
+  then the image of this set is a singleton.\<close>
+
+lemma image_constant_singleton: 
+  assumes "f:X\<rightarrow>Y" "A\<subseteq>X" "A\<noteq>0" "\<forall>x\<in>A. f`(x) = c"
+  shows "f``(A) = {c}"
+  using assms func_imagedef by auto
+
 text\<open>A technical lemma about graphs of functions: if we have two disjoint sets $A$ and $B$
   then the cartesian product of the inverse image of $A$ and $B$ is disjoint
   with (the graph of) $f$.\<close>
@@ -879,8 +887,7 @@ proof -
 qed
 
 text\<open>A composition of functions is a function. This is a slight
-  generalization of standard Isabelle's \<open>comp_fun\<close>
-\<close>
+  generalization of standard Isabelle's \<open>comp_fun\<close>. \<close>
 
 lemma comp_fun_subset: 
   assumes A1: "g:A\<rightarrow>B"  and A2: "f:C\<rightarrow>D" and A3: "B \<subseteq> C"
@@ -1290,6 +1297,28 @@ proof -
     using func1_1_L5A right_inverse by auto
 qed
 
+text\<open>For a bijection between $Y$ and $X$ and a set $A\subseteq X$ 
+  an element $y\in Y$ is in the image $f(A)$ if and only if $f^{-1}(y)$ 
+  is an element of $A$. Note this is false with the weakened assumption that 
+  $f$ is an injection, for example consider $f:\{ 0,1\}\rightarrow \mathbb{N}, f(n)= n+1$
+  and $y=3$. Then $f^{-1}:\{1, 2\}\rightarrow \{ 0,1\}$ and (since $3$ is not in the domain 
+  of the inverse function) $f^{-1}(3) = \emptyset = 0 \in {0,1}$, but $3$ is not in the 
+  image $f(\{ 0,1\})$.  \<close>
+
+lemma bij_val_image_vimage: assumes "f \<in> bij(X,Y)" "A\<subseteq>X" "y\<in>Y"
+  shows "y\<in>f``(A) \<longleftrightarrow> converse(f)`(y) \<in> A"
+proof 
+  assume "y\<in>f``(A)"
+  with assms(1,2) show "converse(f)`(y) \<in> A" 
+    unfolding bij_def using inj_inv_back_in_set by blast
+next
+  assume "converse(f)`(y) \<in> A"
+  with assms(1,3) have "y\<in>{f`(x). x\<in>A}" using right_inverse_bij 
+    by force
+  with assms(1,2) show "y\<in>f``(A)" using bij_is_fun func_imagedef 
+    by force
+qed
+
 text\<open>For injections if a value at a point 
   belongs to the image of a set, then the point
   belongs to the set.\<close>