# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Ring_ZF imports AbelianGroup_ZF
begin

This theory file covers basic facts about rings.

### Definition and basic properties

In this section we define what is a ring and list the basic properties of rings.

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

$$\text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge$$ $$\text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M)$$

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

$$\text{HasNoZeroDivs}(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\$$ $$M\langle a,b\rangle = \text{ TheNeutralElement}(R,A) \longrightarrow$$ $$a = \text{ TheNeutralElement}(R,A) \vee b = \text{ TheNeutralElement}(R,A))$$

Next we define a locale that will be used when considering rings.

locale ring0

assumes ringAssum: $$\text{IsAring}(R,A,M)$$

defines $$x + y \equiv A\langle x,y\rangle$$

defines $$( - x) \equiv \text{GroupInv}(R,A)(x)$$

defines $$x - y \equiv x + ( - y)$$

defines $$x\cdot y \equiv M\langle x,y\rangle$$

defines $$0 \equiv \text{ TheNeutralElement}(R,A)$$

defines $$1 \equiv \text{ TheNeutralElement}(R,M)$$

defines $$2 \equiv 1 + 1$$

defines $$x^2 \equiv x\cdot x$$

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 \text{ is commutative on } R$$ using ringAssum, IsAring_def, group0_def, monoid0_def

The theorems proven in in group0 context (locale) are valid in the ring0 context when applied to the additive group of the ring.

using Ring_ZF_1_L1(2) unfolding ringa_def, ringminus_def, ringzero_def

The theorem proven in the monoid0 context are valid in the ring0 context when applied to the multiplicative monoid of the ring.

sublocale ring0 < mult_monoid: monoid0

using Ring_ZF_1_L1(1) unfolding ringm_def

The additive operation in a ring is distributive with respect to the multiplicative operation.

lemma (in ring0) ring_oper_distr:

assumes A1: $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b + c) = a\cdot b + a\cdot c$$, $$(b + c)\cdot a = b\cdot a + c\cdot a$$ using ringAssum, assms, IsAring_def, IsDistributive_def

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 $$0 \in R$$, $$1 \in R$$, $$( - 0 ) = 0$$ using group0_2_L2, unit_is_neutral, group_inv_of_one

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\in R$$

shows $$( - a) \in R$$, $$( - ( - a)) = a$$, $$a + 0 = a$$, $$0 + a = a$$, $$a\cdot 1 = a$$, $$1 \cdot a = a$$, $$a - a = 0$$, $$a - 0 = a$$, $$2 \cdot a = a + a$$, $$( - a) + a = 0$$ using assms, inverse_in_group, group_inv_of_inv, group0_2_L6, group0_2_L2, unit_is_neutral, Ring_ZF_1_L2, ring_oper_distr

Properties that require two elements of a ring.

lemma (in ring0) Ring_ZF_1_L4:

assumes A1: $$a\in R$$, $$b\in R$$

shows $$a + b \in R$$, $$a - b \in R$$, $$a\cdot b \in R$$, $$a + b = b + a$$ using assms, Ring_ZF_1_L1(3), Ring_ZF_1_L3, group0_1_L1, group0_1_L1 unfolding IsCommutative_def

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.

assumes A1: $$a\in R$$, $$b\in R$$ and A2: $$a + b = a$$

shows $$b = 0$$ using assms, group0_2_L7

Any element of a ring multiplied by zero is zero.

lemma (in ring0) Ring_ZF_1_L6:

assumes A1: $$x\in R$$

