(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2022 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Rings - Ideals› theory Ring_ZF_2 imports Ring_ZF Group_ZF_2 Finite_ZF Finite1 Cardinal_ZF Semigroup_ZF begin text ‹This section defines the concept of a ring ideal, and defines some basic concepts and types, finishing with the theorem that shows that the quotient of the additive group by the ideal is actually a full ring.› text‹An ideal is a subgroup of the additive group of the ring, which is closed by left and right multiplication by any ring element.› definition (in ring0) Ideal ("_◃R") where "I ◃R ≡ (∀x∈I. ∀y∈R. y⋅x∈I ∧ x⋅y∈I) ∧ IsAsubgroup(I,A)" text‹To write less during proofs, we add this small definition› abbreviation (in ring0) ideals ("ℐ") where "ℐ ≡ {J∈Pow(R). J◃R}" text‹The first examples of ideals are the whole ring and the zero ring:› lemma (in ring0) R_ideal: shows "R ◃R" unfolding Ideal_def apply simp using add_group.group0_3_T3[of R] Ring_ZF_1_L3(1) Ring_ZF_1_L2(1) unfolding IsOpClosed_def using Ring_ZF_1_L4(1,3) by auto lemma (in ring0) zero_ideal: shows "{𝟬} ◃R" unfolding Ideal_def using Ring_ZF_1_L6 add_group.unit_singl_subgr by auto text‹Some small lemmas dividing the definition of ideal into small parts› lemma (in ring0) ideal_dest_subset: assumes "I ◃R" shows "I ⊆ R" using assms unfolding Ideal_def using add_group.group0_3_L2 by auto lemma (in ring0) ideal_dest_sum: assumes "I ◃R" "x∈I" "y∈I" shows "x\<ra>y ∈I" using assms add_group.group0_3_L6 unfolding Ideal_def by auto lemma (in ring0) ideal_dest_mult: assumes "I ◃R" "x∈I" "y∈R" shows "x⋅y ∈I" "y⋅x ∈I" using assms unfolding Ideal_def by auto lemma (in ring0) ideal_dest_minus: assumes "I ◃R" "x∈I" shows "(\<rm>x) ∈ I" using assms unfolding Ideal_def using add_group.group0_3_T3A by auto lemma (in ring0) ideal_dest_zero: assumes "I ◃R" shows "𝟬 ∈ I" using assms unfolding Ideal_def using add_group.group0_3_L5 by auto text‹The most simple way to obtain an ideal from others is the intersection, since the intersection of arbitrary ideals is an ideal.› theorem (in ring0) intersection_ideals: assumes "∀J∈𝒥. (J ◃R)" "𝒥 ≠ 0" shows "(⋂𝒥) ◃R" proof- { fix x assume x:"x:⋂𝒥" { fix y assume y:"y:R" { fix J assume J:"J∈𝒥" with x have "x∈J" by auto with y J have "y⋅x∈J ∧ x⋅y∈J" using assms(1) ideal_dest_mult by auto } then have "y⋅x∈⋂𝒥 ∧ x⋅y∈⋂𝒥" using assms(2) by auto } then have "∀y∈R. y⋅x∈⋂𝒥 ∧ x⋅y∈⋂𝒥" by auto } then have e2:"∀x∈⋂𝒥. ∀y∈R. y⋅x∈⋂𝒥 ∧ x⋅y∈⋂𝒥" by auto have "IsAsubgroup(⋂𝒥,A)" using add_group.subgroup_inter[OF assms(2)] assms(1) unfolding Ideal_def by auto with e2 show ?thesis unfolding Ideal_def by auto qed text‹From any set, we may construct the minimal ideal containing that set› definition (in ring0) generatedIdeal ("⟨_⟩⇩_{I}") where "X⊆R ⟹ ⟨X⟩⇩_{I}≡ ⋂{I∈ℐ. X ⊆ I}" text‹The ideal generated by a set is an ideal› corollary (in ring0) generated_ideal_is_ideal: assumes "X⊆R" shows " ⟨X⟩⇩_{I}◃R" unfolding generatedIdeal_def[OF assms] apply (rule intersection_ideals) apply simp using R_ideal assms by auto text‹The ideal generated by a set is contained in any ideal containing the set› corollary (in ring0) generated_ideal_small: assumes "X ⊆ I" "I ◃R" shows " ⟨X⟩⇩_{I}⊆ I" proof- have "I∈{J∈Pow(R). J ◃R ∧ X⊆J}" using assms(2,1) ideal_dest_subset by auto then have "⋂{J∈Pow(R). J ◃R ∧ X⊆J} ⊆ I" by auto moreover from assms have "X⊆ R" using ideal_dest_subset by auto ultimately show "⟨X⟩⇩_{I}⊆ I" using generatedIdeal_def[of X] by auto qed text‹The ideal generated by a set contains the set› corollary (in ring0) generated_ideal_contains_set: assumes "X⊆R" shows "X⊆⟨X⟩⇩_{I}" proof- { fix J assume J:"J:{J∈ℐ. X⊆J}" { fix t assume "t:X" with J have "t:J" by auto } then have "X⊆J" by auto } then have "X⊆⋂{J∈ℐ. X⊆J} ∨ {J∈ℐ. X⊆J}=0" by auto then show "X⊆⟨X⟩⇩_{I}" unfolding generatedIdeal_def[OF assms] using assms R_ideal by auto qed text‹To be able to show properties of an ideal generated by a set, we have the following induction result› lemma (in ring0) induction_generated_ideal: assumes "∀y∈R. ∀z∈R. ∀q∈⟨X⟩⇩_{I}. P(q) ⟶ P(y⋅q⋅z)" "∀y∈R. ∀z∈R. P(y) ∧ P(z) ⟶ P(y\<ra>z)" "X ⊆ R" "∀x∈X. P(x)" "X≠0" shows "∀y∈⟨X⟩⇩_{I}. P(y)" proof- let ?J="{m∈⟨X⟩⇩_{I}. P(m)}" have XJ:"X ⊆ ?J" using assms(3,4) generated_ideal_contains_set by auto have sub:"?J ⊆ R" using generated_ideal_is_ideal ideal_dest_subset assms(3) by auto moreover { fix y z assume "y∈R" "z∈?J" then have yz:"z∈⟨X⟩⇩_{I}" "y∈R" "P(z)" "z:R" using sub by auto from assms(1) yz have "P(y⋅z)" using Ring_ZF_1_L2(2) Ring_ZF_1_L3(5)[of "y⋅z"] Ring_ZF_1_L4(3)[of y] by force moreover from assms(1) yz have "P(z⋅y)" using Ring_ZF_1_L2(2) Ring_ZF_1_L3(6) Ring_ZF_1_L4(3)[of _ y] by force moreover from yz(1,2) have "y⋅z∈⟨X⟩⇩_{I}" "z⋅y∈⟨X⟩⇩_{I}" using generated_ideal_is_ideal[OF assms(3)] ideal_dest_mult by auto ultimately have "y⋅z∈?J" "z⋅y∈?J" by auto } then have "∀x∈?J. ∀y∈R. y ⋅ x ∈ ?J ∧ x ⋅ y ∈ ?J" by auto moreover have "IsAsubgroup(?J,A)" proof(rule add_group.group0_3_T3) show "?J≠0" using assms(3-5) generated_ideal_contains_set[OF assms(3)] by force show "?J⊆R" using sub . { fix x assume "x:?J" then have x:"x:⟨X⟩⇩_{I}" "x∈R" "P(x)" using sub by auto moreover have "𝟭:R" using Ring_ZF_1_L2(2). then have "𝟭:R" "(\<rm>𝟭):R" using Ring_ZF_1_L3(1) by auto ultimately have "P((\<rm>𝟭)⋅x⋅𝟭)" using assms(1) by auto then have "P((\<rm>x)⋅𝟭)" using Ring_ZF_1_L3(6)[of x] Ring_ZF_1_L7(1)[of 𝟭 x] `𝟭:R` `x:R` by auto then have "P(\<rm>x)" using Ring_ZF_1_L3(5)[OF Ring_ZF_1_L3(1)] `x:R` by auto moreover from x(1) have "(\<rm>x)∈⟨X⟩⇩_{I}" using generated_ideal_is_ideal[OF assms(3)] ideal_dest_minus by auto ultimately have "(\<rm>x)∈?J" by auto } then show "∀x∈?J. (\<rm> x) ∈ ?J" by auto { fix x y assume as:"x∈?J" "y∈?J" from as have "P(x\<ra>y)" using assms(2) ideal_dest_subset[OF generated_ideal_is_ideal[OF assms(3)]] by auto moreover have "x\<ra>y∈⟨X⟩⇩_{I}" using as generated_ideal_is_ideal[OF assms(3)] ideal_dest_sum by auto ultimately have "x\<ra>y ∈ ?J" by auto } then show "?J {is closed under} A" unfolding IsOpClosed_def by auto qed ultimately have "?J◃R" unfolding Ideal_def by auto with XJ have "⟨X⟩⇩_{I}⊆ ?J" using generated_ideal_small by auto then show ?thesis by auto qed text‹An ideal is very particular with the elements it may contain. If it contains any invertible element, it is in fact the whole ring and not a proper subset› theorem (in ring0) ideal_with_one: assumes "I◃R" "𝟭∈I" shows "I = R" proof- from assms(1) have "I ⊆ R" using ideal_dest_subset by auto moreover { fix t assume t:"t:R" with assms have "t⋅𝟭 ∈I" using ideal_dest_mult(2) by auto with t have "t:I" using Ring_ZF_1_L3(5) by auto } then have "R⊆ I" by auto ultimately show "I=R" by auto qed theorem (in ring0) ideal_with_unit: assumes "I◃R" "x∈I" "∃y∈R. y⋅x = 𝟭 ∨ x⋅y =𝟭" shows "I = R" proof- from assms(3) obtain y where y:"y:R" "y⋅x = 𝟭 ∨ x⋅y =𝟭" by auto from this(1) assms(1,2) have "y⋅x ∈I" "x⋅y∈I" unfolding Ideal_def by auto with y(2) have "𝟭∈I" by auto with ideal_with_one assms(1) show ?thesis by auto qed text‹The previous result drives us to define what a maximal ideal would be: an ideal such that any bigger ideal is the whole ring› definition (in ring0) maximalIdeal ("_◃⇩_{m}R") where "I◃⇩_{m}R ≡ I◃R ∧ I ≠R ∧ (∀J∈ℐ. I⊆J ∧ J≠R ⟶ I=J)" text‹Before delving into maximal ideals, lets define some operation on ideals that are useful when formulating some proofs.› definition (in ring0) productIdeal (infix "⋅⇩_{I}" 90) where "I◃R ⟹ J◃R ⟹ I⋅⇩_{I}J ≡ ⟨M``(I×J)⟩⇩_{I}" definition (in ring0) sumIdeal (infix "+⇩_{I}" 90) where "I◃R ⟹ J◃R ⟹ I+⇩_{I}J ≡ ⟨I∪J⟩⇩_{I}" text‹Some times, we may need to sum an arbitrary number of ideals, and not just two› definition(in ring0) sumArbitraryIdeals ("⊕⇩_{I}_" 90) where "𝒥 ⊆ ℐ ⟹ ⊕⇩_{I}𝒥 ≡ ⟨⋃𝒥⟩⇩_{I}" text‹Every element in the arbitrary sum of ideals is generated by only a finite subset of those ideals› lemma (in ring0) sum_ideals_finite_sum: assumes "𝒥 ⊆ ℐ" "s∈(⊕⇩_{I}𝒥)" shows "∃𝒯∈FinPow(𝒥). s∈(⊕⇩_{I}𝒯)" proof- { assume "⋃𝒥=0" then have "𝒥⊆{0}" by auto then have "Finite(𝒥)" using subset_Finite[OF _ nat_into_Finite[of 1]] by auto then have "𝒥∈FinPow(𝒥)" unfolding FinPow_def by auto then have ?thesis using assms(2) by auto } moreover { assume notE:"⋃𝒥≠0" let ?P= "λt. ∃𝒯∈FinPow(𝒥). t∈(⊕⇩_{I}𝒯)" { fix t assume "t∈⋃𝒥" then obtain J where J:"t∈J" "J∈𝒥" by auto then have "{J}∈FinPow(𝒥)" unfolding FinPow_def using eqpoll_imp_Finite_iff[of "{J}" "1"] nat_into_Finite by auto moreover have "(⊕⇩_{I}{J}) = ⟨J⟩⇩_{I}" using J(2) assms(1) sumArbitraryIdeals_def by auto with J(1) have "t∈(⊕⇩_{I}{J})" using generated_ideal_contains_set[of J] J(2) assms(1) by auto ultimately have "?P(t)" by auto } then have "∀t∈⋃𝒥. ?P(t)" by auto moreover { fix y z q assume q:"?P(q)" "y:R" "z:R" "q:⟨⋃𝒥⟩⇩_{I}" then obtain 𝒯 where T:"𝒯∈FinPow(𝒥)" "q:⊕⇩_{I}𝒯" by auto from T(1) have "⋃𝒯 ⊆ R" "𝒯⊆ℐ" using assms(1) unfolding FinPow_def by auto then have "(⊕⇩_{I}𝒯)◃R" using generated_ideal_is_ideal[of "⋃𝒯"] sumArbitraryIdeals_def[of 𝒯] by auto with T(2) q(2,3) have "y ⋅ q ⋅ z ∈ ⊕⇩_{I}𝒯" unfolding Ideal_def by auto with T(1) have "?P(y ⋅ q ⋅ z)" by auto } then have "∀y∈R. ∀z∈R. ∀q∈⟨⋃𝒥⟩⇩_{I}. ?P(q) ⟶ ?P(y ⋅ q ⋅ z)" by auto moreover { fix y z assume "?P(y)" "?P(z)" then obtain Ty Tz where T:"Ty∈FinPow(𝒥)" "y ∈ ⊕⇩_{I}Ty" "Tz∈FinPow(𝒥)" "z ∈ ⊕⇩_{I}Tz" by auto from T(1,3) have A:"Ty∪Tz:FinPow(𝒥)" unfolding FinPow_def using Finite_Un by auto then have "⋃Ty ⊆ ⋃(Ty∪Tz)" "⋃Tz ⊆ ⋃(Ty∪Tz)" and sub:"⋃(Ty∪Tz) ⊆R" unfolding FinPow_def using assms(1) by auto with A have "⋃Ty ⊆ ⟨⋃(Ty∪Tz)⟩⇩_{I}" "⋃Tz ⊆ ⟨⋃(Ty∪Tz)⟩⇩_{I}" using generated_ideal_contains_set[of "⋃(Ty∪Tz)"] by auto then have "⟨⋃Ty⟩⇩_{I}⊆ ⟨⋃(Ty∪Tz)⟩⇩_{I}" "⟨⋃Tz⟩⇩_{I}⊆ ⟨⋃(Ty∪Tz)⟩⇩_{I}" using generated_ideal_small[OF _ generated_ideal_is_ideal] sub by auto moreover from T(1,3) have Q:"Ty ⊆ℐ" "Tz⊆ ℐ" using assms(1) unfolding FinPow_def by auto moreover note T(2,4) ultimately have "y∈⟨⋃(Ty∪Tz)⟩⇩_{I}" "z∈⟨⋃(Ty∪Tz)⟩⇩_{I}" using sumArbitraryIdeals_def[of "Ty"] sumArbitraryIdeals_def[of "Tz"] by auto then have "y\<ra>z∈⟨⋃(Ty∪Tz)⟩⇩_{I}" using generated_ideal_is_ideal[OF sub] ideal_dest_sum by auto then have "y\<ra>z∈(⊕⇩_{I}(Ty∪Tz))" using sumArbitraryIdeals_def[of "Ty∪Tz"] Q by force with A have "?P(y\<ra>z)" by auto } then have "∀y∈R. ∀z∈R. ?P(y) ∧ ?P(z) ⟶ ?P(y \<ra> z)" by auto moreover have sub:"⋃𝒥 ⊆ R" using assms(1) by auto ultimately have "∀t∈⟨⋃𝒥⟩⇩_{I}. ?P(t)" using induction_generated_ideal[of "⋃𝒥" ?P] notE by blast with assms(2) have ?thesis unfolding sumArbitraryIdeals_def[OF assms(1)] by auto } ultimately show ?thesis by auto qed text‹By definition of product of ideals and of an ideal itself, it follows that the product of ideals is an ideal contained in the intersection› theorem (in ring0) product_in_intersection: assumes "I◃R" "J◃R" shows "I⋅⇩_{I}J ⊆ I∩J" and "(I⋅⇩_{I}J)◃R" and "M``(I×J) ⊆ I⋅⇩_{I}J" proof- have s:"M``(I×J) ⊆ I∩J" proof fix x assume x:"x∈M``(I×J)" then obtain y where "y:I×J" "⟨y,x⟩∈M" unfolding image_def by auto then obtain yi yj where y:"yi:I" "yj:J" "⟨⟨yi,yj⟩,x⟩∈M" by auto then have "yi⋅yj:I" "yi⋅yj:J" using assms ideal_dest_subset[of I] ideal_dest_subset[of J] unfolding Ideal_def by auto with y(3) show "x∈I∩J" using apply_equality[of _ x M] using ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto qed moreover have "(I∩J) ◃R" using intersection_ideals[of "{I,J}"] assms by auto ultimately show "I⋅⇩_{I}J ⊆ I∩J" unfolding productIdeal_def[OF assms] using generated_ideal_small by auto from s have q:"M``(I×J) ⊆ R" using assms ideal_dest_subset by auto with generated_ideal_is_ideal show "(I⋅⇩_{I}J) ◃R" unfolding productIdeal_def[OF assms] by auto from q show "M``(I×J) ⊆ I⋅⇩_{I}J" using generated_ideal_contains_set unfolding productIdeal_def[OF assms] by auto qed text‹We will show now that the sum of ideals is no more that the sum of the ideal elements› lemma (in ring0) sum_elements: assumes "I ◃R" "J ◃R" "x ∈ I" "y ∈ J" shows "x\<ra>y ∈ I+⇩_{I}J" proof- from assms(1,2) have "I∪J ⊆ R" using ideal_dest_subset by auto moreover have "x∈ I∪J" "y∈ I∪J" using assms(3,4) by auto ultimately have "x ∈ ⟨I∪J⟩⇩_{I}" "y ∈ ⟨I∪J⟩⇩_{I}" using generated_ideal_contains_set by auto moreover have "⟨I∪J⟩⇩_{I}◃R" using generated_ideal_is_ideal[of "I∪J"] assms(1,2) using ideal_dest_subset[of I] ideal_dest_subset[of J] by auto ultimately have "x\<ra>y∈⟨I∪J⟩⇩_{I}" using ideal_dest_sum by auto then show ?thesis using sumIdeal_def assms(1,2) by auto qed lemma (in ring0) sum_elements_is_ideal: assumes "I ◃R" "J ◃R" shows "(A``(I×J)) ◃R" proof- have a:"A:R×R → R" using add_group.groupAssum IsAgroup_def IsAmonoid_def IsAssociative_def by simp from assms have ij:"I×J ⊆ R×R" using ideal_dest_subset by auto from a have Aimage:"A``(I×J) ⊆ R" using func1_1_L6(2) by auto moreover { fix x y assume xy:"x∈R" "y∈A``(I×J)" from ij xy(2) obtain z where "y=A`z" "z∈I×J" using func_imagedef[OF a, of "I×J"] by auto then obtain yi yj where y:"y=yi\<ra>yj" "yi∈I" "yj∈J" by auto from y(1) have "x⋅y = x⋅(yi\<ra>yj)" "y⋅x = (yi\<ra>yj)⋅x" by auto then have "x⋅y = (x⋅yi)\<ra>(x⋅yj)" "y⋅x = (yi⋅x)\<ra>(yj⋅x)" using ring_oper_distr xy(1) y ij add_group.group_op_closed by auto moreover have "x⋅yi ∈ I" "yi⋅x ∈ I" "x⋅yj ∈ J" "yj⋅x ∈ J" using assms xy(1) y(2,3) ideal_dest_mult by auto ultimately have "x⋅y∈A``(I×J)" "y⋅x∈A``(I×J)" using func_imagedef[OF a, of "I×J"] ij by auto } then have "∀x∈A``(I×J). ∀y∈R. y ⋅ x ∈ A``(I×J) ∧ x ⋅ y ∈ A``(I×J)" by auto moreover have "IsAsubgroup(A``(I×J),A)" proof(rule add_group.group0_3_T3) show AsubR:"A `` (I × J) ⊆ R" using Aimage. { fix x assume "x∈A `` (I × J)" then obtain z where "x=A`z" "z∈I×J" using func_imagedef[OF a, of "I×J"] ij by auto then obtain xi xj where x:"xi∈I" "xj∈J" "x=xi\<ra>xj" by auto from x(3) have "(\<rm>x) = \<rm>(xi\<ra>xj)" by auto then have "(\<rm>x) = (\<rm>xi)\<rs>xj" using Ring_ZF_1_L9(2) assms x(1,2) ideal_dest_subset by auto moreover have "(\<rm>xi)∈I" using assms(1) ideal_dest_minus x(1) by auto moreover have "(\<rm>xj)∈J" using assms(2) ideal_dest_minus x(2) by auto ultimately have "(\<rm>x) ∈ A``(I×J)" using func_imagedef[OF a, of "I×J"] ij by auto } then show "∀x∈A `` (I × J). (\<rm> x) ∈ A `` (I × J)" by auto have "𝟬∈I" "𝟬∈J" using ideal_dest_zero assms by auto then have "𝟬\<ra>𝟬 ∈ A `` (I × J)" using func_imagedef[OF a, of "I×J"] ij by auto then show "A `` (I × J) ≠ 0" by auto { fix x y assume xy:"x∈ A `` (I × J)" "y∈ A `` (I × J)" then obtain z g where "x=A`z" "z∈I×J" "y=A`g" "g∈I×J" using func_imagedef[OF a, of "I×J"] ij by auto then obtain xi xj yi yj where x:"xi∈I" "xj∈J" "x=xi\<ra>xj" "yi∈I" "yj∈J" "y=yi\<ra>yj" by auto have "x\<ra>y = (x\<ra>yi)\<ra>yj" using xy(1) AsubR x(4-6) ij Ring_ZF_1_L10(1)[of x yi yj] by force then have "x\<ra>y = (xi\<ra>yi)\<ra>(xj\<ra>yj)" using x(1-5) ij Ring_ZF_2_L5(4)[of xi xj yi yj] by auto moreover have "xi\<ra>yi ∈ I" using x(1,4) assms(1) ideal_dest_sum by auto moreover have "xj\<ra>yj ∈ J" using x(2,5) assms(2) ideal_dest_sum by auto ultimately have "x\<ra>y ∈ A``(I×J)" using func_imagedef[OF a, of "I×J"] ij by auto } then show "A `` (I × J) {is closed under} A" unfolding IsOpClosed_def by auto qed ultimately show "(A `` (I × J))◃R" unfolding Ideal_def by auto qed corollary (in ring0) sum_ideals_is_sum_elements: assumes "I ◃R" "J ◃R" shows "(A `` (I × J)) = I+⇩_{I}J" proof have a:"A:R×R → R" using add_group.groupAssum IsAgroup_def IsAmonoid_def IsAssociative_def by simp from assms have ij:"I⊆R" "J ⊆ R" using ideal_dest_subset by auto then have ij_prd:"I×J ⊆ R×R" by auto then show "A `` (I × J) ⊆ I +⇩_{I}J" using sum_elements[OF assms] func_imagedef[OF a, of "I×J"] by auto { fix x assume x:"x∈I" with ij(1) have "x=x\<ra>𝟬" using Ring_ZF_1_L3(3)[of x] by auto then have "x∈A `` (I × J)" using x assms(2) add_group.group0_3_L5[of J] unfolding Ideal_def using func_imagedef[OF a, of "I×J"] ij_prd by auto } then have "I ⊆ A `` (I × J)" by auto moreover { fix x assume x:"x∈J" with ij(2) have "x=𝟬\<ra>x" using Ring_ZF_1_L3(4)[of x] by auto then have "x∈A `` (I × J)" using x assms(1) add_group.group0_3_L5[of I] unfolding Ideal_def using func_imagedef[OF a, of "I×J"] ij_prd by auto } then have "J ⊆ A `` (I × J)" by auto ultimately have "I∪J ⊆ A `` (I × J)" by auto then show "I+⇩_{I}J ⊆ A `` (I × J)" using generated_ideal_small sum_elements_is_ideal[OF assms] assms sumIdeal_def by auto qed corollary (in ring0) sum_ideals_is_ideal: assumes "I ◃R" "J ◃R" shows "(I +⇩_{I}J) ◃R" using assms sum_ideals_is_sum_elements sum_elements_is_ideal ideal_dest_subset by auto corollary (in ring0) sum_ideals_commute: assumes "I◃R" "J◃R" shows "(I +⇩_{I}J) = (J +⇩_{I}I)" proof- have "I ∪ J = J ∪ I" by auto then show ?thesis unfolding sumIdeal_def[OF assms] sumIdeal_def[OF assms(2,1)] by auto qed text‹Now that we know what the product of ideals is, we are able to define what a prime ideal is:› definition (in ring0) primeIdeal ("_◃⇩_{p}R") where "P◃⇩_{p}R ≡ P◃R ∧ P≠R ∧ (∀I∈ℐ. ∀J∈ℐ. I ⋅⇩_{I}J ⊆ P ⟶ (I ⊆ P ∨ J ⊆ P))" text‹Any maximal ideal is prime› theorem (in ring0) maximal_is_prime: assumes "Q◃⇩_{m}R" shows "Q◃⇩_{p}R" proof- have a:"A:R×R → R" using add_group.groupAssum IsAgroup_def IsAmonoid_def IsAssociative_def by simp have MI:"Q ∈ ℐ" using assms unfolding maximalIdeal_def using ideal_dest_subset by auto { fix I J assume ij:"I∈ℐ" "J∈ℐ" "I ⋅⇩_{I}J ⊆ Q" { assume K:"¬(I⊆Q)" "¬(J⊆Q)" from this(1) obtain x where x:"x∈I-Q" by auto then have xR:"x∈R" using ij(1) ideal_dest_subset by auto let ?K = "⟨Q∪{x}⟩⇩_{I}" have MK:"Q ⊆ ?K" "x∈?K" using generated_ideal_contains_set[of "Q∪{x}"] assms unfolding maximalIdeal_def using ideal_dest_subset[of Q] xR by auto with x have "Q ⊆ ?K" "?K≠Q" by auto with assms have "?K∈ℐ ⟹ ?K=R" unfolding maximalIdeal_def by auto then have KR:"?K=R" using generated_ideal_is_ideal[of "Q∪{x}"] xR assms unfolding maximalIdeal_def using ideal_dest_subset[of Q] ideal_dest_subset[of "⟨Q∪{x}⟩⇩_{I}"] by auto let ?P="Q+⇩_{I}I" have "Q∪I ⊆ Q+⇩_{I}I" using generated_ideal_contains_set[of "Q∪I"] sumIdeal_def[of Q I] assms ij(1) maximalIdeal_def using ideal_dest_subset by auto then have "Q∪{x} ⊆ Q+⇩_{I}I" using x by auto then have "?K ⊆ Q+⇩_{I}I" "Q+⇩_{I}I ⊆R" using generated_ideal_small[of "Q∪{x}" "Q+⇩_{I}I"] generated_ideal_is_ideal[of "Q∪I"] sumIdeal_def[of Q I] ij(1) assms unfolding maximalIdeal_def using ideal_dest_subset by auto with KR have "Q+⇩_{I}I = R" by auto then have "𝟭∈Q+⇩_{I}I " using Ring_ZF_1_L2(2) by auto then have "𝟭∈A``(Q×I)" using sum_ideals_is_sum_elements MI ij(1) by auto moreover have "Q×I ⊆ R×R" using MI ij(1) by auto ultimately obtain xm xi where mi1:"xm∈Q" "xi∈I" "𝟭=xm\<ra>xi" using func_imagedef[OF a, of "Q×I"] by auto { fix y assume y:"y∈J" then have "𝟭⋅y = y" using Ring_ZF_1_L3(6) ij(2) by auto with mi1(3) have "(xm\<ra>xi)⋅y = y" by auto moreover have elems:"y:R" "xm:R" "xi:R" using y mi1(1,2) MI ij(1,2) by auto ultimately have "(xm⋅y)\<ra>(xi⋅y) = y" using ring_oper_distr(2)[of y xm xi] by auto moreover have "xm⋅y:Q" using mi1(1) elems(1) MI ideal_dest_mult(1) by auto moreover have sub:"I×J ⊆ R×R" using ij(1,2) by auto have MR:"M:R×R→R" using ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto from sub MR have "xi⋅y:M``(I×J)" using func_imagedef[of M "R×R" R "I×J"] y mi1(2) by auto then have "xi⋅y:I⋅⇩_{I}J" using generated_ideal_contains_set[of "M``(I×J)"] func1_1_L6(2)[OF MR] productIdeal_def ij(1,2) by auto with ij(3) have "xi⋅y:Q" by auto ultimately have "y∈Q" using MI ideal_dest_sum by force } then have "J ⊆ Q" by auto with K have False by auto } then have "(I⊆Q)∨(J⊆Q)" by auto } then have "∀I∈ℐ. ∀J∈ℐ. I ⋅⇩_{I}J ⊆ Q ⟶ (I ⊆ Q ∨ J ⊆ Q)" by auto then show ?thesis using assms unfolding maximalIdeal_def primeIdeal_def by auto qed text‹In case of non-commutative rings, the zero divisor concept is too constrictive. For that we define the following concept of a prime ring. Note that in case that our ring is commutative, this is equivalent to having no zero divisors (there is no proof yet)› definition primeRing ("[_,_,_]{is a prime ring}") where "IsAring(R,A,M) ⟹ [R,A,M]{is a prime ring} ≡ (∀x∈R. ∀y∈R. (∀z∈R. M`⟨M`⟨x,z⟩,y⟩ = TheNeutralElement(R,A)) ⟶ x =TheNeutralElement(R,A) ∨ y=TheNeutralElement(R,A))" text‹Prime rings appear when the zero ideal is prime› lemma (in ring0) prime_ring_zero_prime_ideal: assumes "[R,A,M]{is a prime ring}" "R≠{𝟬}" shows "{𝟬}◃⇩_{p}R" proof- have MR:"M:R×R→R" using ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto { fix I J assume ij:"I∈ℐ" "J∈ℐ" "I ⋅⇩_{I}J ⊆ {𝟬}" from ij(1,2) have ij_rr:"I×J ⊆ R×R" by auto { assume "¬(I⊆{𝟬})" "¬(J⊆{𝟬})" then obtain xi xj where x:"xi≠𝟬" "xj≠𝟬" "xi∈I" "xj:J" by auto { fix u assume "u∈R" with x(3) have "xi⋅u∈I" using ij(1) ideal_dest_mult(1) by auto with x(4) have "xi⋅u⋅xj:M``(I×J)" using func_imagedef[OF MR] ij_rr by auto then have "xi⋅u⋅xj:I ⋅⇩_{I}J" using generated_ideal_contains_set[of "M `` (I × J)"] func1_1_L6(2)[OF MR, of "I×J"] productIdeal_def ij(1,2) by auto with ij(3) have "xi⋅u⋅xj = 𝟬" by auto } then have "∀u∈R. xi⋅u⋅xj = 𝟬" by auto moreover have "xi∈R" "xj∈R" using ij(1,2) x(3,4) by auto moreover note assms(1) ultimately have False using x(1,2) unfolding primeRing_def[OF ringAssum] by auto } then have "I⊆{𝟬} ∨ J⊆{𝟬}" by auto } then have "∀I∈ℐ. ∀J∈ℐ. I ⋅⇩_{I}J ⊆ {𝟬} ⟶ (I ⊆ {𝟬} ∨ J ⊆ {𝟬})" by auto moreover note zero_ideal assms(2) ultimately show ?thesis unfolding primeIdeal_def by auto qed lemma (in ring0) zero_prime_ideal_prime_ring: assumes "{𝟬}◃⇩_{p}R" shows "[R,A,M]{is a prime ring}" proof- have MR:"M:R×R→R" using ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto { fix x y z assume as:"x∈R" "y∈R" "∀z∈R. x⋅z⋅y = 𝟬" let ?X="⟨{x}⟩⇩_{I}" let ?Y="⟨{y}⟩⇩_{I}" have "?X⊆R" "?Y⊆R" using generated_ideal_is_ideal ideal_dest_subset as(1,2) by auto then have XY:"?X×?Y ⊆ R×R" by auto let ?P="λq. (∀z∈?Y. q⋅z = 𝟬)" let ?Q="λq. (∀z∈R. x⋅z⋅q =𝟬)" have Y:"∀y∈?Y. ?Q(y)" proof(rule induction_generated_ideal) show "{y}⊆R" "{y}≠0" using as(2) by auto show "∀xa∈{y}. ∀z∈R. x ⋅ z ⋅ xa = 𝟬" using as(3) by auto { fix s t q assume yzq:"s:R" "t:R" "q:⟨{y}⟩⇩_{I}" "∀k∈R. x ⋅ k ⋅ q = 𝟬" from yzq(3) have q:"q∈R" using generated_ideal_is_ideal ideal_dest_subset as(2) by auto { fix u assume "u:R" have "x ⋅ u ⋅ (s ⋅ q ⋅ t) = (x ⋅ (u⋅s)⋅q)⋅t" using Ring_ZF_1_L11(2) yzq(1-2) q `u:R` as(1) Ring_ZF_1_L4(3) by auto moreover have "u⋅s:R" using `u:R` yzq(1) Ring_ZF_1_L4(3) by auto moreover note yzq(4) ultimately have "x ⋅ u ⋅ (s ⋅ q ⋅ t) = 𝟬⋅t" by auto then have "x ⋅ u ⋅ (s ⋅ q ⋅ t) = 𝟬" using yzq(2) Ring_ZF_1_L6(1) by auto } then have "∀za∈R. x ⋅ za ⋅ (s ⋅ q ⋅ t) = 𝟬" by auto } then show "∀t∈R. ∀z∈R. ∀q∈⟨{y}⟩⇩_{I}. (∀z∈R. x ⋅ z ⋅ q = 𝟬) ⟶ (∀za∈R. x ⋅ za ⋅ (t ⋅ q ⋅ z) = 𝟬)" by auto { fix s t assume st:"s:R" "t:R" "∀k∈R. x ⋅ k ⋅ s = 𝟬" "∀k∈R. x ⋅ k ⋅ t = 𝟬" { fix u assume "u:R" have "x ⋅ u ⋅ (s \<ra> t) = (x ⋅ u ⋅ s) \<ra>(x ⋅ u ⋅ t)" using ring_oper_distr(1) `u:R` as(1) st(1,2) Ring_ZF_1_L4(3) by auto with st(3,4) `u:R` have "x ⋅ u ⋅ (s \<ra> t) = 𝟬 \<ra> 𝟬" by auto then have "x ⋅ u ⋅ (s \<ra> t) = 𝟬" using Ring_ZF_1_L3(3) Ring_ZF_1_L2(1) by auto } then have "∀za∈R. x ⋅ za ⋅ (s \<ra> t) = 𝟬" by auto } then show "∀y∈R. ∀z∈R. (∀z∈R. x ⋅ z ⋅ y = 𝟬) ∧ (∀za∈R. x ⋅ za ⋅ z = 𝟬) ⟶ (∀za∈R. x ⋅ za ⋅ (y \<ra> z) = 𝟬)" by auto qed { fix yy assume "yy:?Y" with Y have "∀z∈R. x ⋅ z ⋅ yy = 𝟬" by auto then have "x⋅yy = 𝟬" using Ring_ZF_1_L2(2) Ring_ZF_1_L3(5) as(1) by auto } then have z:"∀y∈?Y. x⋅y = 𝟬" by auto have yy:"?Y◃R" "?Y ⊆ R" using generated_ideal_is_ideal as(2) ideal_dest_subset by auto have xy:"∀y∈?X. ?P(y)" proof(rule induction_generated_ideal) show "{x}⊆R" "{x}≠0" using as(1) by auto from z show "∀x∈{x}. ∀z∈⟨{y}⟩⇩_{I}. x ⋅ z = 𝟬" by auto { fix q1 q2 q3 assume q:"q1:R" "q2:R" "q3:⟨{x}⟩⇩_{I}" "∀k∈?Y. q3 ⋅ k = 𝟬" have q3:"q3∈R" using q(3) generated_ideal_is_ideal as(1) ideal_dest_subset by auto { fix q4 assume q4:"q4∈?Y" from yy q4 q(2) have "q2 ⋅ q4 :?Y" using ideal_dest_mult(2) by auto moreover have "q1 ⋅ q3 ⋅ q2 ⋅ q4 = q1 ⋅ (q3 ⋅ (q2 ⋅ q4))" using q(1-2) q3 q4 yy(2) Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) by auto moreover note q(4) ultimately have "q1 ⋅ q3 ⋅ q2 ⋅ q4 = q1 ⋅ 𝟬" by auto then have "q1 ⋅ q3 ⋅ q2 ⋅ q4 = 𝟬" using Ring_ZF_1_L6(2) q(1) by auto } then have "∀za∈⟨{y}⟩⇩_{I}. q1 ⋅ q3 ⋅ q2 ⋅ za = 𝟬" by auto } then show "∀ya∈R. ∀z∈R. ∀q∈⟨{x}⟩⇩_{I}. (∀z∈⟨{y}⟩⇩_{I}. q ⋅ z = 𝟬) ⟶ (∀za∈⟨{y}⟩⇩_{I}. ya ⋅ q ⋅ z ⋅ za = 𝟬)" by auto { fix q1 q2 assume q:"q1:R" "q2:R" "∀z∈⟨{y}⟩⇩_{I}. q1 ⋅ z = 𝟬" "∀za∈⟨{y}⟩⇩_{I}. q2 ⋅ za = 𝟬" { fix q3 assume "q3∈?Y" have "(q1 \<ra> q2) ⋅ q3 = (q1⋅q3) \<ra> (q2⋅q3)" using ring_oper_distr(2) q(1,2) `q3:?Y` yy(2) by auto with q(3,4) have "(q1 \<ra> q2) ⋅ q3 = 𝟬 \<ra> 𝟬" using `q3:?Y` by auto then have "(q1 \<ra> q2) ⋅ q3 = 𝟬" using Ring_ZF_1_L3(3) Ring_ZF_1_L2(1) by auto } then have "∀q∈?Y. (q1 \<ra> q2) ⋅ q = 𝟬" by auto } then show "∀ya∈R. ∀z∈R. (∀z∈⟨{y}⟩⇩_{I}. ya ⋅ z = 𝟬) ∧ (∀za∈⟨{y}⟩⇩_{I}. z ⋅ za = 𝟬) ⟶ (∀za∈⟨{y}⟩⇩_{I}. (ya \<ra> z) ⋅ za = 𝟬)" by auto qed { fix q assume "q∈M``(?X×?Y)" then obtain qx qy where q:"qx:?X" "qy:?Y" "q=qx⋅qy" using func_imagedef[OF MR XY] by auto with xy have "q=𝟬" by auto } then have "M``(?X×?Y) ⊆ {𝟬}" by auto then have "?X⋅⇩_{I}?Y ⊆ {𝟬}" using generated_ideal_small zero_ideal productIdeal_def generated_ideal_is_ideal as(1,2) by auto then have "?X ⊆ {𝟬} ∨ ?Y ⊆ {𝟬}" using assms unfolding primeIdeal_def using generated_ideal_is_ideal as(1,2) ideal_dest_subset by auto then have "x=𝟬 ∨ y =𝟬" using generated_ideal_contains_set as(1,2) by auto } then have " ∀x∈R. ∀y∈R. (∀z∈R. x ⋅ z ⋅ y = 𝟬) ⟶ x = 𝟬 ∨ y = 𝟬" by auto then show ?thesis unfolding primeRing_def[OF ringAssum] by auto qed text‹We can actually use this definition of a prime ring, as a condition to check for prime ideals.› theorem (in ring0) equivalent_prime_ideal: assumes "P◃⇩_{p}R" shows "∀x∈R. ∀y∈R. (∀z∈R. x⋅z⋅y∈P) ⟶ x∈P ∨ y∈P" proof(safe) fix x y assume as:"x∈R" "y∈R" "∀z∈R. x⋅z⋅y∈P" "y∉P" let ?X="⟨{x}⟩⇩_{I}" let ?Y="⟨{y}⟩⇩_{I}" from as(3) have "∀x∈{x}. ∀u∈R. x ⋅ u ⋅ y ∈ P" by auto moreover have "∀ya∈R. ∀z∈R. ∀q∈?X. (∀u∈R. q ⋅ u ⋅ y ∈ P) ⟶ (∀u∈R. ya ⋅ q ⋅ z ⋅ u ⋅ y ∈ P)" proof(safe) fix ya z q u assume ass:"ya∈R" "z∈R" "q∈?X" "∀u∈R. q ⋅ u ⋅ y ∈ P" "u ∈ R" from ass(3) have q:"q∈R" using generated_ideal_is_ideal[THEN ideal_dest_subset] as(1) by auto from ass(2,5) have "z⋅u∈R" using Ring_ZF_1_L4(3) by auto with ass(4) have "q⋅(z⋅u)⋅y:P" by auto with ass(1) have "ya⋅(q⋅(z⋅u)⋅y)∈P" using assms unfolding primeIdeal_def using ideal_dest_mult(2) by auto then show "ya⋅q⋅z⋅u⋅y∈P" using Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) ass(1,2,5) as(2) q by auto qed moreover have "∀ya∈R. ∀z∈R. (∀u∈R. ya ⋅ u ⋅ y ∈ P) ∧ (∀u∈R. z ⋅ u ⋅ y ∈ P) ⟶ (∀u∈R. (ya \<ra> z) ⋅ u ⋅ y ∈ P)" proof(safe) fix ya z u assume ass:"ya∈R" "z∈R" "u∈R" "∀u∈R. ya ⋅ u ⋅ y ∈ P" "∀u∈R. z ⋅ u ⋅ y ∈ P" from ass(3-5) have "ya ⋅ u ⋅ y ∈ P" "z ⋅ u ⋅ y ∈ P" by auto then have "(ya ⋅ u ⋅ y)\<ra>(z ⋅ u ⋅ y) ∈ P" using ideal_dest_sum assms unfolding primeIdeal_def by auto then have "((ya⋅u)\<ra>(z⋅u))⋅y∈P" using ring_oper_distr(2) as(2) Ring_ZF_1_L4(3) ass(1-3) by auto then show "((ya\<ra>z)⋅u)⋅y∈P" using ring_oper_distr(2) ass(1-3) by auto qed ultimately have R:"∀ya∈⟨{x}⟩⇩_{I}. ∀u∈R. ya ⋅ u ⋅ y ∈ P" using induction_generated_ideal[of "{x}" "λt. ∀u∈R. t⋅u⋅y ∈ P"] as(1) by auto then have "∀xa∈{y}. ∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ xa ∈ P" by auto moreover have "∀ya∈R. ∀z∈R. ∀q∈⟨{y}⟩⇩_{I}. (∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ q ∈ P) ⟶ (∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ (ya ⋅ q ⋅ z) ∈ P)" proof(safe) fix ya z q t u assume ass:"ya∈R" "z∈R" "q∈?Y" "∀t∈?X. ∀u∈R. t ⋅ u ⋅ q ∈ P" "t∈?X" "u∈R" from ass(3,5) have qt:"q:R" "t∈R" using generated_ideal_is_ideal ideal_dest_subset as(1,2) by auto from ass(1,6) have "u⋅ya:R" using Ring_ZF_1_L4(3) by auto with ass(4,5) have "t⋅(u⋅ya)⋅q ∈P" by auto then have "(t⋅(u⋅ya)⋅q)⋅z∈P" using ass(2) assms ideal_dest_mult(1) unfolding primeIdeal_def by auto then show "t ⋅ u ⋅ (ya ⋅ q ⋅ z) ∈P" using Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) ass(1,2,6) qt by auto qed moreover have "∀y∈R. ∀z∈R. (∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ y ∈ P) ∧ (∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ z ∈ P) ⟶ (∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ (y \<ra> z) ∈ P)" proof(safe) fix ya z t u assume ass:"ya∈R" "z∈R" "t∈?X" "u∈R" "∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ ya ∈ P" "∀t∈⟨{x}⟩⇩_{I}. ∀u∈R. t ⋅ u ⋅ z ∈ P" from ass(3) have "t∈R" using ideal_dest_subset generated_ideal_is_ideal as(1) by auto from ass(3-6) have "t ⋅ u ⋅ ya ∈ P" "t ⋅ u ⋅ z ∈ P" by auto then have "(t ⋅ u ⋅ ya)\<ra>(t ⋅ u ⋅ z) ∈P" using assms unfolding primeIdeal_def using ideal_dest_sum by auto then have "t⋅((u⋅ya)\<ra>(u⋅z)) ∈P" using ring_oper_distr(1) `t∈R` Ring_ZF_1_L4(3) ass(4,2,1) Ring_ZF_1_L11 by auto then have "t⋅(u⋅(ya\<ra>z)) ∈P" using ring_oper_distr(1) ass(1,2,4) by auto then show "t⋅u⋅(ya\<ra>z) ∈P" using Ring_ZF_1_L11(2) Ring_ZF_1_L4(1) ass(1,2,4) `t∈R` by auto qed ultimately have R:"∀q∈?Y. ∀t∈?X. ∀u∈R. t⋅u⋅q ∈ P" using induction_generated_ideal[of "{y}" "λq. ∀t∈?X. ∀u∈R. t⋅u⋅q ∈ P"] as(2) by auto have "?X⊆R" "?Y⊆R" using ideal_dest_subset generated_ideal_is_ideal as(1,2) by auto then have subprd:"?X×?Y ⊆ R×R" by auto { fix t assume "t∈M``(?X×?Y)" then obtain tx ty where t:"tx∈?X" "ty∈?Y" "t= tx⋅ty" using func_imagedef[of M "R×R" R "?X×?Y"] subprd ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto from this(1,2) have "tx⋅𝟭⋅ty ∈P" using R Ring_ZF_1_L2(2) by auto moreover from t(1) have "tx∈R" using generated_ideal_is_ideal[THEN ideal_dest_subset] as(1) by auto ultimately have "t∈P" using Ring_ZF_1_L3(5) t(3) by auto } then have "M``(?X×?Y) ⊆ P" by auto then have "?X⋅⇩_{I}?Y ⊆ P" using generated_ideal_small assms unfolding primeIdeal_def using productIdeal_def[ OF generated_ideal_is_ideal generated_ideal_is_ideal] as(1,2) by auto moreover have "?X:ℐ" "?Y:ℐ" using generated_ideal_is_ideal generated_ideal_is_ideal[THEN ideal_dest_subset] as(1,2) by auto ultimately have "?X ⊆ P ∨ ?Y ⊆ P" using assms unfolding primeIdeal_def by auto with as(4) generated_ideal_contains_set as(2) have "?X ⊆ P" by auto then show "x∈P" using generated_ideal_contains_set as(1) by auto qed theorem (in ring0) equivalent_prime_ideal_2: assumes "∀x∈R. ∀y∈R. (∀z∈R. x⋅z⋅y∈P) ⟶ x∈P ∨ y∈P" "P◃R" "P≠R" shows "P◃⇩_{p}R" unfolding primeIdeal_def apply(safe) using assms(2) apply simp using assms(3) apply simp proof- fix I J x xa assume as:"I◃R" "I⊆R" "J◃R" "J⊆R" "I ⋅⇩_{I}J ⊆ P" "x ∈ J" "x ∉ P" "xa ∈ I" from as(4,2) have prdsub:"I×J ⊆ R×R" by auto { fix z assume z:"z∈R" then have "xa⋅z∈I" using as(1,8) ideal_dest_mult(1) by auto then have "⟨xa⋅z,x⟩∈I×J" using as(6) by auto then have "(xa⋅z⋅x)∈M``(I×J)" using func_imagedef[of M "R×R" R "I×J"] prdsub ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto then have "(xa⋅z⋅x)∈⟨M``(I×J)⟩⇩_{I}" using generated_ideal_contains_set [OF func1_1_L6(2)[of M "R×R" R]] ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by force then have "(xa⋅z⋅x)∈ I⋅⇩_{I}J" using productIdeal_def as(1,3) by auto with as(5) have "xa⋅z⋅x∈P" by auto } then have "∀z∈R. xa⋅z⋅x ∈ P" by auto moreover have "xa∈R" "x∈R" using as(2,4,6,8) by auto with assms(1) have "(∀z∈R. xa ⋅ z ⋅ x ∈ P) ⟶ x ∈ P ∨ xa ∈ P" by auto ultimately have "x∈P ∨ xa∈P" by auto with as(7) show "xa∈P" by auto qed subsection‹Ring quotient› text‹Similar to groups, rings can be quotiented by normal additive subgroups; but to keep the structure of the multiplicative monoid we need extra structure in the normal subgroup. This extra structure is given by the ideal.› text‹Any ideal is a normal subgroup› lemma (in ring0) ideal_normal_add_subgroup: assumes "I◃R" shows "IsAnormalSubgroup(R,A,I)" using Group_ZF_2_4_L6(1) using ringAssum unfolding IsAring_def using assms unfolding Ideal_def by auto definition (in ring0) QuotientBy where "I◃R ⟹ QuotientBy(I) ≡ R//QuotientGroupRel(R,A,I)" text‹Any ideal gives rise to an equivalent relation› corollary (in ring0) equiv_rel: assumes "I◃R" shows "equiv(R,QuotientGroupRel(R,A,I))" using assms add_group.Group_ZF_2_4_L3 unfolding Ideal_def by auto text‹Any quotient by an ideal is an abelian group› lemma (in ring0) quotientBy_add_group: assumes "I◃R" shows "IsAgroup(QuotientBy(I), QuotientGroupOp(R, A, I))" and "QuotientGroupOp(R, A, I) {is commutative on} QuotientBy(I)" proof- from Group_ZF_2_4_T1[of R A I] show "IsAgroup(QuotientBy(I), QuotientGroupOp(R, A, I))" using ideal_normal_add_subgroup[OF assms] ringAssum unfolding QuotientBy_def[OF assms] IsAring_def by auto from Group_ZF_2_4_L6(2) show "QuotientGroupOp(R, A, I) {is commutative on} QuotientBy(I)" using ringAssum unfolding IsAring_def QuotientBy_def[OF assms] using assms unfolding Ideal_def by auto qed text‹The multiplicative monoid is congruent with the quotient relation and gives rise to a monoid in the quotient› lemma (in ring0) quotientBy_mul_monoid: assumes "I◃R" shows "Congruent2(QuotientGroupRel(R, A, I),M)" and "IsAmonoid(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R,A,I), M))" proof- { fix x y s t assume "⟨x,y⟩∈QuotientGroupRel(R,A,I)" "⟨s,t⟩∈QuotientGroupRel(R,A,I)" then have xyst:"x∈R" "y∈R" "s∈R" "t∈R" "x\<rs>y ∈I" "s\<rs>t ∈I" unfolding QuotientGroupRel_def by auto have "(x⋅s)\<rs>(y⋅t) = (x⋅s)\<ra>𝟬\<rs>(y⋅t)" using Ring_ZF_1_L3(3) Ring_ZF_1_L4(3)[OF xyst(1,3)] by auto then have "(x⋅s)\<rs>(y⋅t) = ((x⋅s)\<ra>((\<rm>(y⋅s))\<ra>(y⋅s)))\<rs>(y⋅t)" using Ring_ZF_1_L3(7)[of "y⋅s"] Ring_ZF_1_L4(3)[OF xyst(2,3)] Ring_ZF_1_L4(4)[of "\<rm>(y⋅s)" "y⋅s"] Ring_ZF_1_L3(1)[of "y⋅s"] by auto then have "(x⋅s)\<rs>(y⋅t) = ((x⋅s)\<rs>(y⋅s))\<ra>((y⋅s)\<rs>(y⋅t))" using Ring_ZF_1_L3(1) Ring_ZF_1_L4(1,2) Ring_ZF_1_L10(1)[of "x⋅s" "\<rm>(y⋅s)" "y⋅s"] Ring_ZF_1_L10(1)[of "(x⋅s)\<rs>(y⋅s)" "y⋅s" "\<rm>(y⋅t)"] Ring_ZF_1_L4(3)[OF xyst(1,3)] Ring_ZF_1_L4(3)[OF xyst(2,3)] Ring_ZF_1_L4(3)[OF xyst(2,4)] by auto then have "(x⋅s)\<rs>(y⋅t) = ((x\<rs>y)⋅s)\<ra>(y⋅(s\<rs>t))" using Ring_ZF_1_L8 xyst(1-4) by auto moreover have "(x\<rs>y)⋅s ∈I" using xyst(3,5) assms ideal_dest_mult(1) by auto moreover have "y⋅(s\<rs>t) ∈I" using xyst(2,6) assms ideal_dest_mult(2) by auto ultimately have "(x⋅s)\<rs>(y⋅t) ∈I" using assms ideal_dest_sum by auto then have "⟨M ` ⟨x, s⟩, M ` ⟨y, t⟩⟩ ∈ QuotientGroupRel(R, A, I)" unfolding QuotientGroupRel_def using Ring_ZF_1_L4(3) xyst(1-4) by auto } then show "Congruent2(QuotientGroupRel(R, A, I),M)" unfolding Congruent2_def by auto moreover have "equiv(R,QuotientGroupRel(R,A,I))" using add_group.Group_ZF_2_4_L3 assms unfolding Ideal_def by auto moreover note mult_monoid.Group_ZF_2_2_T1 ultimately show "IsAmonoid(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R,A,I), M))" unfolding QuotientBy_def[OF assms] by auto qed definition (in ring0) ideal_radd ("_{\<ra>_}_") where "x{\<ra>I}y ≡ QuotientGroupOp(R, A, I)`⟨x,y⟩" definition (in ring0) ideal_rmult ("_{⋅_}_") where "x{⋅I}y ≡ ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩" definition (in ring0) ideal_rmin ("{\<rm>_}_") where "{\<rm>I}y ≡ GroupInv(QuotientBy(I),QuotientGroupOp(R, A, I))`y" definition (in ring0) ideal_rsub ("_{\<rs>_}_") where "x{\<rs>I}y ≡ x{\<ra>I}({\<rm>I}y)" definition (in ring0) ideal_rzero ("𝟬⇩_") where "𝟬⇩I ≡ QuotientGroupRel(R,A,I)``{𝟬}" definition (in ring0) ideal_rone ("𝟭⇩_") where "𝟭⇩I ≡ QuotientGroupRel(R,A,I)``{𝟭}" definition (in ring0) ideal_rtwo ("𝟮⇩_") where "𝟮⇩I ≡ QuotientGroupRel(R,A,I)``{𝟮}" definition (in ring0) ideal_rsqr ("_⇧^{2}⇧_") where "x⇧^{2}⇧I ≡ ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,x⟩" lemma (in ring0) neutral_quotient: assumes "I◃R" shows "QuotientGroupRel(R,A,I)``{𝟬} = TheNeutralElement(QuotientBy(I),QuotientGroupOp(R, A, I))" using Group_ZF_2_4_L5B[of R A I "QuotientGroupRel(R, A, I)" 𝟬] ideal_normal_add_subgroup[OF assms] ringAssum unfolding IsAring_def QuotientBy_def[OF assms] by auto lemma (in ring0) one_quotient: assumes "I◃R" shows "QuotientGroupRel(R,A,I)``{𝟭} = TheNeutralElement(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R, A, I), M))" using Group_ZF_2_2_L1[of R M "QuotientGroupRel(R, A, I)" "ProjFun2(R, QuotientGroupRel(R, A, I), M)" 𝟭] equiv_rel[OF assms] quotientBy_mul_monoid[OF assms] ringAssum unfolding IsAring_def QuotientBy_def[OF assms] by auto lemma (in ring0) two_quotient: assumes "I◃R" shows "QuotientGroupRel(R,A,I)``{𝟮} = QuotientGroupOp(R, A, I)`⟨QuotientGroupRel(R,A,I)``{𝟭},QuotientGroupRel(R,A,I)``{𝟭}⟩" proof- have "QuotientGroupRel(R,A,I)``{𝟮} = QuotientGroupRel(R,A,I)``{𝟭\<ra>𝟭}" unfolding ringtwo_def by auto then show "QuotientGroupRel(R,A,I)``{𝟮} = QuotientGroupOp(R, A, I)`⟨QuotientGroupRel(R,A,I)``{𝟭}, QuotientGroupRel(R,A,I)``{𝟭}⟩" using EquivClass_1_L10[OF equiv_rel[OF assms] _ Ring_ZF_1_L2(2) Ring_ZF_1_L2(2), of A] Group_ZF_2_4_L5A[of R A I] ringAssum ideal_normal_add_subgroup[OF assms] unfolding IsAring_def QuotientGroupOp_def by auto qed lemma (in ring0) sqrt_quotient: assumes "I◃R" "x∈R" shows "QuotientGroupRel(R,A,I)``{x⇧^{2}} = ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupRel(R,A,I)``{x},QuotientGroupRel(R,A,I)``{x}⟩" proof- have "QuotientGroupRel(R,A,I)``{x⇧^{2}} = QuotientGroupRel(R,A,I)``{x⋅x}" unfolding ringsq_def by auto then show ?thesis using EquivClass_1_L10[OF equiv_rel[OF assms(1)] quotientBy_mul_monoid(1)[OF assms(1)] assms(2,2)] by auto qed text‹Both quotient operations are distributive› lemma (in ring0) quotientBy_distributive: assumes "I◃R" shows "IsDistributive(QuotientBy(I),QuotientGroupOp(R, A, I),ProjFun2(R, QuotientGroupRel(R,A,I), M))" proof- { fix x y z assume xyz:"x∈QuotientBy(I)" "y∈QuotientBy(I)" "z∈QuotientBy(I)" then obtain x1 y1 z1 where xyz1:"x1∈R" "y1∈R" "z1∈R" "QuotientGroupRel(R,A,I)``{x1} =x" "QuotientGroupRel(R,A,I)``{y1} =y" "QuotientGroupRel(R,A,I)``{z1} =z" unfolding QuotientBy_def[OF assms] quotient_def by auto have aux:"QuotientGroupOp(R, A, I)`⟨y,z⟩ = QuotientGroupRel(R,A,I)``{y1\<ra>z1}" using EquivClass_1_L10[OF equiv_rel Group_ZF_2_4_L5A] unfolding QuotientGroupOp_def using assms ringAssum ideal_normal_add_subgroup unfolding IsAring_def using xyz1(2,3,5,6) by auto then have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,QuotientGroupOp(R, A, I)`⟨y,z⟩⟩ = QuotientGroupRel(R,A,I)``{x1⋅(y1\<ra>z1)}" using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)] assms xyz1(1-4) Ring_ZF_1_L4(1) by auto moreover have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩ = QuotientGroupRel(R,A,I)``{x1⋅y1}" "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩ = QuotientGroupRel(R,A,I)``{x1⋅z1}" using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)] assms xyz1 by auto then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩ = QuotientGroupRel(R,A,I)``{(x1⋅y1)\<ra>(x1⋅z1)}" using EquivClass_1_L10[OF equiv_rel Group_ZF_2_4_L5A] unfolding QuotientGroupOp_def using assms ringAssum ideal_normal_add_subgroup unfolding IsAring_def using Ring_ZF_1_L4(3) xyz1(1-3) by auto then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩ = QuotientGroupRel(R,A,I)``{x1⋅(y1\<ra>z1)}" using ring_oper_distr(1) xyz1 by auto ultimately have A:"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,QuotientGroupOp(R, A, I)`⟨y,z⟩⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩" by auto from aux have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupOp(R, A, I)`⟨y,z⟩,x⟩ = QuotientGroupRel(R,A,I)``{(y1\<ra>z1)⋅x1}" using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)] assms xyz1(1-4) Ring_ZF_1_L4(1) by auto moreover have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩ = QuotientGroupRel(R,A,I)``{y1⋅x1}" "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩ = QuotientGroupRel(R,A,I)``{z1⋅x1}" using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)] assms xyz1 by auto then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩ = QuotientGroupRel(R,A,I)``{(y1⋅x1)\<ra>(z1⋅x1)}" using EquivClass_1_L10[OF equiv_rel Group_ZF_2_4_L5A] unfolding QuotientGroupOp_def using assms ringAssum ideal_normal_add_subgroup unfolding IsAring_def using Ring_ZF_1_L4(3) xyz1(1-3) by auto then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩ = QuotientGroupRel(R,A,I)``{(y1\<ra>z1)⋅x1}" using ring_oper_distr(2) xyz1 by auto ultimately have B:"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupOp(R, A, I)`⟨y,z⟩,x⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩" by auto with A have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,QuotientGroupOp(R, A, I)`⟨y,z⟩⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩" "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupOp(R, A, I)`⟨y,z⟩,x⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩" by auto } with IsDistributive_def show "IsDistributive (QuotientBy(I), QuotientGroupOp(R, A, I), ProjFun2(R, QuotientGroupRel(R, A, I), M))" by auto qed text‹The quotient group is a ring with the quotient multiplication› theorem (in ring0) quotientBy_is_ring: assumes "I◃R" shows "IsAring(QuotientBy(I), QuotientGroupOp(R, A, I), ProjFun2(R, QuotientGroupRel(R, A, I), M))" unfolding IsAring_def using quotientBy_distributive[OF assms] quotientBy_mul_monoid(2)[OF assms] quotientBy_add_group[OF assms] by auto text‹An import property satisfied by many important rings is being Noetherian: every ideal is finitely generated.› definition (in ring0) isFinGen ("_{is finitely generated}") where "I◃R ⟹ I{is finitely generated} ≡ ∃S∈FinPow(R). I = ⟨S⟩⇩_{I}" text‹For noetherian rings the arbitrary sum can be reduced to the sum of a finite subset of the initial set of ideals› theorem (in ring0) sum_ideals_noetherian: assumes "∀I∈ℐ. (I{is finitely generated})" "𝒥 ⊆ ℐ" shows "∃𝒯∈FinPow(𝒥). (⊕⇩_{I}𝒥) = (⊕⇩_{I}𝒯)" proof- have JR:"(⊕⇩_{I}𝒥)◃R" using generated_ideal_is_ideal[of "⋃𝒥"] assms(2) unfolding sumArbitraryIdeals_def[OF assms(2)] by auto with assms(1) have "(⊕⇩_{I}𝒥) {is finitely generated}" using ideal_dest_subset by auto then obtain S where S:"S∈FinPow(R)" "(⊕⇩_{I}𝒥) = ⟨S⟩⇩_{I}" unfolding isFinGen_def[OF JR] by auto from this(1) have fins:"Finite(S)" unfolding FinPow_def by auto then obtain n where n:"n∈nat" "S≈n" unfolding Finite_def by auto then have "S≲n" using eqpoll_iff by auto moreover let ?N = "λs∈S. {J∈FinPow(𝒥). s∈(⊕⇩_{I}J)}" from n(1) have "{the axiom of} n {choice holds}" using finite_choice by auto ultimately have "(∀t∈S. ?N ` t ≠ 0) ⟶ (∃f. f ∈ (∏t∈S. ?N ` t) ∧ (∀t∈S. f ` t ∈ ?N ` t))" unfolding AxiomCardinalChoiceGen_def by blast moreover { fix t assume t:"t∈S" then have "?N`t = {J∈FinPow(𝒥). t∈(⊕⇩_{I}J)}" using lamE by auto moreover from t have "t∈⟨S⟩⇩_{I}" using generated_ideal_contains_set S(1) unfolding FinPow_def by auto with S(2) have "t∈(⊕⇩_{I}𝒥)" by auto ultimately have "?N`t≠0" using sum_ideals_finite_sum[OF assms(2)] by auto } ultimately obtain f where f:"f:(∏t∈S. ?N ` t)" "∀t∈S. f ` t ∈ ?N ` t" by auto { fix y assume "y∈f``S" with image_iff obtain x where x:"x∈S" "⟨x,y⟩∈f" by auto with f(1) have "y∈?N`x" unfolding Pi_def by auto then have "y:{J∈FinPow(𝒥). x∈(⊕⇩_{I}J)}" using x(1) lamE by auto then have "Finite(y)" using lamE unfolding FinPow_def by auto } moreover from f(1) have f_Fun:"f:S→ (⋃{?N`t. t:S})" unfolding Pi_def Sigma_def by blast then have "Finite(f``S)" using Finite1_L6A[of f S _ S] Finite_Fin_iff fins Fin_into_Finite by auto ultimately have A:"Finite(⋃(f``S))" using Finite_Union by auto { fix t assume "t∈⋃(f``S)" then obtain q where q:"t∈q" "q∈f``S" by auto then obtain s where s:"t∈f`s" "s∈S" using func_imagedef[OF f_Fun] by auto from s(2) have J:"f`s∈FinPow(𝒥)" "s∈(⊕⇩_{I}(f`s))" using f(2) lamE by auto with s(1) have "t:𝒥" unfolding FinPow_def by auto } with A have B:"(⋃(f``S)):FinPow(𝒥)" unfolding FinPow_def by auto then have P:"(⋃(f``S)) ⊆ 𝒥" unfolding FinPow_def by auto then have C:"(⋃(f``S)) ⊆ ℐ" using assms(2) by auto then have "(⋃(f``S)) ⊆ Pow(R)" by auto then have sub:"⋃(⋃(f``S)) ⊆ R" by auto { fix t assume t:"t∈S" then have J:"f`t∈FinPow(𝒥)" "t∈(⊕⇩_{I}(f`t))" using f(2) lamE by auto from t have "⋃(f`t) ⊆ ⋃(⋃(f``S))" using func_imagedef[OF f_Fun] by auto then have "⋃(f`t) ⊆ ⟨⋃(⋃(f``S))⟩⇩_{I}" using generated_ideal_contains_set sub by blast then have "⟨⋃(f`t)⟩⇩_{I}⊆ ⟨⋃(⋃(f``S))⟩⇩_{I}" using generated_ideal_is_ideal[OF sub] generated_ideal_small by auto moreover have "f`t ⊆ ℐ" using J(1) assms(2) unfolding FinPow_def by auto moreover note J(2) ultimately have "t∈⟨⋃(⋃(f``S))⟩⇩_{I}" using sumArbitraryIdeals_def by auto then have "t∈(⊕⇩_{I}(⋃(f``S)))" using sumArbitraryIdeals_def C by auto } then have "S ⊆ ⊕⇩_{I}(⋃(f``S))" by auto then have "⟨S⟩⇩_{I}⊆ ⊕⇩_{I}(⋃(f``S))" using generated_ideal_small[ OF _ generated_ideal_is_ideal[OF sub]] sumArbitraryIdeals_def[OF C] by auto with S(2) have "(⊕⇩_{I}𝒥)⊆ ⊕⇩_{I}(⋃(f `` S))" by auto moreover from P have "⋃(⋃(f``S)) ⊆ ⋃𝒥" by auto then have "⋃(⋃(f``S)) ⊆⟨⋃𝒥⟩⇩_{I}" using generated_ideal_contains_set[of "⋃𝒥"] assms(2) by blast then have "⟨⋃(⋃(f``S))⟩⇩_{I}⊆ ⟨⋃𝒥⟩⇩_{I}" using generated_ideal_small[OF _ generated_ideal_is_ideal] assms(2) by blast then have "(⊕⇩_{I}(⋃(f `` S))) ⊆(⊕⇩_{I}𝒥)" unfolding sumArbitraryIdeals_def[OF assms(2)] sumArbitraryIdeals_def[OF C]. ultimately have "(⊕⇩_{I}𝒥) = ⊕⇩_{I}(⋃(f `` S))" by auto with B show ?thesis by auto qed end