P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ringcl 13201	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 13202	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 13203*	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 13204	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 13205*	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 13206	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 13207	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 13208	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 13209	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 13210	Lemma for ringlidm 13211 and ringridm 13212. (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 13211	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 )
Theorem	ringridm 13212	The unity element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X .x. .1. ) = X )
Theorem	isringid 13213*	Properties showing that an element I is the unity element of a ring. (Contributed by NM, 7-Aug-2013.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )
Theorem	ringid 13214*	The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> E. u e. B ( ( u .x. X ) = X /\ ( X .x. u ) = X ) )
Theorem	ringadd2 13215*	A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> E. x e. B ( X .+ X ) = ( ( x .+ x ) .x. X ) )
Theorem	ringo2times 13216	A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ A e. B ) -> ( A .+ A ) = ( ( .1. .+ .1. ) .x. A ) )
Theorem	ringidss 13217	A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- M = ( (mulGrp ` R ) ↾s A )   &    |- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> .1. = ( 0g ` M ) )
Theorem	ringacl 13218	Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	ringcom 13219	Commutativity of the additive group of a ring. (Contributed by Gérard Lang, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	ringabl 13220	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|- ( R e. Ring -> R e. Abel )
Theorem	ringcmn 13221	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. CMnd )
Theorem	ringpropd 13222*	If two structures have the same group components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( K e. Ring <-> L e. Ring ) )
Theorem	crngpropd 13223*	If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( K e. CRing <-> L e. CRing ) )
Theorem	ringprop 13224	If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   &    |- ( .r ` K ) = ( .r ` L )   =>    |- ( K e. Ring <-> L e. Ring )
Theorem	isringd 13225*	Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> R e. Grp )   &    |- ( ( 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 -> .1. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )   =>    |- ( ph -> R e. Ring )
Theorem	iscrngd 13226*	Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> R e. Grp )   &    |- ( ( 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 -> .1. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) = ( y .x. x ) )   =>    |- ( ph -> R e. CRing )
Theorem	ringlz 13227	The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .0. )
Theorem	ringrz 13228	The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
Theorem	ringsrg 13229	Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
|- ( R e. Ring -> R e. SRing )
Theorem	ring1eq0 13230	If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element { 0 }. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( .1. = .0. -> X = Y ) )
Theorem	ringinvnz1ne0 13231*	In a unital ring, a left invertible element is different from zero iff .1. =/= .0.. (Contributed by FL, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> E. a e. B ( a .x. X ) = .1. )   =>    |- ( ph -> ( X =/= .0. <-> .1. =/= .0. ) )
Theorem	ringinvnzdiv 13232*	In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010.) (Revised by Jeff Madsen, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> E. a e. B ( a .x. X ) = .1. )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )
Theorem	ringnegl 13233	Negation in a ring is the same as left multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( N ` .1. ) .x. X ) = ( N ` X ) )
Theorem	ringnegr 13234	Negation in a ring is the same as right multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .x. ( N ` .1. ) ) = ( N ` X ) )
Theorem	ringmneg1 13235	Negation of a product in a ring. (mulneg1 8354 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. Y ) = ( N ` ( X .x. Y ) ) )
Theorem	ringmneg2 13236	Negation of a product in a ring. (mulneg2 8355 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) )
Theorem	ringm2neg 13237	Double negation of a product in a ring. (mul2neg 8357 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( invg ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )
Theorem	ringsubdi 13238	Ring multiplication distributes over subtraction. (subdi 8344 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) )
Theorem	ringsubdir 13239	Ring multiplication distributes over subtraction. (subdir 8345 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )
Theorem	mulgass2 13240	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = (.g ` R )   &    |- .X. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( N .x. X ) .X. Y ) = ( N .x. ( X .X. Y ) ) )
Theorem	ring1 13241	The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }   =>    |- ( Z e. V -> M e. Ring )
Theorem	ringn0 13242	The class of rings is not empty (it is also inhabited, as shown at ring1 13241). (Contributed by AV, 29-Apr-2019.)
|- Ring =/= (/)
Theorem	ringressid 13243	A ring restricted to its base set is a ring. It will usually be the original ring exactly, of course, but to show that needs additional conditions such as those in strressid 12532. (Contributed by Jim Kingdon, 28-Feb-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Ring -> ( G ↾s B ) e. Ring )
7.3.5  Opposite ring
Syntax	coppr 13244	The opposite ring operation.
class oppr
Definition	df-oppr 13245	Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
Theorem	opprvalg 13246	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   =>    |- ( R e. V -> O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) )
Theorem	opprmulfvalg 13247	Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( .r ` O )   =>    |- ( R e. V -> .xb = tpos .x. )
Theorem	opprmulg 13248	Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( .r ` O )   =>    |- ( ( R e. V /\ X e. W /\ Y e. U ) -> ( X .xb Y ) = ( Y .x. X ) )
Theorem	crngoppr 13249	In a commutative ring, the opposite ring is equivalent to the original ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( .r ` O )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X .xb Y ) )
Theorem	opprex 13250	Existence of the opposite ring. If you know that R is a ring, see opprring 13254. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> O e. _V )
Theorem	opprsllem 13251	Lemma for opprbasg 13252 and oppraddg 13253. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|- O = (oppr ` R )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( E ` ndx ) =/= ( .r ` ndx )   =>    |- ( R e. V -> ( E ` R ) = ( E ` O ) )
Theorem	opprbasg 13252	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|- O = (oppr ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. V -> B = ( Base ` O ) )
Theorem	oppraddg 13253	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|- O = (oppr ` R )   &    |- .+ = ( +g ` R )   =>    |- ( R e. V -> .+ = ( +g ` O ) )
Theorem	opprring 13254	An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- O = (oppr ` R )   =>    |- ( R e. Ring -> O e. Ring )
Theorem	opprringbg 13255	Bidirectional form of opprring 13254. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. Ring <-> O e. Ring ) )
Theorem	oppr0g 13256	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. V -> .0. = ( 0g ` O ) )
Theorem	oppr1g 13257	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. V -> .1. = ( 1r ` O ) )
Theorem	opprnegg 13258	The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- O = (oppr ` R )   &    |- N = ( invg ` R )   =>    |- ( R e. V -> N = ( invg ` O ) )
Theorem	mulgass3 13259	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = (.g ` R )   &    |- .X. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .X. ( N .x. Y ) ) = ( N .x. ( X .X. Y ) ) )
7.3.6  Divisibility
Syntax	cdsr 13260	Ring divisibility relation.
class ||r
Syntax	cui 13261	Units in a ring.
class Unit
Syntax	cir 13262	Ring irreducibles.
class Irred
Definition	df-dvdsr 13263*	Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||r ` (oppr ` R ) ). (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
Definition	df-unit 13264	Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
Definition	df-irred 13265*	Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- Irred = ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )
Theorem	reldvdsrsrg 13266	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
|- ( R e. SRing -> Rel ( ||r ` R ) )
Theorem	dvdsrvald 13267*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   =>    |- ( ph -> .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } )
Theorem	dvdsrd 13268*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   =>    |- ( ph -> ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) ) )
Theorem	dvdsr2d 13269*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .|| Y <-> E. z e. B ( z .x. X ) = Y ) )
Theorem	dvdsrmuld 13270	A left-multiple of X is divisible by X. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> X .|| ( Y .x. X ) )
Theorem	dvdsrcld 13271	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> X .|| Y )   =>    |- ( ph -> X e. B )
Theorem	dvdsrex 13272	Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.)
|- ( R e. SRing -> ( ||r ` R ) e. _V )
Theorem	dvdsrcl2 13273	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ X .|| Y ) -> Y e. B )
Theorem	dvdsrid 13274	An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| X )
Theorem	dvdsrtr 13275	Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ Y .|| Z /\ Z .|| X ) -> Y .|| X )
Theorem	dvdsrmul1 13276	The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ Z e. B /\ X .|| Y ) -> ( X .x. Z ) .|| ( Y .x. Z ) )
Theorem	dvdsrneg 13277	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- N = ( invg ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| ( N ` X ) )
Theorem	dvdsr01 13278	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning.) (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| .0. )
Theorem	dvdsr02 13279	Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .0. .|| X <-> X = .0. ) )
Theorem	isunitd 13280	Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> .1. = ( 1r ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> S = (oppr ` R ) )   &    |- ( ph -> E = ( ||r ` S ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> ( X e. U <-> ( X .|| .1. /\ X E .1. ) ) )
Theorem	1unit 13281	The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. e. U )
Theorem	unitcld 13282	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> X e. U )   =>    |- ( ph -> X e. B )
Theorem	unitssd 13283	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> U C_ B )
Theorem	opprunitd 13284	Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> S = (oppr ` R ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> U = (Unit ` S ) )
Theorem	crngunit 13285	Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( R e. CRing -> ( X e. U <-> X .|| .1. ) )
Theorem	dvdsunit 13286	A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. CRing /\ Y .|| X /\ X e. U ) -> Y e. U )
Theorem	unitmulcl 13287	The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) e. U )
Theorem	unitmulclb 13288	Reversal of unitmulcl 13287 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U <-> ( X e. U /\ Y e. U ) ) )
Theorem	unitgrpbasd 13289	The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> G = ( (mulGrp ` R ) ↾s U ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> U = ( Base ` G ) )
Theorem	unitgrp 13290	The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( R e. Ring -> G e. Grp )
Theorem	unitabl 13291	The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( R e. CRing -> G e. Abel )
Theorem	unitgrpid 13292	The identity of the group of units of a ring is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. = ( 0g ` G ) )
Theorem	unitsubm 13293	The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = (Unit ` R )   &    |- M = (mulGrp ` R )   =>    |- ( R e. Ring -> U e. (SubMnd ` M ) )
Syntax	cinvr 13294	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 13295	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
Theorem	invrfvald 13296	Multiplicative inverse function for a ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> G = ( (mulGrp ` R ) ↾s U ) )   &    |- ( ph -> I = ( invr ` R ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> I = ( invg ` G ) )
Theorem	unitinvcl 13297	The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. U )
Theorem	unitinvinv 13298	The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` ( I ` X ) ) = X )
Theorem	ringinvcl 13299	The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. B )
Theorem	unitlinv 13300	A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) .x. X ) = .1. )