(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2005, 2006 Slawomir Kolodynski 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 - introduction› theory Ring_ZF imports AbelianGroup_ZF begin text‹This theory file covers basic facts about rings.› subsection‹Definition and basic properties› text‹In this section we define what is a ring and list the basic properties of rings.› text‹We say that three sets $(R,A,M)$ form a ring if $(R,A)$ is an abelian group, $(R,M)$ is a monoid and $A$ is distributive with respect to $M$ on $R$. $A$ represents the additive operation on $R$. As such it is a subset of $(R\times R)\times R$ (recall that in ZF set theory functions are sets). Similarly $M$ represents the multiplicative operation on $R$ and is also a subset of $(R\times R)\times R$. We don't require the multiplicative operation to be commutative in the definition of a ring.› definition "IsAring(R,A,M) ≡ IsAgroup(R,A) ∧ (A {is commutative on} R) ∧ IsAmonoid(R,M) ∧ IsDistributive(R,A,M)" text‹We also define the notion of having no zero divisors. In standard notation the ring has no zero divisors if for all $a,b \in R$ we have $a\cdot b = 0$ implies $a = 0$ or $b = 0$. › definition "HasNoZeroDivs(R,A,M) ≡ (∀a∈R. ∀b∈R. M`⟨ a,b⟩ = TheNeutralElement(R,A) ⟶ a = TheNeutralElement(R,A) ∨ b = TheNeutralElement(R,A))" text‹Next we define a locale that will be used when considering rings.› locale ring0 = fixes R and A and M assumes ringAssum: "IsAring(R,A,M)" fixes ringa (infixl "\<ra>" 90) defines ringa_def [simp]: "x\<ra>y ≡ A`⟨x,y⟩" fixes ringminus ("\<rm> _" 89) defines ringminus_def [simp]: "(\<rm>x) ≡ GroupInv(R,A)`(x)" fixes ringsub (infixl "\<rs>" 90) defines ringsub_def [simp]: "x\<rs>y ≡ x\<ra>(\<rm>y)" fixes ringm (infixl "⋅" 95) defines ringm_def [simp]: "x⋅y ≡ M`⟨x,y⟩" fixes ringzero ("𝟬") defines ringzero_def [simp]: "𝟬 ≡ TheNeutralElement(R,A)" fixes ringone ("𝟭") defines ringone_def [simp]: "𝟭 ≡ TheNeutralElement(R,M)" fixes ringtwo ("𝟮") defines ringtwo_def [simp]: "𝟮 ≡ 𝟭\<ra>𝟭" fixes ringsq ("_⇧^{2}" [96] 97) defines ringsq_def [simp]: "x⇧^{2}≡ x⋅x" text‹In the ‹ring0› context we can use theorems proven in some other contexts.› lemma (in ring0) Ring_ZF_1_L1: shows "monoid0(R,M)" "group0(R,A)" "A {is commutative on} R" using ringAssum IsAring_def group0_def monoid0_def by auto text‹The theorems proven in in ‹group0› context (locale) are valid in the ‹ring0› context when applied to the additive group of the ring. › sublocale ring0 < add_group: group0 R A ringzero ringa ringminus using Ring_ZF_1_L1(2) unfolding ringa_def ringminus_def ringzero_def by auto text‹The theorem proven in the ‹monoid0› context are valid in the ‹ring0› context when applied to the multiplicative monoid of the ring. › sublocale ring0 < mult_monoid: monoid0 R M ringm using Ring_ZF_1_L1(1) unfolding ringm_def by auto text‹The additive operation in a ring is distributive with respect to the multiplicative operation.› lemma (in ring0) ring_oper_distr: assumes A1: "a∈R" "b∈R" "c∈R" shows "a⋅(b\<ra>c) = a⋅b \<ra> a⋅c" "(b\<ra>c)⋅a = b⋅a \<ra> c⋅a" using ringAssum assms IsAring_def IsDistributive_def by auto text‹Zero and one of the ring are elements of the ring. The negative of zero is zero.› lemma (in ring0) Ring_ZF_1_L2: shows "𝟬∈R" "𝟭∈R" "(\<rm>𝟬) = 𝟬" using add_group.group0_2_L2 mult_monoid.unit_is_neutral add_group.group_inv_of_one by auto text‹The next lemma lists some properties of a ring that require one element of a ring.› lemma (in ring0) Ring_ZF_1_L3: assumes "a∈R" shows "(\<rm>a) ∈ R" "(\<rm>(\<rm>a)) = a" "a\<ra>𝟬 = a" "𝟬\<ra>a = a" "a⋅𝟭 = a" "𝟭⋅a = a" "a\<rs>a = 𝟬" "a\<rs>𝟬 = a" "𝟮⋅a = a\<ra>a" "(\<rm>a)\<ra>a = 𝟬" using assms add_group.inverse_in_group add_group.group_inv_of_inv add_group.group0_2_L6 add_group.group0_2_L2 mult_monoid.unit_is_neutral Ring_ZF_1_L2 ring_oper_distr by auto text‹Properties that require two elements of a ring.› lemma (in ring0) Ring_ZF_1_L4: assumes A1: "a∈R" "b∈R" shows "a\<ra>b ∈ R" "a\<rs>b ∈ R" "a⋅b ∈ R" "a\<ra>b = b\<ra>a" using assms Ring_ZF_1_L1(3) Ring_ZF_1_L3 add_group.monoid.group0_1_L1 mult_monoid.group0_1_L1 unfolding IsCommutative_def by auto text‹Cancellation of an element on both sides of equality. This is a property of groups, written in the (additive) notation we use for the additive operation in rings. › lemma (in ring0) ring_cancel_add: assumes A1: "a∈R" "b∈R" and A2: "a \<ra> b = a" shows "b = 𝟬" using assms add_group.group0_2_L7 by simp text‹Any element of a ring multiplied by zero is zero.› lemma (in ring0) Ring_ZF_1_L6: assumes A1: "x∈R" shows "𝟬⋅x = 𝟬" "x⋅𝟬 = 𝟬" proof - let ?a = "x⋅𝟭" let ?b = "x⋅𝟬" let ?c = "𝟭⋅x" let ?d = "𝟬⋅x" from A1 have "?a \<ra> ?b = x⋅(𝟭 \<ra> 𝟬)" "?c \<ra> ?d = (𝟭 \<ra> 𝟬)⋅x" using Ring_ZF_1_L2 ring_oper_distr by auto moreover have "x⋅(𝟭 \<ra> 𝟬) = ?a" "(𝟭 \<ra> 𝟬)⋅x = ?c" using Ring_ZF_1_L2 Ring_ZF_1_L3 by auto ultimately have "?a \<ra> ?b = ?a" and T1: "?c \<ra> ?d = ?c" by auto moreover from A1 have "?a ∈ R" "?b ∈ R" and T2: "?c ∈ R" "?d ∈ R" using Ring_ZF_1_L2 Ring_ZF_1_L4 by auto ultimately have "?b = 𝟬" using ring_cancel_add by blast moreover from T2 T1 have "?d = 𝟬" using ring_cancel_add by blast ultimately show "x⋅𝟬 = 𝟬" "𝟬⋅x = 𝟬" by auto qed text‹Negative can be pulled out of a product.› lemma (in ring0) Ring_ZF_1_L7: assumes A1: "a∈R" "b∈R" shows "(\<rm>a)⋅b = \<rm>(a⋅b)" "a⋅(\<rm>b) = \<rm>(a⋅b)" "(\<rm>a)⋅b = a⋅(\<rm>b)" proof - from A1 have I: "a⋅b ∈ R" "(\<rm>a) ∈ R" "((\<rm>a)⋅b) ∈ R" "(\<rm>b) ∈ R" "a⋅(\<rm>b) ∈ R" using Ring_ZF_1_L3 Ring_ZF_1_L4 by auto moreover have "(\<rm>a)⋅b \<ra> a⋅b = 𝟬" and II: "a⋅(\<rm>b) \<ra> a⋅b = 𝟬" proof - from A1 I have "(\<rm>a)⋅b \<ra> a⋅b = ((\<rm>a)\<ra> a)⋅b" "a⋅(\<rm>b) \<ra> a⋅b= a⋅((\<rm>b)\<ra>b)" using ring_oper_distr by auto moreover from A1 have "((\<rm>a)\<ra> a)⋅b = 𝟬" "a⋅((\<rm>b)\<ra>b) = 𝟬" using add_group.group0_2_L6 Ring_ZF_1_L6 by auto ultimately show "(\<rm>a)⋅b \<ra> a⋅b = 𝟬" "a⋅(\<rm>b) \<ra> a⋅b = 𝟬" by auto qed ultimately show "(\<rm>a)⋅b = \<rm>(a⋅b)" using add_group.group0_2_L9 by simp moreover from I II show "a⋅(\<rm>b) = \<rm>(a⋅b)" using add_group.group0_2_L9 by simp ultimately show "(\<rm>a)⋅b = a⋅(\<rm>b)" by simp qed text‹Minus times minus is plus.› lemma (in ring0) Ring_ZF_1_L7A: assumes "a∈R" "b∈R" shows "(\<rm>a)⋅(\<rm>b) = a⋅b" using assms Ring_ZF_1_L3 Ring_ZF_1_L7 Ring_ZF_1_L4 by simp text‹Subtraction is distributive with respect to multiplication.› lemma (in ring0) Ring_ZF_1_L8: assumes "a∈R" "b∈R" "c∈R" shows "a⋅(b\<rs>c) = a⋅b \<rs> a⋅c" "(b\<rs>c)⋅a = b⋅a \<rs> c⋅a" using assms Ring_ZF_1_L3 ring_oper_distr Ring_ZF_1_L7 Ring_ZF_1_L4 by auto text‹Other basic properties involving two elements of a ring.› lemma (in ring0) Ring_ZF_1_L9: assumes "a∈R" "b∈R" shows "(\<rm>b)\<rs>a = (\<rm>a)\<rs>b" "(\<rm>(a\<ra>b)) = (\<rm>a)\<rs>b" "(\<rm>(a\<rs>b)) = ((\<rm>a)\<ra>b)" "a\<rs>(\<rm>b) = a\<ra>b" using assms Ring_ZF_1_L1(3) add_group.group0_4_L4 add_group.group_inv_of_inv by auto text‹If the difference of two element is zero, then those elements are equal.› lemma (in ring0) Ring_ZF_1_L9A: assumes A1: "a∈R" "b∈R" and A2: "a\<rs>b = 𝟬" shows "a=b" using add_group.group0_2_L11A assms by auto text‹Other basic properties involving three elements of a ring.› lemma (in ring0) Ring_ZF_1_L10: assumes "a∈R" "b∈R" "c∈R" shows "a\<ra>(b\<ra>c) = a\<ra>b\<ra>c" (*"a\<ra>(b\<rs>c) = a\<ra>b\<rs>c"*) "a\<rs>(b\<ra>c) = a\<rs>b\<rs>c" "a\<rs>(b\<rs>c) = a\<rs>b\<ra>c" using assms Ring_ZF_1_L1(3) add_group.group_oper_assoc add_group.group0_4_L4A by auto text‹Another property with three elements.› lemma (in ring0) Ring_ZF_1_L10A: assumes A1: "a∈R" "b∈R" "c∈R" shows "a\<ra>(b\<rs>c) = a\<ra>b\<rs>c" using assms Ring_ZF_1_L3 Ring_ZF_1_L10 by simp text‹Associativity of addition and multiplication.› lemma (in ring0) Ring_ZF_1_L11: assumes "a∈R" "b∈R" "c∈R" shows "a\<ra>b\<ra>c = a\<ra>(b\<ra>c)" "a⋅b⋅c = a⋅(b⋅c)" using assms add_group.group_oper_assoc mult_monoid.sum_associative by auto text‹An interpretation of what it means that a ring has no zero divisors.› lemma (in ring0) Ring_ZF_1_L12: assumes "HasNoZeroDivs(R,A,M)" and "a∈R" "a≠𝟬" "b∈R" "b≠𝟬" shows "a⋅b≠𝟬" using assms HasNoZeroDivs_def by auto text‹In rings with no zero divisors we can cancel nonzero factors.› lemma (in ring0) Ring_ZF_1_L12A: assumes A1: "HasNoZeroDivs(R,A,M)" and A2: "a∈R" "b∈R" "c∈R" and A3: "a⋅c = b⋅c" and A4: "c≠𝟬" shows "a=b" proof - from A2 have T: "a⋅c ∈ R" "a\<rs>b ∈ R" using Ring_ZF_1_L4 by auto with A1 A2 A3 have "a\<rs>b = 𝟬 ∨ c=𝟬" using Ring_ZF_1_L3 Ring_ZF_1_L8 HasNoZeroDivs_def by simp with A2 A4 have "a∈R" "b∈R" "a\<rs>b = 𝟬" by auto then show "a=b" by (rule Ring_ZF_1_L9A) qed text‹In rings with no zero divisors if two elements are different, then after multiplying by a nonzero element they are still different.› lemma (in ring0) Ring_ZF_1_L12B: assumes A1: "HasNoZeroDivs(R,A,M)" "a∈R" "b∈R" "c∈R" "a≠b" "c≠𝟬" shows "a⋅c ≠ b⋅c" using A1 Ring_ZF_1_L12A by auto (* A1 has to be here *) text‹In rings with no zero divisors multiplying a nonzero element by a nonone element changes the value.› lemma (in ring0) Ring_ZF_1_L12C: assumes A1: "HasNoZeroDivs(R,A,M)" and A2: "a∈R" "b∈R" and A3: "𝟬≠a" "𝟭≠b" shows "a ≠ a⋅b" proof - { assume "a = a⋅b" with A1 A2 have "a = 𝟬 ∨ b\<rs>𝟭 = 𝟬" using Ring_ZF_1_L3 Ring_ZF_1_L2 Ring_ZF_1_L8 Ring_ZF_1_L3 Ring_ZF_1_L2 Ring_ZF_1_L4 HasNoZeroDivs_def by simp with A2 A3 have False using Ring_ZF_1_L2 Ring_ZF_1_L9A by auto } then show "a ≠ a⋅b" by auto qed text‹If a square is nonzero, then the element is nonzero.› lemma (in ring0) Ring_ZF_1_L13: assumes "a∈R" and "a⇧^{2}≠ 𝟬" shows "a≠𝟬" using assms Ring_ZF_1_L2 Ring_ZF_1_L6 by auto text‹Square of an element and its opposite are the same.› lemma (in ring0) Ring_ZF_1_L14: assumes "a∈R" shows "(\<rm>a)⇧^{2}= ((a)⇧^{2})" using assms Ring_ZF_1_L7A by simp text‹Adding zero to a set that is closed under addition results in a set that is also closed under addition. This is a property of groups.› lemma (in ring0) Ring_ZF_1_L15: assumes "H ⊆ R" and "H {is closed under} A" shows "(H ∪ {𝟬}) {is closed under} A" using assms add_group.group0_2_L17 by simp text‹Adding zero to a set that is closed under multiplication results in a set that is also closed under multiplication.› lemma (in ring0) Ring_ZF_1_L16: assumes A1: "H ⊆ R" and A2: "H {is closed under} M" shows "(H ∪ {𝟬}) {is closed under} M" using assms Ring_ZF_1_L2 Ring_ZF_1_L6 IsOpClosed_def by auto text‹The ring is trivial iff $0=1$.› lemma (in ring0) Ring_ZF_1_L17: shows "R = {𝟬} ⟷ 𝟬=𝟭" proof assume "R = {𝟬}" then show "𝟬=𝟭" using Ring_ZF_1_L2 by blast next assume A1: "𝟬 = 𝟭" then have "R ⊆ {𝟬}" using Ring_ZF_1_L3 Ring_ZF_1_L6 by auto moreover have "{𝟬} ⊆ R" using Ring_ZF_1_L2 by auto ultimately show "R = {𝟬}" by auto qed text‹The sets $\{m\cdot x. x\in R\}$ and $\{-m\cdot x. x\in R\}$ are the same.› lemma (in ring0) Ring_ZF_1_L18: assumes A1: "m∈R" shows "{m⋅x. x∈R} = {(\<rm>m)⋅x. x∈R}" proof { fix a assume "a ∈ {m⋅x. x∈R}" then obtain x where "x∈R" and "a = m⋅x" by auto with A1 have "(\<rm>x) ∈ R" and "a = (\<rm>m)⋅(\<rm>x)" using Ring_ZF_1_L3 Ring_ZF_1_L7A by auto then have "a ∈ {(\<rm>m)⋅x. x∈R}" by auto } then show "{m⋅x. x∈R} ⊆ {(\<rm>m)⋅x. x∈R}" by auto next { fix a assume "a ∈ {(\<rm>m)⋅x. x∈R}" then obtain x where "x∈R" and "a = (\<rm>m)⋅x" by auto with A1 have "(\<rm>x) ∈ R" and "a = m⋅(\<rm>x)" using Ring_ZF_1_L3 Ring_ZF_1_L7 by auto then have "a ∈ {m⋅x. x∈R}" by auto } then show "{(\<rm>m)⋅x. x∈R} ⊆ {m⋅x. x∈R}" by auto qed subsection‹Rearrangement lemmas› text‹In happens quite often that we want to show a fact like $(a+b)c+d = (ac+d-e)+(bc+e)$in rings. This is trivial in romantic math and probably there is a way to make it trivial in formalized math. However, I don't know any other way than to tediously prove each such rearrangement when it is needed. This section collects facts of this type.› text‹Rearrangements with two elements of a ring.› lemma (in ring0) Ring_ZF_2_L1: assumes "a∈R" "b∈R" shows "a\<ra>b⋅a = (b\<ra>𝟭)⋅a" using assms Ring_ZF_1_L2 ring_oper_distr Ring_ZF_1_L3 Ring_ZF_1_L4 by simp text‹Rearrangements with two elements and cancelling.› lemma (in ring0) Ring_ZF_2_L1A: assumes "a∈R" "b∈R" shows "a\<rs>b\<ra>b = a" "a\<ra>b\<rs>a = b" "(\<rm>a)\<ra>b\<ra>a = b" "(\<rm>a)\<ra>(b\<ra>a) = b" "a\<ra>(b\<rs>a) = b" using assms add_group.inv_cancel_two add_group.group0_4_L6A Ring_ZF_1_L1(3) by auto text‹In rings $a-(b+1)c = (a-d-c)+(d-bc)$ and $a+b+(c+d) = a+(b+c)+d$.› lemma (in ring0) Ring_ZF_2_L2: assumes "a∈R" "b∈R" "c∈R" "d∈R" shows "a\<rs>(b\<ra>𝟭)⋅c = (a\<rs>d\<rs>c)\<ra>(d\<rs>b⋅c)" "a\<ra>b\<ra>(c\<ra>d) = a\<ra>b\<ra>c\<ra>d" "a\<ra>b\<ra>(c\<ra>d) = a\<ra>(b\<ra>c)\<ra>d" proof - let ?B = "b⋅c" from ringAssum assms have "A {is commutative on} R" and "a∈R" "?B ∈ R" "c∈R" "d∈R" unfolding IsAring_def using Ring_ZF_1_L4 by auto then have "a\<ra>(\<rm>?B\<ra>c) = a\<ra>(\<rm>d)\<ra>(\<rm>c)\<ra>(d\<ra>(\<rm>?B))" by (rule add_group.group0_4_L8) with assms show "a\<rs>(b\<ra>𝟭)⋅c = (a\<rs>d\<rs>c)\<ra>(d\<rs>b⋅c)" using Ring_ZF_1_L2 ring_oper_distr Ring_ZF_1_L3 by simp from assms show "a\<ra>b\<ra>(c\<ra>d) = a\<ra>b\<ra>c\<ra>d" using Ring_ZF_1_L4(1) Ring_ZF_1_L10(1) by simp with assms(1,2,3) show "a\<ra>b\<ra>(c\<ra>d) = a\<ra>(b\<ra>c)\<ra>d" using Ring_ZF_1_L10(1) by simp qed text‹Rerrangement about adding linear functions.› lemma (in ring0) Ring_ZF_2_L3: assumes A1: "a∈R" "b∈R" "c∈R" "d∈R" "x∈R" shows "(a⋅x \<ra> b) \<ra> (c⋅x \<ra> d) = (a\<ra>c)⋅x \<ra> (b\<ra>d)" proof - from A1 have "A {is commutative on} R" "a⋅x ∈ R" "b∈R" "c⋅x ∈ R" "d∈R" using Ring_ZF_1_L1 Ring_ZF_1_L4 by auto then have "A`⟨A`⟨ a⋅x,b⟩,A`⟨ c⋅x,d⟩⟩ = A`⟨A`⟨ a⋅x,c⋅x⟩,A`⟨ b,d⟩⟩" using add_group.group0_4_L8(3) by auto with A1 show "(a⋅x \<ra> b) \<ra> (c⋅x \<ra> d) = (a\<ra>c)⋅x \<ra> (b\<ra>d)" using ring_oper_distr by simp qed text‹Rearrangement with three elements› lemma (in ring0) Ring_ZF_2_L4: assumes "M {is commutative on} R" and "a∈R" "b∈R" "c∈R" shows "a⋅(b⋅c) = a⋅c⋅b" and "a⋅b⋅c = a⋅c⋅b" using assms IsCommutative_def Ring_ZF_1_L11 by simp_all text‹Some other rearrangements with three elements.› lemma (in ring0) ring_rearr_3_elemA: assumes A1: "M {is commutative on} R" and A2: "a∈R" "b∈R" "c∈R" shows "a⋅(a⋅c) \<rs> b⋅(\<rm>b⋅c) = (a⋅a \<ra> b⋅b)⋅c" "a⋅(\<rm>b⋅c) \<ra> b⋅(a⋅c) = 𝟬" proof - from A2 have T: "b⋅c ∈ R" "a⋅a ∈ R" "b⋅b ∈ R" "b⋅(b⋅c) ∈ R" "a⋅(b⋅c) ∈ R" using Ring_ZF_1_L4 by auto with A2 show "a⋅(a⋅c) \<rs> b⋅(\<rm>b⋅c) = (a⋅a \<ra> b⋅b)⋅c" using Ring_ZF_1_L7 Ring_ZF_1_L3 Ring_ZF_1_L11 ring_oper_distr by simp from A2 T have "a⋅(\<rm>b⋅c) \<ra> b⋅(a⋅c) = (\<rm>a⋅(b⋅c)) \<ra> b⋅a⋅c" using Ring_ZF_1_L7 Ring_ZF_1_L11 by simp also from A1 A2 T have "… = 𝟬" using IsCommutative_def Ring_ZF_1_L11 Ring_ZF_1_L3 by simp finally show "a⋅(\<rm>b⋅c) \<ra> b⋅(a⋅c) = 𝟬" by simp qed text‹Some rearrangements with four elements. Properties of abelian groups.› lemma (in ring0) Ring_ZF_2_L5: assumes "a∈R" "b∈R" "c∈R" "d∈R" shows "a \<rs> b \<rs> c \<rs> d = a \<rs> d \<rs> b \<rs> c" "a \<ra> b \<ra> c \<rs> d = a \<rs> d \<ra> b \<ra> c" "a \<ra> b \<rs> c \<rs> d = a \<rs> c \<ra> (b \<rs> d)" "a \<ra> b \<ra> c \<ra> d = a \<ra> c \<ra> (b \<ra> d)" using assms Ring_ZF_1_L1(3) add_group.rearr_ab_gr_4_elemB add_group.rearr_ab_gr_4_elemA by auto text‹Two big rearranegements with six elements, useful for proving properties of complex addition and multiplication.› lemma (in ring0) Ring_ZF_2_L6: assumes A1: "a∈R" "b∈R" "c∈R" "d∈R" "e∈R" "f∈R" shows "a⋅(c⋅e \<rs> d⋅f) \<rs> b⋅(c⋅f \<ra> d⋅e) = (a⋅c \<rs> b⋅d)⋅e \<rs> (a⋅d \<ra> b⋅c)⋅f" "a⋅(c⋅f \<ra> d⋅e) \<ra> b⋅(c⋅e \<rs> d⋅f) = (a⋅c \<rs> b⋅d)⋅f \<ra> (a⋅d \<ra> b⋅c)⋅e" "a⋅(c\<ra>e) \<rs> b⋅(d\<ra>f) = a⋅c \<rs> b⋅d \<ra> (a⋅e \<rs> b⋅f)" "a⋅(d\<ra>f) \<ra> b⋅(c\<ra>e) = a⋅d \<ra> b⋅c \<ra> (a⋅f \<ra> b⋅e)" proof - from A1 have T: "c⋅e ∈ R" "d⋅f ∈ R" "c⋅f ∈ R" "d⋅e ∈ R" "a⋅c ∈ R" "b⋅d ∈ R" "a⋅d ∈ R" "b⋅c ∈ R" "b⋅f ∈ R" "a⋅e ∈ R" "b⋅e ∈ R" "a⋅f ∈ R" "a⋅c⋅e ∈ R" "a⋅d⋅f ∈ R" "b⋅c⋅f ∈ R" "b⋅d⋅e ∈ R" "b⋅c⋅e ∈ R" "b⋅d⋅f ∈ R" "a⋅c⋅f ∈ R" "a⋅d⋅e ∈ R" "a⋅c⋅e \<rs> a⋅d⋅f ∈ R" "a⋅c⋅e \<rs> b⋅d⋅e ∈ R" "a⋅c⋅f \<ra> a⋅d⋅e ∈ R" "a⋅c⋅f \<rs> b⋅d⋅f ∈ R" "a⋅c \<ra> a⋅e ∈ R" "a⋅d \<ra> a⋅f ∈ R" using Ring_ZF_1_L4 by auto with A1 show "a⋅(c⋅e \<rs> d⋅f) \<rs> b⋅(c⋅f \<ra> d⋅e) = (a⋅c \<rs> b⋅d)⋅e \<rs> (a⋅d \<ra> b⋅c)⋅f" using Ring_ZF_1_L8 ring_oper_distr Ring_ZF_1_L11 Ring_ZF_1_L10 Ring_ZF_2_L5 by simp from A1 T show "a⋅(c⋅f \<ra> d⋅e) \<ra> b⋅(c⋅e \<rs> d⋅f) = (a⋅c \<rs> b⋅d)⋅f \<ra> (a⋅d \<ra> b⋅c)⋅e" using Ring_ZF_1_L8 ring_oper_distr Ring_ZF_1_L11 Ring_ZF_1_L10A Ring_ZF_2_L5 Ring_ZF_1_L10 by simp from A1 T show "a⋅(c\<ra>e) \<rs> b⋅(d\<ra>f) = a⋅c \<rs> b⋅d \<ra> (a⋅e \<rs> b⋅f)" "a⋅(d\<ra>f) \<ra> b⋅(c\<ra>e) = a⋅d \<ra> b⋅c \<ra> (a⋅f \<ra> b⋅e)" using ring_oper_distr Ring_ZF_1_L10 Ring_ZF_2_L5 by auto qed end