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 ("_²" [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 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\<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;
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 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)² = ((a)²)"
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