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_defThe theorems proven in in group0 context (locale) are valid in the ring0 context when applied to the additive group of the ring.
sublocale ring0 < add_group: group0
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_defZero 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_oneThe 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_distrProperties 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_defCancellation 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, group0_2_L7Any 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
qed
from T2, T1 have \( d = 0 \) using ring_cancel_add
ultimately show \( x\cdot 0 = 0 \), \( 0 \cdot x = 0 \)
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
ultimately show \( ( - a)\cdot b = - (a\cdot b) \) using group0_2_L9
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
qed
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 \)
moreover
qed
from I, II show \( a\cdot ( - b) = - (a\cdot b) \) using group0_2_L9
ultimately show \( ( - a)\cdot b = a\cdot ( - b) \)
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_L4Subtraction 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_L4Other 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_invIf 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, assmsOther 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_L4AAnother 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_L10Associativity 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, group_oper_assoc, sum_associativeAn 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_defIn 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_L12AIn 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_L6Square 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_L7AAdding 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_L17Adding 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_defThe 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
qed
have \( \{ 0 \} \subseteq R \) using Ring_ZF_1_L2
ultimately show \( R = \{ 0 \} \)
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_L4Rearrangements 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
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 \( 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_L11Some 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
qed
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 \)
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_elemATwo 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 \) 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 \) 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 \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8