P. 141 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14001-14100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mgpplusgg 14001	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 14002	Existence of the multiplication group. If R is known to be a semiring, see srgmgp 14045. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- M = (mulGrp ` R )   =>    |- ( R e. V -> M e. _V )
Theorem	mgpbasg 14003	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 14004	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 14005	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 14006	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 14007	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 14008	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 14009	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng 14010*	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 14011*	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 14012	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 14013	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 14014	Restricted functionality of the multiplicative group on non-unital rings (mgpf 14088 analog). (Contributed by AV, 22-Feb-2025.)
|- (mulGrp |` Rng ) :Rng -->Smgrp
Theorem	rnggrp 14015	A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
|- ( R e. Rng -> R e. Grp )
Theorem	rngass 14016	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 14017	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 14018	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 14019	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 14020	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 14021	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 14022	The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 14120. (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 14023	The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 14121. (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 14024	Negation of a product in a non-unital ring (mulneg1 8616 analog). In contrast to ringmneg1 14130, 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 14025	Negation of a product in a non-unital ring (mulneg2 8617 analog). In contrast to ringmneg2 14131, 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 14026	Double negation of a product in a non-unital ring (mul2neg 8619 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 14132. (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 14027	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 14028	Ring multiplication distributes over subtraction. (subdi 8606 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 14133. (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 14029	Ring multiplication distributes over subtraction. (subdir 8607 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 14134. (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 14030*	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 14031	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 13217. (Contributed by Jim Kingdon, 5-May-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Rng -> ( G ↾s B ) e. Rng )
Theorem	rngpropd 14032*	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 14033*	The image structure of a non-unital ring is a non-unital ring (imasring 14141 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 14034	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 14035*	The quotient structure of a non-unital ring is a non-unital ring (qusring2 14143 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 14075). 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 14075 in set.mm), and we have "the ring unity is a unit", see https://us.metamath.org/mpeuni/1unit.html 14075.
Syntax	cur 14036	Extend class notation with ring unity.
class 1r
Definition	df-ur 14037	Define the multiplicative identity, i.e., the monoid identity (df-0g 13404) of the multiplicative monoid (df-mgp 13998) 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 14039, 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 14038	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 14039*	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 14040	Extend class notation with the class of all semirings.
class SRing
Definition	df-srg 14041*	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 14042*	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 14043	A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. CMnd )
Theorem	srgmnd 14044	A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. Mnd )
Theorem	srgmgp 14045	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 14046	Lemma for srgdi 14051 and srgdir 14052. (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 14047	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 14048	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 14049*	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 14050	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 14051	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 14052	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 14053	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 14054	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 14055	Lemma for srglidm 14056 and srgridm 14057. (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 14056	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 14057	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 14058*	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 14059	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 14060	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 14061	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 14062	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 14063*	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 14064	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 14065	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 14066	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 14067	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 14068	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 14069	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 14070*	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 14071*	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 14072	The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 13799. (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 14073	Extend class notation with class of all (unital) rings.
class Ring
Syntax	ccrg 14074	Extend class notation with class of all (unital) commutative rings.
class CRing
Definition	df-ring 14075*	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 14108), 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 14076	Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
Theorem	isring 14077*	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 14078	A ring is a group. (Contributed by NM, 15-Sep-2011.)
|- ( R e. Ring -> R e. Grp )
Theorem	ringmgp 14079	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 14080	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 14081	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 14082	A ring is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. Ring )   =>    |- ( ph -> R e. Grp )
Theorem	ringmnd 14083	A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. Mnd )
Theorem	ringmgm 14084	A ring is a magma. (Contributed by AV, 31-Jan-2020.)
|- ( R e. Ring -> R e. Mgm )
Theorem	crngring 14085	A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. CRing -> R e. Ring )
Theorem	crngringd 14086	A commutative ring is a ring. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. CRing )   =>    |- ( ph -> R e. Ring )
Theorem	crnggrpd 14087	A commutative ring is a group. (Contributed by SN, 16-May-2024.)
|- ( ph -> R e. CRing )   =>    |- ( ph -> R e. Grp )
Theorem	mgpf 14088	Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- (mulGrp |` Ring ) : Ring --> Mnd
Theorem	ringdilem 14089	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 14090	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 14091	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 14092*	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 14093	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 14094*	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 14095	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 14096	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 14097	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 14098	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 14099	Lemma for ringlidm 14100 and ringridm 14101. (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 ) )
Theorem	ringlidm 14100	The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .1. .x. X ) = X )