IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

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 \( a + b \equiv A\langle a,b\rangle \)

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

defines \( a - b \equiv a + ( - b) \)

defines \( a\cdot b \equiv M\langle a,b\rangle \)

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

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

defines \( 2 \equiv 1 + 1 \)

defines \( a^2 \equiv a\cdot a \)

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 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 Ring_ZF_1_L1 , 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 , Ring_ZF_1_L1 , 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 ringAssum , assms , Ring_ZF_1_L1 , Ring_ZF_1_L3 , group0_2_L1 , group0_1_L1 , IsAring_def , 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.

lemma (in ring0) ring_cancel_add:

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

shows \( b = 0 \) using assms , Ring_ZF_1_L1 , 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 Ring_ZF_1_L1 , 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 Ring_ZF_1_L1 , group0_2_L9
moreover
from I, II show \( a\cdot ( - b) = - (a\cdot b) \) using Ring_ZF_1_L1 , 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 , ringAssum , IsAring_def , Ring_ZF_1_L1 , 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 \)proof
from A1, A2 have \( group0(R,A) \), \( a\in R \), \( b\in R \), \( A\langle a, \text{GroupInv}(R,A)(b)\rangle = \text{TheNeutralElement}(R,A) \) using Ring_ZF_1_L1
then show \( a=b \) by (rule group0_2_L11A )
qed

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 , ringAssum , Ring_ZF_1_L1 , group_oper_assoc , IsAring_def , 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

Associativity of addition and multiplication.

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 , ringAssum , Ring_ZF_1_L1 , group_oper_assoc , IsAring_def , IsAmonoid_def , IsAssociative_def

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 , Ring_ZF_1_L1 , 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 , Ring_ZF_1_L1 , inv_cancel_two , group0_4_L6A

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\in R \), \( b\in R \), \( c\in R \), \( d\in R \)

shows \( a - (b + 1 )\cdot c = (a - d - c) + (d - b\cdot c) \)proof
let \( B = b\cdot c \)
from ringAssum have \( A \text{ is commutative on } R \) using IsAring_def
moreover
from A1 have \( a\in R \), \( B \in R \), \( c\in R \), \( d\in R \) using Ring_ZF_1_L4
ultimately have \( A\langle a, \text{GroupInv}(R,A)(A\langle B, c\rangle )\rangle =\) \( A\langle A\langle A\langle a, \text{GroupInv}(R, A)(d)\rangle , \text{GroupInv}(R, A)(c)\rangle ,\) \( A\langle d, \text{GroupInv}(R, A)(B)\rangle \rangle \) using Ring_ZF_1_L1 , group0_4_L8
with A1 show \( thesis \) using Ring_ZF_1_L2 , ring_oper_distr , Ring_ZF_1_L3
qed

Rerrangement about adding linear functions.

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 \( group0(R,A) \), \( 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 \) by (rule group0_4_L8 )
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 \) 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 , 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) \)
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 ring0) Ring_ZF_1_L1: shows \( monoid0(R,M) \), \( group0(R,A) \), \( A \text{ is commutative on } R \)
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_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 group0) group0_2_L1: shows \( monoid0(G,P) \)
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 \)
lemma (in ring0) ring_cancel_add:

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 \)
Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative: \( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
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_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 \)
66
145
15
15