(*

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]: "a⇧^{2}≡ 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 "a⇧^{2}≠ \<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