P. 187 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18601-18700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulgass2 18601	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 18602	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 18603	Rings exist. (Contributed by AV, 29-Apr-2019.)
|- Ring =/= (/)
Theorem	ringlghm 18604*	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	ringrghm 18605*	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 18606*	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 18607*	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	gsummgp0 18608*	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	gsumdixp 18609*	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 18610	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 18611	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	prdsringd 18612	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 18613	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 18614	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	pwsring 18615	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 18616	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 18617	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 18618	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	imasring 18619*	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	qusring2 18620*	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 18621*	The binomial theorem for commutative rings (special case of csrgbinom 18546): ( 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 18622	The opposite ring operation.
class oppr
Definition	df-oppr 18623	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 18624	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 18625	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 18626	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 18627	In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 18697). (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 18628	Lemma for opprbas 18629 and oppradd 18630. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N < 3   =>    |- ( E ` R ) = ( E ` O )
Theorem	opprbas 18629	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- B = ( Base ` R )   =>    |- B = ( Base ` O )
Theorem	oppradd 18630	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .+ = ( +g ` R )   =>    |- .+ = ( +g ` O )
Theorem	opprring 18631	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	opprringb 18632	Bidirectional form of opprring 18631. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- ( R e. Ring <-> O e. Ring )
Theorem	oppr0 18633	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .0. = ( 0g ` R )   =>    |- .0. = ( 0g ` O )
Theorem	oppr1 18634	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .1. = ( 1r ` R )   =>    |- .1. = ( 1r ` O )
Theorem	opprneg 18635	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 18636	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- (SubGrp ` R ) = (SubGrp ` O )
Theorem	mulgass3 18637	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 18638	Ring divisibility relation.
class ||r
Syntax	cui 18639	Ring unit.
class Unit
Syntax	cir 18640	Ring irreducibles.
class Irred
Definition	df-dvdsr 18641*	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 18642	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 18643*	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 18644	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- .|| = ( ||r ` R )   =>    |- Rel .||
Theorem	dvdsrval 18645*	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 18646*	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 18647*	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 18648	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 18649	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( X .|| Y -> X e. B )
Theorem	dvdsrcl2 18650	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 18651	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 18652	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 18653	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 18654	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 18655	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 19283.) (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 18656	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 18657	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 18658	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 18659	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 18660	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 18661	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 18662	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 18663	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 18664	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 18665	Reversal of unitmulcl 18664 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 18666	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 18667	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 18668	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 18669	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 18670	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 18671	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 18672	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
Theorem	invrfval 18673	Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   &    |- I = ( invr ` R )   =>    |- I = ( invg ` G )
Theorem	unitinvcl 18674	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 18675	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 18676	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 18677	A unit times its inverse is the identity. (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. )
Theorem	unitrinv 18678	A unit times its inverse is the identity. (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 ) -> ( X .x. ( I ` X ) ) = .1. )
Theorem	1rinv 18679	The inverse of the identity is the identity. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- I = ( invr ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( I ` .1. ) = .1. )
Theorem	0unit 18680	The additive identity is a unit if and only if 1 = 0, i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( .0. e. U <-> .1. = .0. ) )
Theorem	unitnegcl 18681	The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- N = ( invg ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. U )
Syntax	cdvr 18682	Extend class notation with ring division.
class /r
Definition	df-dvr 18683*	Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
Theorem	dvrfval 18684*	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- ./ = (/r ` R )   =>    |- ./ = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) )
Theorem	dvrval 18685	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( I ` Y ) ) )
Theorem	dvrcl 18686	Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) e. B )
Theorem	unitdvcl 18687	The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ./ Y ) e. U )
Theorem	dvrid 18688	A cancellation law for division. (divid 10714 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( X ./ X ) = .1. )
Theorem	dvr1 18689	A cancellation law for division. (div1 10716 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )
Theorem	dvrass 18690	An associative law for division. (divass 10703 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .x. Y ) ./ Z ) = ( X .x. ( Y ./ Z ) ) )
Theorem	dvrcan1 18691	A cancellation law for division. (divcan1 10694 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = X )
Theorem	dvrcan3 18692	A cancellation law for division. (divcan3 10711 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. Y ) ./ Y ) = X )
Theorem	dvreq1 18693	A cancellation law for division. (diveq1 10718 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) = .1. <-> X = Y ) )
Theorem	ringinvdv 18694	Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) = ( .1. ./ X ) )
Theorem	rngidpropd 18695*	The ring identity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( 1r ` K ) = ( 1r ` L ) )
Theorem	dvdsrpropd 18696*	The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( ||r ` K ) = ( ||r ` L ) )
Theorem	unitpropd 18697*	The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> (Unit ` K ) = (Unit ` L ) )
Theorem	invrpropd 18698*	The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( invr ` K ) = ( invr ` L ) )
Theorem	isirred 18699*	An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = (Irred ` R )   &    |- N = ( B \ U )   &    |- .x. = ( .r ` R )   =>    |- ( X e. I <-> ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) )
Theorem	isnirred 18700*	The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = (Irred ` R )   &    |- N = ( B \ U )   &    |- .x. = ( .r ` R )   =>    |- ( X e. B -> ( -. X e. I <-> ( X e. U \/ E. x e. N E. y e. N ( x .x. y ) = X ) ) )