shows $$0 \cdot x = 0$$, $$x\cdot 0 = 0$$proof
let $$a = x\cdot 1$$
let $$b = x\cdot 0$$
let $$c = 1 \cdot x$$
let $$d = 0 \cdot x$$
from A1 have $$a + b = x\cdot (1 + 0 )$$, $$c + d = (1 + 0 )\cdot x$$ using Ring_ZF_1_L2, ring_oper_distr
moreover
have $$x\cdot (1 + 0 ) = a$$, $$(1 + 0 )\cdot x = c$$ using Ring_ZF_1_L2, Ring_ZF_1_L3
ultimately have $$a + b = a$$ and T1: $$c + d = c$$
moreover
from A1 have $$a \in R$$, $$b \in R$$ and T2: $$c \in R$$, $$d \in R$$ using Ring_ZF_1_L2, Ring_ZF_1_L4
ultimately have $$b = 0$$ using ring_cancel_add
moreover
from T2, T1 have $$d = 0$$ using ring_cancel_add
ultimately show $$x\cdot 0 = 0$$, $$0 \cdot x = 0$$
qed

Negative can be pulled out of a product.

lemma (in ring0) Ring_ZF_1_L7:

assumes A1: $$a\in R$$, $$b\in R$$

shows $$( - a)\cdot b = - (a\cdot b)$$, $$a\cdot ( - b) = - (a\cdot b)$$, $$( - a)\cdot b = a\cdot ( - b)$$proof
from A1 have I: $$a\cdot b \in R$$, $$( - a) \in R$$, $$(( - a)\cdot b) \in R$$, $$( - b) \in R$$, $$a\cdot ( - b) \in R$$ using Ring_ZF_1_L3, Ring_ZF_1_L4
moreover
have $$( - a)\cdot b + a\cdot b = 0$$ and II: $$a\cdot ( - b) + a\cdot b = 0$$proof
from A1, I have $$( - a)\cdot b + a\cdot b = (( - a) + a)\cdot b$$, $$a\cdot ( - b) + a\cdot b= a\cdot (( - b) + b)$$ using ring_oper_distr
moreover
from A1 have $$(( - a) + a)\cdot b = 0$$, $$a\cdot (( - b) + b) = 0$$ using group0_2_L6, Ring_ZF_1_L6
ultimately show $$( - a)\cdot b + a\cdot b = 0$$, $$a\cdot ( - b) + a\cdot b = 0$$
qed
ultimately show $$( - a)\cdot b = - (a\cdot b)$$ using group0_2_L9
moreover
from I, II show $$a\cdot ( - b) = - (a\cdot b)$$ using group0_2_L9
ultimately show $$( - a)\cdot b = a\cdot ( - b)$$
qed

Minus times minus is plus.

lemma (in ring0) Ring_ZF_1_L7A:

assumes $$a\in R$$, $$b\in R$$

shows $$( - a)\cdot ( - b) = a\cdot b$$ using assms, Ring_ZF_1_L3, Ring_ZF_1_L7, Ring_ZF_1_L4

Subtraction is distributive with respect to multiplication.

lemma (in ring0) Ring_ZF_1_L8:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b - c) = a\cdot b - a\cdot c$$, $$(b - c)\cdot a = b\cdot a - c\cdot a$$ using assms, Ring_ZF_1_L3, ring_oper_distr, Ring_ZF_1_L7, Ring_ZF_1_L4

Other basic properties involving two elements of a ring.

lemma (in ring0) Ring_ZF_1_L9:

assumes $$a\in R$$, $$b\in R$$

shows $$( - b) - a = ( - a) - b$$, $$( - (a + b)) = ( - a) - b$$, $$( - (a - b)) = (( - a) + b)$$, $$a - ( - b) = a + b$$ using assms, Ring_ZF_1_L1(3), group0_4_L4, group_inv_of_inv

If the difference of two element is zero, then those elements are equal.

lemma (in ring0) Ring_ZF_1_L9A:

assumes A1: $$a\in R$$, $$b\in R$$ and A2: $$a - b = 0$$

shows $$a=b$$ using group0_2_L11A, assms

Other basic properties involving three elements of a ring.

lemma (in ring0) Ring_ZF_1_L10:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + (b + c) = a + b + c$$, $$a - (b + c) = a - b - c$$, $$a - (b - c) = a - b + c$$ using assms, Ring_ZF_1_L1(3), group_oper_assoc, group0_4_L4A

