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.

*)

header {*\isaheader{Ring\_ZF.thy}*}

theory Ring_ZF imports Group_ZF 

begin

text{*This theory file covers basic facts about rings.*}

section{*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.
  We also define the notion of having no zero divisors.*}

constdefs 
  "IsAring(R,A,M) ≡ IsAgroup(R,A) ∧ (A {is commutative on} R) ∧ 
  IsAmonoid(R,M) ∧ IsDistributive(R,A,M)"

  "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]: "a\<ra>b ≡ A`<a,b>"

  fixes ringminus ("\<rm> _" 89)
  defines ringminus_def [simp]: "(\<rm>a) ≡ GroupInv(R,A)`(a)"

  fixes ringsub (infixl "\<rs>" 90)
  defines ringsub_def [simp]: "a\<rs>b ≡ a\<ra>(\<rm>b)"

  fixes ringm (infixl "·" 95)
  defines ringm_def [simp]: "a·b ≡ M`<a,b>"

  fixes ringzero ("\<zero>")
  defines ringzero_def [simp]: "\<zero> ≡ TheNeutralElement(R,A)"

  fixes ringone ("\<one>")
  defines ringone_def [simp]: "\<one> ≡ TheNeutralElement(R,M)"

  fixes ringtwo ("\<two>")
  defines ringtwo_def [simp]: "\<two> ≡ \<one>\<ra>\<one>"

  fixes ringsq ("_²" [96] 97)
  defines ringsq_def [simp]: "a² ≡ a·a"

text{*In the @{text "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 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 prems 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 "\<zero>∈R"  "\<one>∈R"   "(\<rm>\<zero>) = \<zero>"
  using Ring_ZF_1_L1 group0.group0_2_L2 monoid0.group0_1_L3 
    group0.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>\<zero> = a" 
  "\<zero>\<ra>a = a" 
  "a·\<one> = a" 
  "\<one>·a = a" 
  "a\<rs>a = \<zero>" 
  "a\<rs>\<zero> = a"
  "\<two>·a = a\<ra>a"
  "(\<rm>a)\<ra>a = \<zero>"
  using prems Ring_ZF_1_L1 group0.inverse_in_group group0.group_inv_of_inv 
    group0.group0_2_L6 group0.group0_2_L2 monoid0.group0_1_L3 
    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 ringAssum prems Ring_ZF_1_L1 Ring_ZF_1_L3 
    group0.group0_2_L1 monoid0.group0_1_L1 
    IsAring_def IsCommutative_def
  by auto;

text{*Any element of a ring multiplied by zero is zero.*}

lemma (in ring0) Ring_ZF_1_L6: 
  assumes A1: "x∈R" shows "\<zero>·x = \<zero>"   "x·\<zero> = \<zero>"
proof -
  def D1: a ≡ "x·\<one>";
  def D2: b ≡ "x·\<zero>"
  def D3: c ≡ "\<one>·x"
  def D4: d ≡ "\<zero>·x"
  from A1 D1 D2 D3 D4 have 
    "a \<ra> b = x·(\<one> \<ra> \<zero>)"   "c \<ra> d = (\<one> \<ra> \<zero>)·x"
    using Ring_ZF_1_L2 ring_oper_distr by auto;
  moreover from D1 D3 have "x·(\<one> \<ra> \<zero>) = a" "(\<one> \<ra> \<zero>)·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 D1 D2 D3 D4 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 = \<zero>" using 
    Ring_ZF_1_L1 group0.group0_2_L7 by simp;
  moreover from T2 T1 have "d = \<zero>" using 
    Ring_ZF_1_L1 group0.group0_2_L7 by simp;
  moreover from D2 D4 have "b = x·\<zero>"  "d = \<zero>·x" by auto; 
  ultimately show "x·\<zero> = \<zero>"  "\<zero>·x = \<zero>" 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 = \<zero>" 
    and II: "a·(\<rm>b) \<ra> a·b = \<zero>"
  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 = \<zero>" 
      "a·((\<rm>b)\<ra>b) = \<zero>"
      using Ring_ZF_1_L1 group0.group0_2_L6 Ring_ZF_1_L6
      by auto;
    ultimately show 
      "(\<rm>a)·b \<ra> a·b = \<zero>" 
      "a·(\<rm>b) \<ra> a·b = \<zero>" 
      by auto;
  qed;
  ultimately show "(\<rm>a)·b = \<rm>(a·b)"
    using Ring_ZF_1_L1 group0.group0_2_L9 by simp
  moreover from I II show "a·(\<rm>b) = \<rm>(a·b)"
    using Ring_ZF_1_L1 group0.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 prems 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 prems 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 prems ringAssum IsAring_def 
    Ring_ZF_1_L1 group0.group0_4_L4  group0.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 = \<zero>"
  shows "a=b"
proof -
  from A1 A2 have
    "group0(R,A)"
    "a∈R"  "b∈R"
    "A`⟨a,GroupInv(R,A)`(b)⟩ = TheNeutralElement(R,A)"
    using Ring_ZF_1_L1 by auto;
  then show "a=b" by (rule group0.group0_2_L11A);
qed;

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 prems ringAssum Ring_ZF_1_L1 group0.group_oper_assoc 
    IsAring_def group0.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 prems 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 prems ringAssum Ring_ZF_1_L1 group0.group_oper_assoc
    IsAring_def IsAmonoid_def IsAssociative_def
  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≠\<zero>"  "b∈R"  "b≠\<zero>"
  shows "a·b≠\<zero>" 
  using prems 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≠\<zero>" 
  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 = \<zero> ∨ c=\<zero>"
    using Ring_ZF_1_L3 Ring_ZF_1_L8 HasNoZeroDivs_def
    by simp;
  with A2 A4 have "a∈R"  "b∈R"  "a\<rs>b = \<zero>" 
    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≠\<zero>" 
  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: "\<zero>≠a"  "\<one>≠b"
  shows "a ≠ a·b"
proof -
  { assume "a = a·b"
    with A1 A2 have "a = \<zero> ∨ b\<rs>\<one> = \<zero>"
      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² ≠ \<zero>"
  shows "a≠\<zero>"
  using prems 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)² = ((a)²)"
  using prems 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 ∪ {\<zero>}) {is closed under} A"
  using prems Ring_ZF_1_L1 group0.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 ∪ {\<zero>}) {is closed under} M"
  using prems 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 = {\<zero>} <-> \<zero>=\<one>"
