Theory Ring_ZF

(*
    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