P. 143 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14201-14300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpsval 14201*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )   &    |- G = (Scalar ` R )   &    |- U = ( G X_s { <. (/) , R >. , <. 1o , S >. } )   =>    |- ( ph -> T = ( `' F "s U ) )
7.2.9  Structure power
Syntax	cpws 14202	The function constructing structure powers.
class ^s
Definition	df-pws 14203*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
Theorem	pwsval 14204	Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- F = (Scalar ` R )   =>    |- ( ( R e. V /\ I e. W ) -> Y = ( F X_s ( I X. { R } ) ) )
Theorem	pwsbas 14205	Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   =>    |- ( ( R e. V /\ I e. W ) -> ( B ^m I ) = ( Base ` Y ) )
Theorem	pwselbasb 14206	Membership in the base set of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- V = ( Base ` Y )   =>    |- ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )
Theorem	pwselbas 14207	An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- V = ( Base ` Y )   &    |- ( ph -> R e. W )   &    |- ( ph -> I e. Z )   &    |- ( ph -> X e. V )   =>    |- ( ph -> X : I --> B )
Theorem	pwsplusgval 14208	Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` Y )   =>    |- ( ph -> ( F .+b G ) = ( F oF .+ G ) )
Theorem	pwsmulrval 14209	Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` Y )   =>    |- ( ph -> ( F .xb G ) = ( F oF .x. G ) )
Theorem	pwsdiagel 14210	Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- C = ( Base ` Y )   =>    |- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( I X. { A } ) e. C )
Theorem	pwssnf1o 14211*	Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s { I } )   &    |- B = ( Base ` R )   &    |- F = ( x e. B |-> ( { I } X. { x } ) )   &    |- C = ( Base ` Y )   =>    |- ( ( R e. V /\ I e. W ) -> F : B -1-1-onto-> C )
Theorem	pwsmnd 14212	The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Mnd /\ I e. V ) -> Y e. Mnd )
Theorem	pws0g 14213	The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g ` Y ) )
Theorem	pwsgrp 14214	A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Grp /\ I e. V ) -> Y e. Grp )
Theorem	pwsinvg 14215	Negation in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- M = ( invg ` R )   &    |- N = ( invg ` Y )   =>    |- ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( N ` X ) = ( M o. X ) )
Theorem	pwssub 14216	Subtraction in a structure power. (Contributed by Mario Carneiro, 12-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- M = ( -g ` R )   &    |- .- = ( -g ` Y )   =>    |- ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F oF M G ) )
7.3  Rings
7.3.1  Multiplicative Group
Syntax	cmgp 14217	Multiplicative group.
class mulGrp
Definition	df-mgp 14218	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 14263). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 14219	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V
Theorem	mgpvalg 14220	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 14221	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	mgpplusg 14222	Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- .x. = ( +g ` M )
Theorem	mgpex 14223	Existence of the multiplication group. If R is known to be a semiring, see srgmgp 14272. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- M = (mulGrp ` R )   =>    |- ( R e. V -> M e. _V )
Theorem	mgpbasg 14224	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	mgpbas 14225	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 )   =>    |- B = ( Base ` M )
Theorem	mgpscag 14226	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 14227	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 14228	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 14229	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 14230	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 14231	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng 14232*	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 14233*	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 14234	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 14235	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 14236	Restricted functionality of the multiplicative group on non-unital rings (mgpf 14315 analog). (Contributed by AV, 22-Feb-2025.)
|- (mulGrp |` Rng ) :Rng -->Smgrp
Theorem	rnggrp 14237	A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
|- ( R e. Rng -> R e. Grp )
Theorem	rngass 14238	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 14239	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 14240	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 14241	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 14242	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 14243	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 14244	The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 14348. (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 14245	The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 14349. (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 14246	Negation of a product in a non-unital ring (mulneg1 8722 analog). In contrast to ringmneg1 14358, 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 14247	Negation of a product in a non-unital ring (mulneg2 8723 analog). In contrast to ringmneg2 14359, 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 14248	Double negation of a product in a non-unital ring (mul2neg 8725 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 14360. (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 14249	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 14250	Ring multiplication distributes over subtraction. (subdi 8712 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 14361. (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 14251	Ring multiplication distributes over subtraction. (subdir 8713 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 14362. (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 14252*	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 14253	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 13425. (Contributed by Jim Kingdon, 5-May-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Rng -> ( G ↾s B ) e. Rng )
Theorem	rngpropd 14254*	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 14255*	The image structure of a non-unital ring is a non-unital ring (imasring 14369 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 14256	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 14257*	The quotient structure of a non-unital ring is a non-unital ring (qusring2 14371 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 )
Theorem	rng1zrlem 14258	Lemma for rng1zr 14259 and srg1zr 14291. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Mgm /\ (mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	rng1zr 14259	The only ring 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, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	rngen1zr 14260	The only ring 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, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	rngen1zr0 14261	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. .0. , .0. >. , .0. >. } /\ .* = { <. <. .0. , .0. >. , .0. >. } ) ) )
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 14302). 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 14302 in set.mm), and we have "the ring unity is a unit", see https://us.metamath.org/mpeuni/1unit.html 14302.
Syntax	cur 14262	Extend class notation with ring unity.
class 1r
Definition	df-ur 14263	Define the multiplicative identity, i.e., the monoid identity (df-0g 13612) of the multiplicative monoid (df-mgp 14218) 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 14266, 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 14264	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	ringidval 14265	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 )   =>    |- .1. = ( 0g ` G )
Theorem	dfur2g 14266*	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 14267	Extend class notation with the class of all semirings.
class SRing
Definition	df-srg 14268*	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 14269*	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 14270	A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. CMnd )
Theorem	srgmnd 14271	A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- ( R e. SRing -> R e. Mnd )
Theorem	srgmgp 14272	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 14273	Lemma for srgdi 14278 and srgdir 14279. (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 14274	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 14275	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 14276*	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 14277	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 14278	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 14279	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 14280	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 14281	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 14282	Lemma for srglidm 14283 and srgridm 14284. (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 14283	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 14284	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 14285*	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 14286	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 14287	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 14288	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 14289	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 14290*	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 14291	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.) (Proof shortened by AV, 19-Jun-2026.)
|- 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	srgen1zr0 14292	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 14293	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 14294	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 14295	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 14296	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 14297*	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 14298*	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 14299	The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 13952. (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 14300	Extend class notation with class of all (unital) rings.
class Ring