Another property with three elements.

lemma (in ring0) Ring_ZF_1_L10A:

assumes A1: $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + (b - c) = a + b - c$$ using assms, Ring_ZF_1_L3, Ring_ZF_1_L10

lemma (in ring0) Ring_ZF_1_L11:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + b + c = a + (b + c)$$, $$a\cdot b\cdot c = a\cdot (b\cdot c)$$ using assms, group_oper_assoc, sum_associative

An interpretation of what it means that a ring has no zero divisors.

lemma (in ring0) Ring_ZF_1_L12:

assumes $$\text{HasNoZeroDivs}(R,A,M)$$ and $$a\in R$$, $$a\neq 0$$, $$b\in R$$, $$b\neq 0$$

shows $$a\cdot b\neq 0$$ using assms, HasNoZeroDivs_def

In rings with no zero divisors we can cancel nonzero factors.

lemma (in ring0) Ring_ZF_1_L12A:

assumes A1: $$\text{HasNoZeroDivs}(R,A,M)$$ and A2: $$a\in R$$, $$b\in R$$, $$c\in R$$ and A3: $$a\cdot c = b\cdot c$$ and A4: $$c\neq 0$$

shows $$a=b$$proof
from A2 have T: $$a\cdot c \in R$$, $$a - b \in R$$ using Ring_ZF_1_L4
with A1, A2, A3 have $$a - b = 0 \vee c= 0$$ using Ring_ZF_1_L3, Ring_ZF_1_L8, HasNoZeroDivs_def
with A2, A4 have $$a\in R$$, $$b\in R$$, $$a - b = 0$$
then show $$a=b$$ by (rule Ring_ZF_1_L9A )
qed

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: $$\text{HasNoZeroDivs}(R,A,M)$$, $$a\in R$$, $$b\in R$$, $$c\in R$$, $$a\neq b$$, $$c\neq 0$$

shows $$a\cdot c \neq b\cdot c$$ using A1, Ring_ZF_1_L12A

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: $$\text{HasNoZeroDivs}(R,A,M)$$ and A2: $$a\in R$$, $$b\in R$$ and A3: $$0 \neq a$$, $$1 \neq b$$

shows $$a \neq a\cdot b$$proof
{
assume $$a = a\cdot b$$
with A1, A2 have $$a = 0 \vee b - 1 = 0$$ 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
with A2, A3 have $$False$$ using Ring_ZF_1_L2, Ring_ZF_1_L9A
}
then show $$a \neq a\cdot b$$
qed

If a square is nonzero, then the element is nonzero.

lemma (in ring0) Ring_ZF_1_L13:

assumes $$a\in R$$ and $$a^2 \neq 0$$

shows $$a\neq 0$$ using assms, Ring_ZF_1_L2, Ring_ZF_1_L6

Square of an element and its opposite are the same.

lemma (in ring0) Ring_ZF_1_L14:

assumes $$a\in R$$

shows $$( - a)^2 = ((a)^2)$$ using assms, Ring_ZF_1_L7A

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 \subseteq R$$ and $$H \text{ is closed under } A$$

shows $$(H \cup \{ 0 \}) \text{ is closed under } A$$ using assms, group0_2_L17

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 \subseteq R$$ and A2: $$H \text{ is closed under } M$$

shows $$(H \cup \{ 0 \}) \text{ is closed under } M$$ using assms, Ring_ZF_1_L2, Ring_ZF_1_L6, IsOpClosed_def

The ring is trivial iff $$0=1$$.

lemma (in ring0) Ring_ZF_1_L17:

shows $$R = \{ 0 \} \longleftrightarrow 0 =1$$proof
assume $$R = \{ 0 \}$$
then show $$0 =1$$ using Ring_ZF_1_L2
next
assume A1: $$0 = 1$$
then have $$R \subseteq \{ 0 \}$$ using Ring_ZF_1_L3, Ring_ZF_1_L6
moreover
have $$\{ 0 \} \subseteq R$$ using Ring_ZF_1_L2
ultimately show $$R = \{ 0 \}$$
qed

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\in R$$

