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 \)
defines \( \sum s \equiv \text{Fold}(A, 0 ,s) \)
defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)
defines \( \prod s \equiv \text{Fold}(M,1 ,s) \)
defines \( x^{n} \equiv \prod \{\langle k,x\rangle .\ k\in n\} \)
In the ring0 context we can use theorems proven in some other contexts.
lemma (in ring0) Ring_ZF_1_L1:
shows \( monoid0(R,M) \), \( monoid1(R,M) \), \( group0(R,A) \), \( A \text{ is commutative on } R \) using ringAssum, IsAring_def, group0_def, monoid0_def, monoid1_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(3) unfolding ringa_def, ringminus_def, ringzero_def
The theorems proven in the monoid0 context are valid in the ring0 context when applied to the multiplicative monoid of the ring.
sublocale ring0 < mult_monoid: monoid1
using Ring_ZF_1_L1(2) 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 \), \( 2 \in R \) using group0_2_L2, unit_is_neutral, group_inv_of_one, group_op_closedThe 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(4), 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(4), 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(4), 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_defIf ring has no zero divisors then the set of nonzero elements is closed with respect to multiplication, hence with respect to multiplication restricted to that set.
lemma (in ring0) nozerodivs_nonzero_closed:
assumes \( \text{HasNoZeroDivs}(R,A,M) \)
shows \( (R\setminus \{ 0 \}) \text{ is closed under } M \) and \( (R\setminus \{ 0 \}) \text{ is closed under } \text{restrict}(M,(R\setminus \{ 0 \})\times (R\setminus \{ 0 \})) \) using assms, Ring_ZF_1_L4(3), Ring_ZF_1_L12, func_ZF_4_L5 unfolding IsOpClosed_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(4)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(4), 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) \), \( monoid1(R,M) \), \( group0(R,A) \), \( A \text{ is commutative on } R \)
lemma (in ring0) Ring_ZF_1_L1: shows \( monoid0(R,M) \), \( monoid1(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) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) 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 \), \( 2 \in R \)
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) \), \( monoid1(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_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_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 \) lemma func_ZF_4_L5:
assumes \( A \text{ is closed under } f \) and \( A\subseteq B \)
shows \( A \text{ is closed under } \text{restrict}(f,B\times B) \)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 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 \) 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) \), \( monoid1(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 Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
