Theory Ring_ZF

theory Ring_ZF
imports AbelianGroup_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 AbelianGroup_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.*}



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]: "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 ("_2" [96] 97)
defines ringsq_def [simp]: "a2 ≡ 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 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 "\<zero>∈R" "\<one>∈R" "(\<rm>\<zero>) = \<zero>"
using Ring_ZF_1_L1 group0.group0_2_L2 monoid0.unit_is_neutral
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 assms Ring_ZF_1_L1 group0.inverse_in_group group0.group_inv_of_inv
group0.group0_2_L6 group0.group0_2_L2 monoid0.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 ringAssum assms Ring_ZF_1_L1 Ring_ZF_1_L3
group0.group0_2_L1 monoid0.group0_1_L1
IsAring_def 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 = \<zero>"
using assms Ring_ZF_1_L1 group0.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 "\<zero>·x = \<zero>" "x·\<zero> = \<zero>"
proof -
let ?a = "x·\<one>";
let ?b = "x·\<zero>"
let ?c = "\<one>·x"
let ?d = "\<zero>·x"
from A1 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 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 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_cancel_add
by blast;
moreover from T2 T1 have "?d = \<zero>" using ring_cancel_add
by blast;
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 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 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 assms 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 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 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 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≠\<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 "a2 ≠ \<zero>"
shows "a≠\<zero>"
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 ∪ {\<zero>}) {is closed under} A"
using assms 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 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 = {\<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 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 Ring_ZF_1_L1 group0.inv_cancel_two 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 -;
let ?B = "b·c"
from ringAssum have "A {is commutative on} R"
using IsAring_def by simp;
moreover from A1 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 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 assms 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 assms 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