P. 171 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscrng2 17001*	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	rngass 17002	Associative law for the multiplication operation of 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	rngideu 17003*	The unit 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	rngdi 17004	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	rngdir 17005	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	rngidcl 17006	The unit 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	rng0cl 17007	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	rngidmlem 17008	Lemma for rnglidm 17009 and rngridm 17010. (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	rnglidm 17009	The unit 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	rngridm 17010	The unit 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	isrngid 17011*	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	rngidss 17012	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	rngacl 17013	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	rngcom 17014	Commutativity of the additive group of a ring. (See also lmodcom 17339.) (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	rngabl 17015	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|- ( R e. Ring -> R e. Abel )
Theorem	rngcmn 17016	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. CMnd )
Theorem	rngpropd 17017*	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 17018*	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	rngprop 17019	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	isrngd 17020*	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 17021*	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	rnglz 17022	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	rngrz 17023	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	rngsrg 17024	Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.)
|- ( R e. Ring -> R e. SRing )
Theorem	rng1eq0 17025	If one and zero are equal, then any two elements of a ring are equal. Alternatively, 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	rngnegl 17026	Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 29955 analog.) (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	rngnegr 17027	Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 29956 analog.) (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	rngmneg1 17028	Negation of a product in a ring. (mulneg1 9989 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	rngmneg2 17029	Negation of a product in a ring. (mulneg2 9990 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	rngm2neg 17030	Double negation of a product in a ring. (mul2neg 9992 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	rngsubdi 17031	Ring multiplication distributes over subtraction. (subdi 9986 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	rngsubdir 17032	Ring multiplication distributes over subtraction. (subdir 9987 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 17033	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	rnglghm 17034*	Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( x e. B |-> ( X .x. x ) ) e. ( R GrpHom R ) )
Theorem	rngrghm 17035*	Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) e. ( R GrpHom R ) )
Theorem	gsummulc1 17036*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   =>    |- ( ph -> ( R gsumg ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsumg ( k e. A |-> X ) ) .x. Y ) )
Theorem	gsummulc2 17037*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( k e. A |-> X ) finSupp .0. )   =>    |- ( ph -> ( R gsumg ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsumg ( k e. A |-> X ) ) ) )
Theorem	gsummulc1OLD 17038*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) Obsolete version of gsummulc1 17036 as of 10-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( `' ( k e. A |-> X ) " ( _V \ { .0. } ) ) e. Fin )   =>    |- ( ph -> ( R gsumg ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsumg ( k e. A |-> X ) ) .x. Y ) )
Theorem	gsummulc2OLD 17039*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) Obsolete version of gsummulc1 17036 as of 10-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( `' ( k e. A |-> X ) " ( _V \ { .0. } ) ) e. Fin )   =>    |- ( ph -> ( R gsumg ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsumg ( k e. A |-> X ) ) ) )
Theorem	gsummgp0 17040*	If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019.)
|- G = (mulGrp ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ n e. N ) -> A e. ( Base ` R ) )   &    |- ( ( ph /\ n = i ) -> A = B )   &    |- ( ph -> E. i e. N B = .0. )   =>    |- ( ph -> ( G gsumg ( n e. N |-> A ) ) = .0. )
Theorem	gsumdixpOLD 17041*	Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) Obsolete version of gsumdixp 17042 as of 10-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> I e. V )   &    |- ( ph -> J e. W )   &    |- ( ph -> R e. Ring )   &    |- ( ( ph /\ x e. I ) -> X e. B )   &    |- ( ( ph /\ y e. J ) -> Y e. B )   &    |- ( ph -> ( `' ( x e. I |-> X ) " ( _V \ { .0. } ) ) e. Fin )   &    |- ( ph -> ( `' ( y e. J |-> Y ) " ( _V \ { .0. } ) ) e. Fin )   =>    |- ( ph -> ( ( R gsumg ( x e. I |-> X ) ) .x. ( R gsumg ( y e. J |-> Y ) ) ) = ( R gsumg ( x e. I , y e. J |-> ( X .x. Y ) ) ) )
Theorem	gsumdixp 17042*	Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> I e. V )   &    |- ( ph -> J e. W )   &    |- ( ph -> R e. Ring )   &    |- ( ( ph /\ x e. I ) -> X e. B )   &    |- ( ( ph /\ y e. J ) -> Y e. B )   &    |- ( ph -> ( x e. I |-> X ) finSupp .0. )   &    |- ( ph -> ( y e. J |-> Y ) finSupp .0. )   =>    |- ( ph -> ( ( R gsumg ( x e. I |-> X ) ) .x. ( R gsumg ( y e. J |-> Y ) ) ) = ( R gsumg ( x e. I , y e. J |-> ( X .x. Y ) ) ) )
Theorem	prdsmgp 17043	The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- M = (mulGrp ` Y )   &    |- Z = ( S X_s (mulGrp o. R ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> S e. W )   &    |- ( ph -> R Fn I )   =>    |- ( ph -> ( ( Base ` M ) = ( Base ` Z ) /\ ( +g ` M ) = ( +g ` Z ) ) )
Theorem	prdsmulrcl 17044	A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .x. G ) e. B )
Theorem	prdsrngd 17045	A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Ring )   =>    |- ( ph -> Y e. Ring )
Theorem	prdscrngd 17046	A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> CRing )   =>    |- ( ph -> Y e. CRing )
Theorem	prds1 17047	Value of the ring unit in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Ring )   =>    |- ( ph -> ( 1r o. R ) = ( 1r ` Y ) )
Theorem	pwsrng 17048	A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Ring /\ I e. V ) -> Y e. Ring )
Theorem	pws1 17049	Value of the ring unit in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( R ^s I )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ I e. V ) -> ( I X. { .1. } ) = ( 1r ` Y ) )
Theorem	pwscrng 17050	A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. CRing /\ I e. V ) -> Y e. CRing )
Theorem	pwsmgp 17051	The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- Y = ( R ^s I )   &    |- M = (mulGrp ` R )   &    |- Z = ( M ^s I )   &    |- N = (mulGrp ` Y )   &    |- B = ( Base ` N )   &    |- C = ( Base ` Z )   &    |- .+ = ( +g ` N )   &    |- .+b = ( +g ` Z )   =>    |- ( ( R e. V /\ I e. W ) -> ( B = C /\ .+ = .+b ) )
Theorem	imasrng 17052*	The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` 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. Ring )   =>    |- ( ph -> ( U e. Ring /\ ( F ` .1. ) = ( 1r ` U ) ) )
Theorem	divsrng2 17053*	The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` 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. Ring )   =>    |- ( ph -> ( U e. Ring /\ [ .1. ] .~ = ( 1r ` U ) ) )
Theorem	crngbinom 17054*	The binomial theorem for commutative rings (special case of csrgbinom 16985): ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ). (Contributed by AV, 24-Aug-2019.)
|- S = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .x. = (.g ` R )   &    |- .+ = ( +g ` R )   &    |- G = (mulGrp ` R )   &    |- .^ = (.g ` G )   =>    |- ( ( ( R e. CRing /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( N .^ ( A .+ B ) ) = ( R gsumg ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
10.4.4  Opposite ring
Syntax	coppr 17055	The opposite ring operation.
class oppr
Definition	df-oppr 17056	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	opprval 17057	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   =>    |- O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )
Theorem	opprmulfval 17058	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 )   =>    |- .xb = tpos .x.
Theorem	opprmul 17059	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 )   =>    |- ( X .xb Y ) = ( Y .x. X )
Theorem	crngoppr 17060	In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 17130). (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	opprlem 17061	Lemma for opprbas 17062 and oppradd 17063. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N < 3   =>    |- ( E ` R ) = ( E ` O )
Theorem	opprbas 17062	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- B = ( Base ` R )   =>    |- B = ( Base ` O )
Theorem	oppradd 17063	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .+ = ( +g ` R )   =>    |- .+ = ( +g ` O )
Theorem	opprrng 17064	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	opprrngb 17065	Bidirectional form of opprrng 17064. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- ( R e. Ring <-> O e. Ring )
Theorem	oppr0 17066	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .0. = ( 0g ` R )   =>    |- .0. = ( 0g ` O )
Theorem	oppr1 17067	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .1. = ( 1r ` R )   =>    |- .1. = ( 1r ` O )
Theorem	opprneg 17068	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 )   =>    |- N = ( invg ` O )
Theorem	opprsubg 17069	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- (SubGrp ` R ) = (SubGrp ` O )
Theorem	mulgass3 17070	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 ) ) )
10.4.5  Divisibility
Syntax	cdsr 17071	Ring divides relation.
class ||r
Syntax	cui 17072	Ring unit.
class Unit
Syntax	cir 17073	Ring irreducibles.
class Irred
Definition	df-dvdsr 17074*	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 17075	Define the set of units in a ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
Definition	df-irred 17076*	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	reldvdsr 17077	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- .|| = ( ||r ` R )   =>    |- Rel .||
Theorem	dvdsrval 17078*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) }
Theorem	dvdsr 17079*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) )
Theorem	dvdsr2 17080*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( X e. B -> ( X .|| Y <-> E. z e. B ( z .x. X ) = Y ) )
Theorem	dvdsrmul 17081	A left-multiple of X is divisible by X. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( X e. B /\ Y e. B ) -> X .|| ( Y .x. X ) )
Theorem	dvdsrcl 17082	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( X .|| Y -> X e. B )
Theorem	dvdsrcl2 17083	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 17084	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 17085	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 17086	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 17087	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 17088	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 17702.) (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 17089	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	isunit 17090	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.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   &    |- .|| = ( ||r ` R )   &    |- S = (oppr ` R )   &    |- E = ( ||r ` S )   =>    |- ( X e. U <-> ( X .|| .1. /\ X E .1. ) )
Theorem	1unit 17091	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	unitcl 17092	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   =>    |- ( X e. U -> X e. B )
Theorem	unitss 17093	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   =>    |- U C_ B
Theorem	opprunit 17094	Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- S = (oppr ` R )   =>    |- U = (Unit ` S )
Theorem	crngunit 17095	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 17096	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 17097	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 17098	Reversal of unitmulcl 17097 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	unitgrpbas 17099	The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- U = ( Base ` G )
Theorem	unitgrp 17100	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 )