shows $$\{m\cdot x.\ x\in R\} = \{( - m)\cdot x.\ x\in R\}$$proof
{
fix $$a$$
assume $$a \in \{m\cdot x.\ x\in R\}$$
then obtain $$x$$ where $$x\in R$$ and $$a = m\cdot x$$
with A1 have $$( - x) \in R$$ and $$a = ( - m)\cdot ( - x)$$ using Ring_ZF_1_L3, Ring_ZF_1_L7A
then have $$a \in \{( - m)\cdot x.\ x\in R\}$$
}
then show $$\{m\cdot x.\ x\in R\} \subseteq \{( - m)\cdot x.\ x\in R\}$$
next
{
fix $$a$$
assume $$a \in \{( - m)\cdot x.\ x\in R\}$$
then obtain $$x$$ where $$x\in R$$ and $$a = ( - m)\cdot x$$
with A1 have $$( - x) \in R$$ and $$a = m\cdot ( - x)$$ using Ring_ZF_1_L3, Ring_ZF_1_L7
then have $$a \in \{m\cdot x.\ x\in R\}$$
}
then show $$\{( - m)\cdot x.\ x\in R\} \subseteq \{m\cdot x.\ x\in R\}$$
qed

### Rearrangement lemmas

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.

Rearrangements with two elements of a ring.

lemma (in ring0) Ring_ZF_2_L1:

assumes $$a\in R$$, $$b\in R$$

shows $$a + b\cdot a = (b + 1 )\cdot a$$ using assms, Ring_ZF_1_L2, ring_oper_distr, Ring_ZF_1_L3, Ring_ZF_1_L4

Rearrangements with two elements and cancelling.

lemma (in ring0) Ring_ZF_2_L1A:

assumes $$a\in R$$, $$b\in R$$

shows $$a - b + b = a$$, $$a + b - a = b$$, $$( - a) + b + a = b$$, $$( - a) + (b + a) = b$$, $$a + (b - a) = b$$ using assms, inv_cancel_two, group0_4_L6A, Ring_ZF_1_L1(3)

In rings $$a-(b+1)c = (a-d-c)+(d-bc)$$ and $$a+b+(c+d) = a+(b+c)+d$$.

lemma (in ring0) Ring_ZF_2_L2:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$, $$d\in R$$

shows $$a - (b + 1 )\cdot c = (a - d - c) + (d - b\cdot c)$$, $$a + b + (c + d) = a + b + c + d$$, $$a + b + (c + d) = a + (b + c) + d$$proof
let $$B = b\cdot c$$
from ringAssum, assms have $$A \text{ is commutative on } R$$ and $$a\in R$$, $$B \in R$$, $$c\in R$$, $$d\in R$$ unfolding IsAring_def using Ring_ZF_1_L4
then have $$a + ( - B + c) = a + ( - d) + ( - c) + (d + ( - B))$$ by (rule group0_4_L8 )
with assms show $$a - (b + 1 )\cdot c = (a - d - c) + (d - b\cdot c)$$ using Ring_ZF_1_L2, ring_oper_distr, Ring_ZF_1_L3
from assms show $$a + b + (c + d) = a + b + c + d$$ using Ring_ZF_1_L4(1), Ring_ZF_1_L10(1)
with assms(1,2,3) show $$a + b + (c + d) = a + (b + c) + d$$ using Ring_ZF_1_L10(1)
qed

lemma (in ring0) Ring_ZF_2_L3:

assumes A1: $$a\in R$$, $$b\in R$$, $$c\in R$$, $$d\in R$$, $$x\in R$$

