P. 338 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33701-33800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngoid 33701*	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.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X ) -> E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) )
Theorem	rngoideu 33702*	The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> E! u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) )
Theorem	rngodi 33703	Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H ( B G C ) ) = ( ( A H B ) G ( A H C ) ) )
Theorem	rngodir 33704	Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) H C ) = ( ( A H C ) G ( B H C ) ) )
Theorem	rngoass 33705	Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( A H ( B H C ) ) )
Theorem	rngo2 33706*	A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X ) -> E. x e. X ( A G A ) = ( ( x G x ) H A ) )
Theorem	rngoablo 33707	A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   =>    |- ( R e. RingOps -> G e. AbelOp )
Theorem	rngoablo2 33708	In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
|- ( <. G , H >. e. RingOps -> G e. AbelOp )
Theorem	rngogrpo 33709	A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   =>    |- ( R e. RingOps -> G e. GrpOp )
Theorem	rngone0 33710	The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> X =/= (/) )
Theorem	rngogcl 33711	Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
Theorem	rngocom 33712	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
Theorem	rngoaass 33713	The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )
Theorem	rngoa32 33714	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
Theorem	rngoa4 33715	Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )
Theorem	rngorcan 33716	Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )
Theorem	rngolcan 33717	Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )
Theorem	rngo0cl 33718	A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. RingOps -> Z e. X )
Theorem	rngo0rid 33719	The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( A G Z ) = A )
Theorem	rngo0lid 33720	The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( Z G A ) = A )
Theorem	rngolz 33721	The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
|- Z = (GId ` G )   &    |- X = ran G   &    |- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( Z H A ) = Z )
Theorem	rngorz 33722	The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
|- Z = (GId ` G )   &    |- X = ran G   &    |- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( A H Z ) = Z )
Theorem	rngosn3 33723	Obsolete as of 25-Jan-2020. Use ring1zr 19275 or srg1zr 18529 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. B ) -> ( X = { A } <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )
Theorem	rngosn4 33724	Obsolete as of 25-Jan-2020. Use rngen1zr 19276 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( X ~~ 1o <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )
Theorem	rngosn6 33725	Obsolete as of 25-Jan-2020. Use ringen1zr 19277 or srgen1zr 18530 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. RingOps -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )
Theorem	rngonegcl 33726	A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) e. X )
Theorem	rngoaddneg1 33727	Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   &    |- Z = (GId ` G )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( A G ( N ` A ) ) = Z )
Theorem	rngoaddneg2 33728	Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   &    |- Z = (GId ` G )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( ( N ` A ) G A ) = Z )
Theorem	rngosub 33729	Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   &    |- D = ( /g ` G )   =>    |- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( N ` B ) ) )
Theorem	rngmgmbs4 33730*	The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- ( ( G : ( X X. X ) --> X /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) -> ran G = X )
Theorem	rngodm1dm2 33731	In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- G = ( 1st ` R )   =>    |- ( R e. RingOps -> dom dom G = dom dom H )
Theorem	rngorn1 33732	In a unital ring the range of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- G = ( 1st ` R )   =>    |- ( R e. RingOps -> ran G = dom dom H )
Theorem	rngorn1eq 33733	In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- G = ( 1st ` R )   =>    |- ( R e. RingOps -> ran G = ran H )
Theorem	rngomndo 33734	In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- H = ( 2nd ` R )   =>    |- ( R e. RingOps -> H e. MndOp )
Theorem	rngoidmlem 33735	The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- X = ran ( 1st ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) = A /\ ( A H U ) = A ) )
Theorem	rngolidm 33736	The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- X = ran ( 1st ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( U H A ) = A )
Theorem	rngoridm 33737	The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- X = ran ( 1st ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( A H U ) = A )
Theorem	rngo1cl 33738	The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.)
|- X = ran ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- U = (GId ` H )   =>    |- ( R e. RingOps -> U e. X )
Theorem	rngoueqz 33739	Obsolete as of 23-Jan-2020. Use 0ring01eqbi 19273 instead. In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( X ~~ 1o <-> U = Z ) )
Theorem	rngonegmn1l 33740	Negation in a ring is the same as left multiplication by -u 1. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( ( N ` U ) H A ) )
Theorem	rngonegmn1r 33741	Negation in a ring is the same as right multiplication by -u 1. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( A H ( N ` U ) ) )
Theorem	rngoneglmul 33742	Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   =>    |- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( ( N ` A ) H B ) )
Theorem	rngonegrmul 33743	Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- N = ( inv ` G )   =>    |- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( A H ( N ` B ) ) )
Theorem	rngosubdi 33744	Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H ( B D C ) ) = ( ( A H B ) D ( A H C ) ) )
Theorem	rngosubdir 33745	Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) H C ) = ( ( A H C ) D ( B H C ) ) )
Theorem	zerdivemp1x 33746*	In a unitary ring a left invertible element is not a zero divisor. See also ringinvnzdiv 18593. (Contributed by Jeff Madsen, 18-Apr-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X /\ E. a e. X ( a H A ) = U ) -> ( B e. X -> ( ( A H B ) = Z -> B = Z ) ) )
20.19.17  Division Rings
Syntax	cdrng 33747	Extend class notation with the class of all division rings.
class DivRingOps
Definition	df-drngo 33748*	Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
|- DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) ) e. GrpOp ) }
Theorem	isdivrngo 33749	The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
|- ( H e. A -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { (GId ` G ) } ) X. ( ran G \ { (GId ` G ) } ) ) ) e. GrpOp ) ) )
Theorem	drngoi 33750	The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. DivRingOps -> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
Theorem	gidsn 33751	Obsolete as of 23-Jan-2020. Use mnd1id 17332 instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- A e. _V   =>    |- (GId ` { <. <. A , A >. , A >. } ) = A
Theorem	zrdivrng 33752	The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- A e. _V   =>    |- -. <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps
Theorem	dvrunz 33753	In a division ring the unit is different from the zero. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( R e. DivRingOps -> U =/= Z )
Theorem	isgrpda 33754*	Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.)
|- ( ph -> X e. _V )   &    |- ( ph -> G : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ x e. X ) -> ( U G x ) = x )   &    |- ( ( ph /\ x e. X ) -> E. n e. X ( n G x ) = U )   =>    |- ( ph -> G e. GrpOp )
Theorem	isdrngo1 33755	The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   =>    |- ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
Theorem	divrngcl 33756	The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   =>    |- ( ( R e. DivRingOps /\ A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) -> ( A H B ) e. ( X \ { Z } ) )
Theorem	isdrngo2 33757*	A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   &    |- U = (GId ` H )   =>    |- ( R e. DivRingOps <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = U ) ) )
Theorem	isdrngo3 33758*	A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   &    |- U = (GId ` H )   =>    |- ( R e. DivRingOps <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
20.19.18  Ring homomorphisms
Syntax	crnghom 33759	Extend class notation with the class of ring homomorphisms.
class RngHom
Syntax	crngiso 33760	Extend class notation with the class of ring isomorphisms.
class RngIso
Syntax	crisc 33761	Extend class notation with the ring isomorphism relation.
class ~=R
Definition	df-rngohom 33762*	Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- RngHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` (GId ` ( 2nd ` r ) ) ) = (GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } )
Theorem	rngohomval 33763*	The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- U = (GId ` H )   &    |- J = ( 1st ` S )   &    |- K = ( 2nd ` S )   &    |- Y = ran J   &    |- V = (GId ` K )   =>    |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngHom S ) = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } )
Theorem	isrngohom 33764*	The predicate "is a ring homomorphism from R to S." (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- U = (GId ` H )   &    |- J = ( 1st ` S )   &    |- K = ( 2nd ` S )   &    |- Y = ran J   &    |- V = (GId ` K )   =>    |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngHom S ) <-> ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )
Theorem	rngohomf 33765	A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   &    |- Y = ran J   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F : X --> Y )
Theorem	rngohomcl 33766	Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   &    |- Y = ran J   =>    |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ A e. X ) -> ( F ` A ) e. Y )
Theorem	rngohom1 33767	A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.)
|- H = ( 2nd ` R )   &    |- U = (GId ` H )   &    |- K = ( 2nd ` S )   &    |- V = (GId ` K )   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F ` U ) = V )
Theorem	rngohomadd 33768	Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   =>    |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) )
Theorem	rngohommul 33769	Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- H = ( 2nd ` R )   &    |- K = ( 2nd ` S )   =>    |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )
Theorem	rngogrphom 33770	A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.)
|- G = ( 1st ` R )   &    |- J = ( 1st ` S )   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F e. ( G GrpOpHom J ) )
Theorem	rngohom0 33771	A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.)
|- G = ( 1st ` R )   &    |- Z = (GId ` G )   &    |- J = ( 1st ` S )   &    |- W = (GId ` J )   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F ` Z ) = W )
Theorem	rngohomsub 33772	Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- H = ( /g ` G )   &    |- J = ( 1st ` S )   &    |- K = ( /g ` J )   =>    |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )
Theorem	rngohomco 33773	The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RngHom S ) /\ G e. ( S RngHom T ) ) ) -> ( G o. F ) e. ( R RngHom T ) )
Theorem	rngokerinj 33774	A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- W = (GId ` G )   &    |- J = ( 1st ` S )   &    |- Y = ran J   &    |- Z = (GId ` J )   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) )
Definition	df-rngoiso 33775*	Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )
Theorem	rngoisoval 33776*	The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   &    |- Y = ran J   =>    |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngIso S ) = { f e. ( R RngHom S ) | f : X -1-1-onto-> Y } )
Theorem	isrngoiso 33777	The predicate "is a ring isomorphism between R and S." (Contributed by Jeff Madsen, 16-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   &    |- Y = ran J   =>    |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ F : X -1-1-onto-> Y ) ) )
Theorem	rngoiso1o 33778	A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   &    |- Y = ran J   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> F : X -1-1-onto-> Y )
Theorem	rngoisohom 33779	A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> F e. ( R RngHom S ) )
Theorem	rngoisocnv 33780	The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> `' F e. ( S RngIso R ) )
Theorem	rngoisoco 33781	The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RngIso S ) /\ G e. ( S RngIso T ) ) ) -> ( G o. F ) e. ( R RngIso T ) )
Definition	df-risc 33782*	Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }
Theorem	isriscg 33783*	The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( R e. A /\ S e. B ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) ) )
Theorem	isrisc 33784*	The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- R e. _V   &    |- S e. _V   =>    |- ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) )
Theorem	risc 33785*	The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RngIso S ) ) )
Theorem	risci 33786	Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> R ~=R S )
Theorem	riscer 33787	Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ~=R Er dom ~=R
20.19.19  Commutative rings
Syntax	ccm2 33788	Extend class notation with a class that adds commutativity to various flavors of rings.
class Com2
Definition	df-com2 33789*	A device to add commutativity to various sorts of rings. I use ran g because I suppose g has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
|- Com2 = { <. g , h >. | A. a e. ran g A. b e. ran g ( a h b ) = ( b h a ) }
Syntax	cfld 33790	Extend class notation with the class of all fields.
class Fld
Definition	df-fld 33791	Definition of a field. A field is a commutative division ring. (Contributed by FL, 6-Sep-2009.) (Revised by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)
|- Fld = ( DivRingOps i^i Com2 )
Syntax	ccring 33792	Extend class notation with the class of commutative rings.
class CRingOps
Definition	df-crngo 33793	Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.)
|- CRingOps = ( RingOps i^i Com2 )
Theorem	iscom2 33794*	A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
|- ( ( G e. A /\ H e. B ) -> ( <. G , H >. e. Com2 <-> A. a e. ran G A. b e. ran G ( a H b ) = ( b H a ) ) )
Theorem	iscrngo 33795	The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
|- ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )
Theorem	iscrngo2 33796*	The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. CRingOps <-> ( R e. RingOps /\ A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )
Theorem	iscringd 33797*	Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- ( ph -> G e. AbelOp )   &    |- ( ph -> X = ran G )   &    |- ( ph -> H : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ y e. X ) -> ( y H U ) = y )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x H y ) = ( y H x ) )   =>    |- ( ph -> <. G , H >. e. CRingOps )
Theorem	flddivrng 33798	A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- ( K e. Fld -> K e. DivRingOps )
Theorem	crngorngo 33799	A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. CRingOps -> R e. RingOps )
Theorem	crngocom 33800	The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. CRingOps /\ A e. X /\ B e. X ) -> ( A H B ) = ( B H A ) )