P. 140 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13901-14000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mgpvalg 13901	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 13902	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 13903	Existence of the multiplication group. If R is known to be a semiring, see srgmgp 13946. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- M = (mulGrp ` R )   =>    |- ( R e. V -> M e. _V )
Theorem	mgpbasg 13904	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 13905	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 13906	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 13907	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 13908	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 13909	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  Non-unital rings ("rngs") According to Wikipedia, "... in abstract algebra, a rng (or non-unital ring or pseudo-ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 28-Mar-2025).
Syntax	crng 13910	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng 13911*	Define the class of all non-unital rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)
|- Rng = { f e. Abel | ( (mulGrp ` f ) e. Smgrp /\ [. ( Base ` f ) / b ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
Theorem	isrng 13912*	The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
|- B = ( Base ` R )   &    |- G = (mulGrp ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ 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	rngabl 13913	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 13914	A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.)
|- G = (mulGrp ` R )   =>    |- ( R e. Rng -> G e. Smgrp )
Theorem	rngmgpf 13915	Restricted functionality of the multiplicative group on non-unital rings (mgpf 13989 analog). (Contributed by AV, 22-Feb-2025.)
|- (mulGrp |` Rng ) :Rng -->Smgrp
Theorem	rnggrp 13916	A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
|- ( R e. Rng -> R e. Grp )
Theorem	rngass 13917	Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. Y ) .x. Z ) = ( X .x. ( Y .x. Z ) ) )
Theorem	rngdi 13918	Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) )
Theorem	rngdir 13919	Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
Theorem	rngacl 13920	Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	rng0cl 13921	The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Rng -> .0. e. B )
Theorem	rngcl 13922	Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
Theorem	rnglz 13923	The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 14021. (Revised by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = .0. )
Theorem	rngrz 13924	The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 14022. (Revised by AV, 16-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ X e. B ) -> ( X .x. .0. ) = .0. )
Theorem	rngmneg1 13925	Negation of a product in a non-unital ring (mulneg1 8552 analog). In contrast to ringmneg1 14031, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. Y ) = ( N ` ( X .x. Y ) ) )
Theorem	rngmneg2 13926	Negation of a product in a non-unital ring (mulneg2 8553 analog). In contrast to ringmneg2 14032, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) )
Theorem	rngm2neg 13927	Double negation of a product in a non-unital ring (mul2neg 8555 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 14033. (Revised by AV, 17-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )
Theorem	rngansg 13928	Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.)
|- ( R e. Rng -> (NrmSGrp ` R ) = (SubGrp ` R ) )
Theorem	rngsubdi 13929	Ring multiplication distributes over subtraction. (subdi 8542 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 14034. (Revised by AV, 23-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) )
Theorem	rngsubdir 13930	Ring multiplication distributes over subtraction. (subdir 8543 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 14035. (Revised by AV, 23-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )
Theorem	isrngd 13931*	Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> R e. Abel )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )   =>    |- ( ph -> R e. Rng )
Theorem	rngressid 13932	A non-unital ring restricted to its base set is a non-unital ring. It will usually be the original non-unital ring exactly, of course, but to show that needs additional conditions such as those in strressid 13119. (Contributed by Jim Kingdon, 5-May-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Rng -> ( G ↾s B ) e. Rng )
Theorem	rngpropd 13933*	If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( K e. Rng <-> L e. Rng ) )
Theorem	imasrng 13934*	The image structure of a non-unital ring is a non-unital ring (imasring 14042 analog). (Contributed by AV, 22-Feb-2025.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> R e. Rng )   =>    |- ( ph -> U e. Rng )
Theorem	imasrngf1 13935	The image of a non-unital ring under an injection is a non-unital ring. (Contributed by AV, 22-Feb-2025.)
|- U = ( F "s R )   &    |- V = ( Base ` R )   =>    |- ( ( F : V -1-1-> B /\ R e. Rng ) -> U e. Rng )
Theorem	qusrng 13936*	The quotient structure of a non-unital ring is a non-unital ring (qusring2 14044 analog). (Contributed by AV, 23-Feb-2025.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ph -> R e. Rng )   =>    |- ( ph -> U e. Rng )
7.3.3  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 13976). 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 13976 in set.mm), and we have "the ring unity is a unit", see https://us.metamath.org/mpeuni/1unit.html 13976.
Syntax	cur 13937	Extend class notation with ring unity.
class 1r
Definition	df-ur 13938	Define the multiplicative identity, i.e., the monoid identity (df-0g 13306) of the multiplicative monoid (df-mgp 13899) 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 13940, 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 13939	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 13940*	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.4  Semirings
Syntax	csrg 13941	Extend class notation with the class of all semirings.
class SRing
Definition	df-srg 13942*	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 13943*	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 13944	A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. CMnd )
Theorem	srgmnd 13945	A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. Mnd )
Theorem	srgmgp 13946	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 13947	Lemma for srgdi 13952 and srgdir 13953. (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 13948	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 13949	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 13950*	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 13951	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 13952	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 13953	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 13954	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 13955	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 13956	Lemma for srglidm 13957 and srgridm 13958. (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 13957	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 13958	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 13959*	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 13960	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 13961	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 13962	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 13963	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 13964*	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 13965	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 13966	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 13967	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 13968	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 13969	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 13970	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 13971*	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 13972*	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 13973	The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 13701. (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.5  Definition and basic properties of unital rings
Syntax	crg 13974	Extend class notation with class of all (unital) rings.
class Ring
Syntax	ccrg 13975	Extend class notation with class of all (unital) commutative rings.
class CRing
Definition	df-ring 13976*	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 14009), 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 13977	Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
Theorem	isring 13978*	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 13979	A ring is a group. (Contributed by NM, 15-Sep-2011.)
|- ( R e. Ring -> R e. Grp )
Theorem	ringmgp 13980	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 13981	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 13982	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 13983	A ring is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. Ring )   =>    |- ( ph -> R e. Grp )
Theorem	ringmnd 13984	A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. Mnd )
Theorem	ringmgm 13985	A ring is a magma. (Contributed by AV, 31-Jan-2020.)
|- ( R e. Ring -> R e. Mgm )
Theorem	crngring 13986	A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. CRing -> R e. Ring )
Theorem	crngringd 13987	A commutative ring is a ring. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. CRing )   =>    |- ( ph -> R e. Ring )
Theorem	crnggrpd 13988	A commutative ring is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. CRing )   =>    |- ( ph -> R e. Grp )
Theorem	mgpf 13989	Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- (mulGrp |` Ring ) : Ring --> Mnd
Theorem	ringdilem 13990	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 ) ) ) )
Theorem	ringcl 13991	Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
Theorem	crngcom 13992	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
Theorem	iscrng2 13993*	A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. CRing <-> ( R e. Ring /\ A. x e. B A. y e. B ( x .x. y ) = ( y .x. x ) ) )
Theorem	ringass 13994	Associative law for multiplication in a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. Y ) .x. Z ) = ( X .x. ( Y .x. Z ) ) )
Theorem	ringideu 13995*	The unity element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> E! u e. B A. x e. B ( ( u .x. x ) = x /\ ( x .x. u ) = x ) )
Theorem	ringdi 13996	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- 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 ) ) )
Theorem	ringdir 13997	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
Theorem	ringidcl 13998	The unity element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. e. B )
Theorem	ring0cl 13999	The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> .0. e. B )
Theorem	ringidmlem 14000	Lemma for ringlidm 14001 and ringridm 14002. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( ( .1. .x. X ) = X /\ ( X .x. .1. ) = X ) )