shows $$(a\cdot x + b) + (c\cdot x + d) = (a + c)\cdot x + (b + d)$$proof
from A1 have $$A \text{ is commutative on } R$$, $$a\cdot x \in R$$, $$b\in R$$, $$c\cdot x \in R$$, $$d\in R$$ using Ring_ZF_1_L1, Ring_ZF_1_L4
then have $$A\langle A\langle a\cdot x,b\rangle ,A\langle c\cdot x,d\rangle \rangle = A\langle A\langle a\cdot x,c\cdot x\rangle ,A\langle b,d\rangle \rangle$$ using group0_4_L8(3)
with A1 show $$(a\cdot x + b) + (c\cdot x + d) = (a + c)\cdot x + (b + d)$$ using ring_oper_distr
qed

Rearrangement with three elements

lemma (in ring0) Ring_ZF_2_L4:

assumes $$M \text{ is commutative on } R$$ and $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b\cdot c) = a\cdot c\cdot b$$ and $$a\cdot b\cdot c = a\cdot c\cdot b$$ using assms, IsCommutative_def, Ring_ZF_1_L11

Some other rearrangements with three elements.

lemma (in ring0) ring_rearr_3_elemA:

assumes A1: $$M \text{ is commutative on } R$$ and A2: $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (a\cdot c) - b\cdot ( - b\cdot c) = (a\cdot a + b\cdot b)\cdot c$$, $$a\cdot ( - b\cdot c) + b\cdot (a\cdot c) = 0$$proof
from A2 have T: $$b\cdot c \in R$$, $$a\cdot a \in R$$, $$b\cdot b \in R$$, $$b\cdot (b\cdot c) \in R$$, $$a\cdot (b\cdot c) \in R$$ using Ring_ZF_1_L4
with A2 show $$a\cdot (a\cdot c) - b\cdot ( - b\cdot c) = (a\cdot a + b\cdot b)\cdot c$$ using Ring_ZF_1_L7, Ring_ZF_1_L3, Ring_ZF_1_L11, ring_oper_distr
from A2, T have $$a\cdot ( - b\cdot c) + b\cdot (a\cdot c) = ( - a\cdot (b\cdot c)) + b\cdot a\cdot c$$ using Ring_ZF_1_L7, Ring_ZF_1_L11
also
from A1, A2, T have $$\ldots = 0$$ using IsCommutative_def, Ring_ZF_1_L11, Ring_ZF_1_L3
finally show $$a\cdot ( - b\cdot c) + b\cdot (a\cdot c) = 0$$
qed

Some rearrangements with four elements. Properties of abelian groups.

lemma (in ring0) Ring_ZF_2_L5:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$, $$d\in R$$

shows $$a - b - c - d = a - d - b - c$$, $$a + b + c - d = a - d + b + c$$, $$a + b - c - d = a - c + (b - d)$$, $$a + b + c + d = a + c + (b + d)$$ using assms, Ring_ZF_1_L1(3), rearr_ab_gr_4_elemB, rearr_ab_gr_4_elemA

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\in R$$, $$b\in R$$, $$c\in R$$, $$d\in R$$, $$e\in R$$, $$f\in R$$