proof;
  assume "R = {\<zero>}"
  then show "\<zero>=\<one>" using Ring_ZF_1_L2
    by blast;
next assume A1: "\<zero> = \<one>"
  then have "R ⊆ {\<zero>}"
    using Ring_ZF_1_L3 Ring_ZF_1_L6 by auto;
  moreover have "{\<zero>} ⊆ R" using Ring_ZF_1_L2 by auto;
  ultimately show "R = {\<zero>}" 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;

section{*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>\<one>)·a"
  using prems Ring_ZF_1_L2 ring_oper_distr Ring_ZF_1_L3 Ring_ZF_1_L4
  by simp;

text{*Raearrangements 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 prems Ring_ZF_1_L1 group0.group0_2_L16 group0.group0_4_L6A
  by auto;

text{*In commutative rings $a-(b+1)c = (a-d-c)+(d-bc)$. For unknown reasons 
  we have to use the raw set notation in the proof, otherwise all methods 
  fail.*}

lemma (in ring0) Ring_ZF_2_L2: 
  assumes A1: "a∈R"  "b∈R"  "c∈R"  "d∈R"
  shows "a\<rs>(b\<ra>\<one>)·c = (a\<rs>d\<rs>c)\<ra>(d\<rs>b·c)"
proof -;
  def D1: B == "b·c" 
  from ringAssum have "A {is commutative on} R"
    using IsAring_def by simp;
  moreover from A1 D1 have "a∈R" "B ∈ R" "c∈R" "d∈R"
    using Ring_ZF_1_L4 by auto;
  ultimately have "A`⟨a, GroupInv(R,A)`(A`⟨B, c⟩)⟩ =
    A`⟨A`⟨A`⟨a, GroupInv(R, A)`(d)⟩,GroupInv(R, A)`(c)⟩,
    A`⟨d,GroupInv(R, A)`(B)⟩⟩"
    using Ring_ZF_1_L1 group0.group0_4_L8 by blast;
  with D1 A1 show ?thesis 
    using Ring_ZF_1_L2 ring_oper_distr Ring_ZF_1_L3 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 
    "group0(R,A)"
    "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>⟩"
    by (rule group0.group0_4_L8);
  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"
  using prems IsCommutative_def Ring_ZF_1_L11
  by simp;

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) = \<zero>"
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 "… = \<zero>"
    using IsCommutative_def Ring_ZF_1_L11 Ring_ZF_1_L3
    by simp;
  finally show "a·(\<rm>b·c) \<ra> b·(a·c) = \<zero>"
    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 prems Ring_ZF_1_L1 group0.rearr_ab_gr_4_elemB
    group0.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