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]: "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 ("𝟬")
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]: "a⇧2 ≡ a⋅a"
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 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 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>𝟬 = a"
"𝟬\<ra>a = a"
"a⋅𝟭 = a"
"𝟭⋅a = a"
"a\<rs>a = 𝟬"
"a\<rs>𝟬 = a"
"𝟮⋅a = a\<ra>a"
"(\<rm>a)\<ra>a = 𝟬"
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 = 𝟬"
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 "𝟬⋅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 Ring_ZF_1_L1 group0.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 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 = 𝟬"
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≠𝟬" "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
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 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 ∪ {𝟬}) {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 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>𝟭)⋅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) = 𝟬"
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 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