shows $$a\cdot (c\cdot e - d\cdot f) - b\cdot (c\cdot f + d\cdot e) =$$ $$(a\cdot c - b\cdot d)\cdot e - (a\cdot d + b\cdot c)\cdot f$$, $$a\cdot (c\cdot f + d\cdot e) + b\cdot (c\cdot e - d\cdot f) =$$ $$(a\cdot c - b\cdot d)\cdot f + (a\cdot d + b\cdot c)\cdot e$$, $$a\cdot (c + e) - b\cdot (d + f) = a\cdot c - b\cdot d + (a\cdot e - b\cdot f)$$, $$a\cdot (d + f) + b\cdot (c + e) = a\cdot d + b\cdot c + (a\cdot f + b\cdot e)$$proof
from A1 have T: $$c\cdot e \in R$$, $$d\cdot f \in R$$, $$c\cdot f \in R$$, $$d\cdot e \in R$$, $$a\cdot c \in R$$, $$b\cdot d \in R$$, $$a\cdot d \in R$$, $$b\cdot c \in R$$, $$b\cdot f \in R$$, $$a\cdot e \in R$$, $$b\cdot e \in R$$, $$a\cdot f \in R$$, $$a\cdot c\cdot e \in R$$, $$a\cdot d\cdot f \in R$$, $$b\cdot c\cdot f \in R$$, $$b\cdot d\cdot e \in R$$, $$b\cdot c\cdot e \in R$$, $$b\cdot d\cdot f \in R$$, $$a\cdot c\cdot f \in R$$, $$a\cdot d\cdot e \in R$$, $$a\cdot c\cdot e - a\cdot d\cdot f \in R$$, $$a\cdot c\cdot e - b\cdot d\cdot e \in R$$, $$a\cdot c\cdot f + a\cdot d\cdot e \in R$$, $$a\cdot c\cdot f - b\cdot d\cdot f \in R$$, $$a\cdot c + a\cdot e \in R$$, $$a\cdot d + a\cdot f \in R$$ using Ring_ZF_1_L4
with A1 show $$a\cdot (c\cdot e - d\cdot f) - b\cdot (c\cdot f + d\cdot e) =$$ $$(a\cdot c - b\cdot d)\cdot e - (a\cdot d + b\cdot c)\cdot f$$ using Ring_ZF_1_L8, ring_oper_distr, Ring_ZF_1_L11, Ring_ZF_1_L10, Ring_ZF_2_L5
from A1, T show $$a\cdot (c\cdot f + d\cdot e) + b\cdot (c\cdot e - d\cdot f) =$$ $$(a\cdot c - b\cdot d)\cdot f + (a\cdot d + b\cdot c)\cdot 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
from A1, T show $$a\cdot (c + e) - b\cdot (d + f) = a\cdot c - b\cdot d + (a\cdot e - b\cdot f)$$, $$a\cdot (d + f) + b\cdot (c + e) = a\cdot d + b\cdot c + (a\cdot f + b\cdot e)$$ using ring_oper_distr, Ring_ZF_1_L10, Ring_ZF_2_L5
qed
end
Definition of IsAring: $$\text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge$$ $$\text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M)$$
lemma (in ring0) Ring_ZF_1_L1: shows $$monoid0(R,M)$$, $$group0(R,A)$$, $$A \text{ is commutative on } R$$
lemma (in ring0) Ring_ZF_1_L1: shows $$monoid0(R,M)$$, $$group0(R,A)$$, $$A \text{ is commutative on } R$$
Definition of IsDistributive: $$\text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\$$ $$M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge$$ $$M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle )$$
lemma (in group0) group0_2_L2: shows $$1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$$
lemma (in monoid0) unit_is_neutral:

assumes $$e = \text{ TheNeutralElement}(G,f)$$

shows $$e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g)$$
lemma (in group0) group_inv_of_one: shows $$1 ^{-1} = 1$$
lemma (in group0) inverse_in_group:

assumes $$x\in G$$

shows $$x^{-1}\in G$$
lemma (in group0) group_inv_of_inv:

assumes $$a\in G$$

shows $$a = (a^{-1})^{-1}$$
lemma (in group0) group0_2_L6:

assumes $$x\in G$$

shows $$x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1$$
lemma (in ring0) Ring_ZF_1_L2: shows $$0 \in R$$, $$1 \in R$$, $$( - 0 ) = 0$$
lemma (in ring0) ring_oper_distr:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b + c) = a\cdot b + a\cdot c$$, $$(b + c)\cdot a = b\cdot a + c\cdot a$$
lemma (in ring0) Ring_ZF_1_L1: shows $$monoid0(R,M)$$, $$group0(R,A)$$, $$A \text{ is commutative on } R$$
lemma (in ring0) Ring_ZF_1_L3:

assumes $$a\in R$$

