P. 132 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscmn 13101*	The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. CMnd <-> ( G e. Mnd /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
Theorem	isabl2 13102*	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
Theorem	cmnpropd 13103*	If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. CMnd <-> L e. CMnd ) )
Theorem	ablpropd 13104*	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. Abel <-> L e. Abel ) )
Theorem	ablprop 13105	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Abel <-> L e. Abel )
Theorem	iscmnd 13106*	Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. CMnd )
Theorem	isabld 13107*	Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. Abel )
Theorem	isabli 13108*	Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
|- G e. Grp   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- G e. Abel
Theorem	cmnmnd 13109	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. CMnd -> G e. Mnd )
Theorem	cmncom 13110	A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	ablcom 13111	An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	cmn32 13112	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmn4 13113	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
Theorem	cmn12 13114	Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
Theorem	abl32 13115	Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmnmndd 13116	A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. CMnd )   =>    |- ( ph -> G e. Mnd )
Theorem	rinvmod 13117*	Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6070. (Contributed by AV, 31-Dec-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E* w e. B ( A .+ w ) = .0. )
Theorem	ablinvadd 13118	The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( N ` ( X .+ Y ) ) = ( ( N ` X ) .+ ( N ` Y ) ) )
Theorem	ablsub2inv 13119	Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( Y .- X ) )
Theorem	ablsubadd 13120	Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Y .+ Z ) = X ) )
Theorem	ablsub4 13121	Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) )
Theorem	abladdsub4 13122	Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) = ( Z .+ W ) <-> ( X .- Z ) = ( W .- Y ) ) )
Theorem	abladdsub 13123	Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( X .- Z ) .+ Y ) )
Theorem	ablpncan2 13124	Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = Y )
Theorem	ablpncan3 13125	A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = Y )
Theorem	ablsubsub 13126	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .- ( Y .- Z ) ) = ( ( X .- Y ) .+ Z ) )
Theorem	ablsubsub4 13127	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y .+ Z ) ) )
Theorem	ablpnpcan 13128	Cancellation law for mixed addition and subtraction. (pnpcan 8198 analog.) (Contributed by NM, 29-May-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( Y .- Z ) )
Theorem	ablnncan 13129	Cancellation law for group subtraction. (nncan 8188 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .- ( X .- Y ) ) = Y )
Theorem	ablsub32 13130	Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- Z ) = ( ( X .- Z ) .- Y ) )
Theorem	ablnnncan 13131	Cancellation law for group subtraction. (nnncan 8194 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- ( Y .- Z ) ) .- Z ) = ( X .- Y ) )
Theorem	ablnnncan1 13132	Cancellation law for group subtraction. (nnncan1 8195 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( Z .- Y ) )
Theorem	ablsubsub23 13133	Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( A .- C ) = B ) )
Theorem	subcmnd 13134	A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- ( ph -> H = ( G ↾s S ) )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> S e. V )   =>    |- ( ph -> H e. CMnd )
7.3  Rings
7.3.1  Multiplicative Group
Syntax	cmgp 13135	Multiplicative group.
class mulGrp
Definition	df-mgp 13136	Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" or "the multiplicative identity" in terms of the identity of a monoid (df-ur 13148). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 13137	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V
Theorem	mgpvalg 13138	Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. V -> M = ( R sSet <. ( +g ` ndx ) , .x. >. ) )
Theorem	mgpplusgg 13139	Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. V -> .x. = ( +g ` M ) )
Theorem	mgpex 13140	Existence of the multiplication group. If R is known to be a semiring, see srgmgp 13156. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- M = (mulGrp ` R )   =>    |- ( R e. V -> M e. _V )
Theorem	mgpbasg 13141	Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. V -> B = ( Base ` M ) )
Theorem	mgpscag 13142	The multiplication monoid has the same (if any) scalars as the original ring. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.)
|- M = (mulGrp ` R )   &    |- S = (Scalar ` R )   =>    |- ( R e. V -> S = (Scalar ` M ) )
Theorem	mgptsetg 13143	Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   =>    |- ( R e. V -> (TopSet ` R ) = (TopSet ` M ) )
Theorem	mgptopng 13144	Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- J = ( TopOpen ` R )   =>    |- ( R e. V -> J = ( TopOpen ` M ) )
Theorem	mgpdsg 13145	Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( dist ` R )   =>    |- ( R e. V -> B = ( dist ` M ) )
Theorem	mgpress 13146	Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.)
|- S = ( R ↾s A )   &    |- M = (mulGrp ` R )   =>    |- ( ( R e. V /\ A e. W ) -> ( M ↾s A ) = (mulGrp ` S ) )
7.3.2  Ring unity (multiplicative identity) In Wikipedia "Identity element", see https://en.wikipedia.org/wiki/Identity_element (18-Jan-2025): "... an identity with respect to multiplication is called a multiplicative identity (often denoted as 1). ... The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity). This should not be confused with a unit in ring theory, which is any element having a multiplicative inverse. By its own definition, unity itself is necessarily a unit." Calling the multiplicative identity of a ring a unity is taken from the definition of a ring with unity in section 17.3 of [BeauregardFraleigh] p. 135, "A ring ( R , + , . ) is a ring with unity if R is not the zero ring and ( R , . ) is a monoid. In this case, the identity element of ( R , . ) is denoted by 1 and is called the unity of R." This definition of a "ring with unity" corresponds to our definition of a unital ring (see df-ring 13186). Some authors call the multiplicative identity "unit" or "unit element" (for example in section I, 2.2 of [BourbakiAlg1] p. 14, definition in section 1.3 of [Hall] p. 4, or in section I, 1 of [Lang] p. 3), whereas other authors use the term "unit" for an element having a multiplicative inverse (for example in section 17.3 of [BeauregardFraleigh] p. 135, in definition in [Roman] p. 26, or even in section II, 1 of [Lang] p. 84). Sometimes, the multiplicative identity is simply called "one" (see, for example, chapter 8 in [Schechter] p. 180). To avoid this ambiguity of the term "unit", also mentioned in Wikipedia, we call the multiplicative identity of a structure with a multiplication (usually a ring) a "ring unity", or straightly "multiplicative identity". The term "unit" will be used for an element having a multiplicative inverse (see https://us.metamath.org/mpeuni/df-unit.html 13186 in set.mm), and we have "the ring unity is a unit", see https://us.metamath.org/mpeuni/1unit.html 13186.
Syntax	cur 13147	Extend class notation with ring unity.
class 1r
Definition	df-ur 13148	Define the multiplicative identity, i.e., the monoid identity (df-0g 12712) of the multiplicative monoid (df-mgp 13136) of a ring-like structure. This multiplicative identity is also called "ring unity" or "unity element". This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot. See also dfur2g 13150, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- 1r = ( 0g o. mulGrp )
Theorem	ringidvalg 13149	The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- G = (mulGrp ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. V -> .1. = ( 0g ` G ) )
Theorem	dfur2g 13150*	The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. V -> .1. = ( iota e ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) )
7.3.3  Semirings
Syntax	csrg 13151	Extend class notation with the class of all semirings.
class SRing
Definition	df-srg 13152*	Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Like with rings, the additive identity is an absorbing element of the multiplicative law, but in the case of semirings, this has to be part of the definition, as it cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- SRing = { f e. CMnd | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) ) ) }
Theorem	issrg 13153*	The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- B = ( Base ` R )   &    |- G = (mulGrp ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. SRing <-> ( R e. CMnd /\ G e. Mnd /\ A. x e. B ( A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ ( ( .0. .x. x ) = .0. /\ ( x .x. .0. ) = .0. ) ) ) )
Theorem	srgcmn 13154	A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. CMnd )
Theorem	srgmnd 13155	A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. Mnd )
Theorem	srgmgp 13156	A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- G = (mulGrp ` R )   =>    |- ( R e. SRing -> G e. Mnd )
Theorem	srgdilem 13157	Lemma for srgdi 13162 and srgdir 13163. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
Theorem	srgcl 13158	Closure of the multiplication operation of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
Theorem	srgass 13159	Associative law for the multiplication operation of a semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. Y ) .x. Z ) = ( X .x. ( Y .x. Z ) ) )
Theorem	srgideu 13160*	The unity element of a semiring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. SRing -> E! u e. B A. x e. B ( ( u .x. x ) = x /\ ( x .x. u ) = x ) )
Theorem	srgfcl 13161	Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by AV, 24-Aug-2021.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ .x. Fn ( B X. B ) ) -> .x. : ( B X. B ) --> B )
Theorem	srgdi 13162	Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) )
Theorem	srgdir 13163	Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
Theorem	srgidcl 13164	The unity element of a semiring belongs to the base set of the semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. SRing -> .1. e. B )
Theorem	srg0cl 13165	The zero element of a semiring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. SRing -> .0. e. B )
Theorem	srgidmlem 13166	Lemma for srglidm 13167 and srgridm 13168. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( ( .1. .x. X ) = X /\ ( X .x. .1. ) = X ) )
Theorem	srglidm 13167	The unity element of a semiring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( .1. .x. X ) = X )
Theorem	srgridm 13168	The unity element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( X .x. .1. ) = X )
Theorem	issrgid 13169*	Properties showing that an element I is the unity element of a semiring. (Contributed by NM, 7-Aug-2013.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. SRing -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )
Theorem	srgacl 13170	Closure of the addition operation of a semiring. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. SRing /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	srgcom 13171	Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. SRing /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	srgrz 13172	The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( X .x. .0. ) = .0. )
Theorem	srglz 13173	The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( .0. .x. X ) = .0. )
Theorem	srgisid 13174*	In a semiring, the only left-absorbing element is the additive identity. Remark in [Golan] p. 1. (Contributed by Thierry Arnoux, 1-May-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> Z e. B )   &    |- ( ( ph /\ x e. B ) -> ( Z .x. x ) = Z )   =>    |- ( ph -> Z = .0. )
Theorem	srg1zr 13175	The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	srgen1zr 13176	The only semiring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- Z = ( 0g ` R )   =>    |- ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	srgmulgass 13177	An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019.)
|- B = ( Base ` R )   &    |- .x. = (.g ` R )   &    |- .X. = ( .r ` R )   =>    |- ( ( R e. SRing /\ ( N e. NN0 /\ X e. B /\ Y e. B ) ) -> ( ( N .x. X ) .X. Y ) = ( N .x. ( X .X. Y ) ) )
Theorem	srgpcomp 13178	If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019.)
|- S = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- G = (mulGrp ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( A .X. B ) = ( B .X. A ) )   =>    |- ( ph -> ( ( K .^ B ) .X. A ) = ( A .X. ( K .^ B ) ) )
Theorem	srgpcompp 13179	If two elements of a semiring commute, they also commute if the elements are raised to a higher power. (Contributed by AV, 23-Aug-2019.)
|- S = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- G = (mulGrp ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( A .X. B ) = ( B .X. A ) )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) = ( ( ( N + 1 ) .^ A ) .X. ( K .^ B ) ) )
Theorem	srgpcomppsc 13180	If two elements of a semiring commute, they also commute if the elements are raised to a higher power and a scalar multiplication is involved. (Contributed by AV, 23-Aug-2019.)
|- S = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- G = (mulGrp ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> ( A .X. B ) = ( B .X. A ) )   &    |- ( ph -> N e. NN0 )   &    |- .x. = (.g ` R )   &    |- ( ph -> C e. NN0 )   =>    |- ( ph -> ( ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) .X. A ) = ( C .x. ( ( ( N + 1 ) .^ A ) .X. ( K .^ B ) ) ) )
Theorem	srglmhm 13181*	Left-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism. (Contributed by AV, 23-Aug-2019.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( X .x. x ) ) e. ( R MndHom R ) )
Theorem	srgrmhm 13182*	Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism. (Contributed by AV, 23-Aug-2019.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) e. ( R MndHom R ) )
Theorem	srg1expzeq1 13183	The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 13015. (Contributed by AV, 25-Nov-2019.)
|- G = (mulGrp ` R )   &    |- .x. = (.g ` G )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. SRing /\ N e. NN0 ) -> ( N .x. .1. ) = .1. )
7.3.4  Definition and basic properties of unital rings
Syntax	crg 13184	Extend class notation with class of all (unital) rings.
class Ring
Syntax	ccrg 13185	Extend class notation with class of all (unital) commutative rings.
class CRing
Definition	df-ring 13186*	Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition of a ring with identity in part Preliminaries of [Roman] p. 19. So that the additive structure must be abelian (see ringcom 13219), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- Ring = { f e. Grp | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
Definition	df-cring 13187	Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
Theorem	isring 13188*	The predicate "is a (unital) ring". Definition of "ring with unit" in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- G = (mulGrp ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring <-> ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
Theorem	ringgrp 13189	A ring is a group. (Contributed by NM, 15-Sep-2011.)
|- ( R e. Ring -> R e. Grp )
Theorem	ringmgp 13190	A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- G = (mulGrp ` R )   =>    |- ( R e. Ring -> G e. Mnd )
Theorem	iscrng 13191	A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- G = (mulGrp ` R )   =>    |- ( R e. CRing <-> ( R e. Ring /\ G e. CMnd ) )
Theorem	crngmgp 13192	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- G = (mulGrp ` R )   =>    |- ( R e. CRing -> G e. CMnd )
Theorem	ringgrpd 13193	A ring is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. Ring )   =>    |- ( ph -> R e. Grp )
Theorem	ringmnd 13194	A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. Mnd )
Theorem	ringmgm 13195	A ring is a magma. (Contributed by AV, 31-Jan-2020.)
|- ( R e. Ring -> R e. Mgm )
Theorem	crngring 13196	A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. CRing -> R e. Ring )
Theorem	crngringd 13197	A commutative ring is a ring. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. CRing )   =>    |- ( ph -> R e. Ring )
Theorem	crnggrpd 13198	A commutative ring is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. CRing )   =>    |- ( ph -> R e. Grp )
Theorem	mgpf 13199	Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- (mulGrp |` Ring ) : Ring --> Mnd
Theorem	ringdilem 13200	Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )