P. 154 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngi 15301	Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
Theorem	rngcl 15302	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 15303	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 15304*	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 15305	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 15306*	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 15307	Distributive law for the multiplication operation of a ring. (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 15308	Distributive law for the multiplication operation of a ring. (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 15309	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 15310	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 15311	Lemma for rnglidm 15312 and rngridm 15313. (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 15312	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 15313	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 15314*	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 15315	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 15316	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 15317	Commutativity of the additive group of a ring. (See also lmodcom 15619.) (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 15318	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|- ( R e. Ring -> R e. Abel )
Theorem	rngcmn 15319	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. CMnd )
Theorem	rngpropd 15320*	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 15321*	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 15322	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 15323*	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 15324*	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 15325	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 15326	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	rng1eq0 15327	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 15328	Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 25933 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 = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( N ` .1. ) .x. X ) = ( N ` X ) )
Theorem	rngnegr 15329	Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 25934 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 = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .x. ( N ` .1. ) ) = ( N ` X ) )
Theorem	rngmneg1 15330	Negation of a product in a ring. (mulneg1 9170 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. Y ) = ( N ` ( X .x. Y ) ) )
Theorem	rngmneg2 15331	Negation of a product in a ring. (mulneg2 9171 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) )
Theorem	rngm2neg 15332	Double negation of a product in a ring. (mul2neg 9173 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )
Theorem	rngsubdi 15333	Ring multiplication distributes over subtraction. (subdi 9167 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 15334	Ring multiplication distributes over subtraction. (subdir 9168 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 15335	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 15336*	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 15337*	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 15338*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- 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	gsummulc2 15339*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- 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	gsumdixp 15340*	Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.)
|- 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	prdsmgp 15341	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 15342	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 15343	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 15344	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 15345	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 15346	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 15347	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 15348	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 15349	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 15350*	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 15351*	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 ) ) )
10.4.3  Opposite ring
Syntax	coppr 15352	The opposite ring operation.
class oppr
Definition	df-oppr 15353	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 15354	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 15355	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 15356	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 15357	In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 15427). (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 15358	Lemma for opprbas 15359 and oppradd 15360. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N < 3   =>    |- ( E ` R ) = ( E ` O )
Theorem	opprbas 15359	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- B = ( Base ` R )   =>    |- B = ( Base ` O )
Theorem	oppradd 15360	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .+ = ( +g ` R )   =>    |- .+ = ( +g ` O )
Theorem	opprrng 15361	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 15362	Bidirectional form of opprrng 15361. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- ( R e. Ring <-> O e. Ring )
Theorem	oppr0 15363	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .0. = ( 0g ` R )   =>    |- .0. = ( 0g ` O )
Theorem	oppr1 15364	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .1. = ( 1r ` R )   =>    |- .1. = ( 1r ` O )
Theorem	opprneg 15365	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 = ( inv g ` R )   =>    |- N = ( inv g ` O )
Theorem	opprsubg 15366	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- (SubGrp ` R ) = (SubGrp ` O )
Theorem	mulgass3 15367	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.4  Divisibility
Syntax	cdsr 15368	Ring divides relation.
class ||r
Syntax	cui 15369	Ring unit.
class Unit
Syntax	cir 15370	Ring irreducibles.
class Irred
Definition	df-dvdsr 15371*	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 15372	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 15373*	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 15374	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- .|| = ( ||r ` R )   =>    |- Rel .||
Theorem	dvdsrval 15375*	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 15376*	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 15377*	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 15378	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 15379	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( X .|| Y -> X e. B )
Theorem	dvdsrcl2 15380	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 15381	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 15382	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 15383	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 15384	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- N = ( inv g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| ( N ` X ) )
Theorem	dvdsr01 15385	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 15972.) (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 15386	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 15387	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 15388	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 15389	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 15390	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 15391	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 15392	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 15393	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 15394	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 15395	Reversal of unitmulcl 15394 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 15396	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 15397	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 15398	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 15399	The identity of the multiplicative group is 1r. (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 15400	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 ) )