shows $$( - a) \in R$$, $$( - ( - a)) = a$$, $$a + 0 = a$$, $$0 + a = a$$, $$a\cdot 1 = a$$, $$1 \cdot a = a$$, $$a - a = 0$$, $$a - 0 = a$$, $$2 \cdot a = a + a$$, $$( - a) + a = 0$$
lemma (in monoid0) group0_1_L1:

assumes $$a\in G$$, $$b\in G$$

shows $$a\oplus b \in G$$
Definition of IsCommutative: $$f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle$$
lemma (in group0) group0_2_L7:

assumes $$a\in G$$ and $$b\in G$$ and $$a\cdot b = a$$

shows $$b=1$$
lemma (in ring0) Ring_ZF_1_L4:

assumes $$a\in R$$, $$b\in R$$

shows $$a + b \in R$$, $$a - b \in R$$, $$a\cdot b \in R$$, $$a + b = b + a$$

assumes $$a\in R$$, $$b\in R$$ and $$a + b = a$$

shows $$b = 0$$
lemma (in ring0) Ring_ZF_1_L6:

assumes $$x\in R$$

shows $$0 \cdot x = 0$$, $$x\cdot 0 = 0$$
lemma (in group0) group0_2_L9:

assumes $$a\in G$$ and $$b\in G$$ and $$a\cdot b = 1$$

shows $$a = b^{-1}$$ and $$b = a^{-1}$$
lemma (in ring0) Ring_ZF_1_L7:

assumes $$a\in R$$, $$b\in R$$

shows $$( - a)\cdot b = - (a\cdot b)$$, $$a\cdot ( - b) = - (a\cdot b)$$, $$( - a)\cdot b = a\cdot ( - b)$$
lemma (in group0) group0_4_L4:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$

shows $$b^{-1}\cdot a^{-1} = a^{-1}\cdot b^{-1}$$, $$(a\cdot b)^{-1} = a^{-1}\cdot b^{-1}$$, $$(a\cdot b^{-1})^{-1} = a^{-1}\cdot b$$
lemma (in group0) group0_2_L11A:

assumes $$a\in G$$, $$b\in G$$ and $$a\cdot b^{-1} = 1$$

shows $$a=b$$
lemma (in group0) group_oper_assoc:

assumes $$a\in G$$, $$b\in G$$, $$c\in G$$

shows $$a\cdot (b\cdot c) = a\cdot b\cdot c$$
lemma (in group0) group0_4_L4A:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$, $$c\in G$$

shows $$a\cdot b\cdot c = c\cdot a\cdot b$$, $$a^{-1}\cdot (b^{-1}\cdot c^{-1})^{-1} = (a\cdot (b\cdot c)^{-1})^{-1}$$, $$a\cdot (b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1}$$, $$a\cdot (b\cdot c^{-1})^{-1} = a\cdot b^{-1}\cdot c$$, $$a\cdot b^{-1}\cdot c^{-1} = a\cdot c^{-1}\cdot b^{-1}$$
lemma (in ring0) Ring_ZF_1_L10:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + (b + c) = a + b + c$$, $$a - (b + c) = a - b - c$$, $$a - (b - c) = a - b + c$$
lemma (in monoid0) sum_associative:

assumes $$a\in G$$, $$b\in G$$, $$c\in G$$

shows $$(a\oplus b)\oplus c = a\oplus (b\oplus c)$$
Definition of HasNoZeroDivs: $$\text{HasNoZeroDivs}(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\$$ $$M\langle a,b\rangle = \text{ TheNeutralElement}(R,A) \longrightarrow$$ $$a = \text{ TheNeutralElement}(R,A) \vee b = \text{ TheNeutralElement}(R,A))$$
lemma (in ring0) Ring_ZF_1_L8:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b - c) = a\cdot b - a\cdot c$$, $$(b - c)\cdot a = b\cdot a - c\cdot a$$
lemma (in ring0) Ring_ZF_1_L9A:

assumes $$a\in R$$, $$b\in R$$ and $$a - b = 0$$

shows $$a=b$$
lemma (in ring0) Ring_ZF_1_L12A:

assumes $$\text{HasNoZeroDivs}(R,A,M)$$ and $$a\in R$$, $$b\in R$$, $$c\in R$$ and $$a\cdot c = b\cdot c$$ and $$c\neq 0$$

shows $$a=b$$
lemma (in ring0) Ring_ZF_1_L7A:

assumes $$a\in R$$, $$b\in R$$

shows $$( - a)\cdot ( - b) = a\cdot b$$
lemma (in group0) group0_2_L17:

assumes $$H\subseteq G$$ and $$H \text{ is closed under } P$$

shows $$(H \cup \{1 \}) \text{ is closed under } P$$
Definition of IsOpClosed: $$A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A$$
lemma (in group0) inv_cancel_two:

assumes $$a\in G$$, $$b\in G$$

shows $$a\cdot b^{-1}\cdot b = a$$, $$a\cdot b\cdot b^{-1} = a$$, $$a^{-1}\cdot (a\cdot b) = b$$, $$a\cdot (a^{-1}\cdot b) = b$$
lemma (in group0) group0_4_L6A:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$

shows $$a\cdot b\cdot a^{-1} = b$$, $$a^{-1}\cdot b\cdot a = b$$, $$a^{-1}\cdot (b\cdot a) = b$$, $$a\cdot (b\cdot a^{-1}) = b$$
lemma (in group0) group0_4_L8:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$, $$c\in G$$, $$d\in G$$

shows $$a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1})$$, $$a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d)$$, $$a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d)$$, $$a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1}$$, $$(a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1}$$
lemma (in ring0) Ring_ZF_1_L4:

assumes $$a\in R$$, $$b\in R$$

shows $$a + b \in R$$, $$a - b \in R$$, $$a\cdot b \in R$$, $$a + b = b + a$$
lemma (in ring0) Ring_ZF_1_L10:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + (b + c) = a + b + c$$, $$a - (b + c) = a - b - c$$, $$a - (b - c) = a - b + c$$
lemma (in ring0) Ring_ZF_1_L1: shows $$monoid0(R,M)$$, $$group0(R,A)$$, $$A \text{ is commutative on } R$$
lemma (in group0) group0_4_L8:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$, $$c\in G$$, $$d\in G$$

shows $$a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1})$$, $$a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d)$$, $$a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d)$$, $$a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1}$$, $$(a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1}$$
lemma (in ring0) Ring_ZF_1_L11:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + b + c = a + (b + c)$$, $$a\cdot b\cdot c = a\cdot (b\cdot c)$$
lemma (in group0) rearr_ab_gr_4_elemB:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$, $$c\in G$$, $$d\in G$$

shows $$a\cdot b^{-1}\cdot c^{-1}\cdot d^{-1} = a\cdot d^{-1}\cdot b^{-1}\cdot c^{-1}$$, $$a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c$$, $$a\cdot b\cdot c^{-1}\cdot d^{-1} = a\cdot c^{-1}\cdot (b\cdot d^{-1})$$
lemma (in group0) rearr_ab_gr_4_elemA:

assumes $$P \text{ is commutative on } G$$ and $$a\in G$$, $$b\in G$$, $$c\in G$$, $$d\in G$$

shows $$a\cdot b\cdot c\cdot d = a\cdot d\cdot b\cdot c$$, $$a\cdot b\cdot c\cdot d = a\cdot c\cdot (b\cdot d)$$
lemma (in ring0) Ring_ZF_2_L5:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$, $$d\in R$$

shows $$a - b - c - d = a - d - b - c$$, $$a + b + c - d = a - d + b + c$$, $$a + b - c - d = a - c + (b - d)$$, $$a + b + c + d = a + c + (b + d)$$
lemma (in ring0) Ring_ZF_1_L10A:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + (b - c) = a + b - c$$