P. 323 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32201-32300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	crisc 32201	Extend class notation with the ring isomorphism relation.
class ~=R
Definition	df-rngohom 32202*	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 32203*	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 32204*	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 32205	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 32206	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 32207	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 32208	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 32209	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 32210	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 32211	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 32212	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 32213	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 32214	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 32215*	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 32216*	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 32217	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 32218	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 32219	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 32220	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 32221	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 32222*	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 32223*	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 32224*	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 32225*	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 32226	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 32227	Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ~=R Er dom ~=R
21.18.16  Commutative rings
Syntax	ccring 32228	Extend class notation with the class of commutative rings.
class CRingOps
Definition	df-crngo 32229	Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.)
|- CRingOps = ( RingOps i^i Com2 )
Theorem	iscrngo 32230	The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
|- ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )
Theorem	iscrngo2 32231*	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 32232*	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	crngorngo 32233	A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. CRingOps -> R e. RingOps )
Theorem	crngocom 32234	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 ) )
Theorem	crngm23 32235	Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( ( A H C ) H B ) )
Theorem	crngm4 32236	Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. CRingOps /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A H B ) H ( C H D ) ) = ( ( A H C ) H ( B H D ) ) )
Theorem	fldcrng 32237	A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.)
|- ( K e. Fld -> K e. CRingOps )
Theorem	isfld2 32238	The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( K e. Fld <-> ( K e. DivRingOps /\ K e. CRingOps ) )
Theorem	crngohomfo 32239	The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- J = ( 1st ` S )   &    |- Y = ran J   =>    |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps )
21.18.17  Ideals
Syntax	cidl 32240	Extend class notation with the class of ideals.
class Idl
Syntax	cpridl 32241	Extend class notation with the class of prime ideals.
class PrIdl
Syntax	cmaxidl 32242	Extend class notation with the class of maximal ideals.
class MaxIdl
Definition	df-idl 32243*	Define the class of (two-sided) ideals of a ring R. A subset of R is an ideal if it contains 0, is closed under addition, and is closed under multiplication on either side by any element of R. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- Idl = ( r e. RingOps |-> { i e. ~P ran ( 1st ` r ) | ( (GId ` ( 1st ` r ) ) e. i /\ A. x e. i ( A. y e. i ( x ( 1st ` r ) y ) e. i /\ A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i ) ) ) } )
Definition	df-pridl 32244*	Define the class of prime ideals of a ring R. A proper ideal I of R is prime if whenever A B C_ I for ideals A and B, either A C_ I or B C_ I. The more familiar definition using elements rather than ideals is equivalent provided R is commutative; see ispridl2 32271 and ispridlc 32303. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- PrIdl = ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
Definition	df-maxidl 32245*	Define the class of maximal ideals of a ring R. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- MaxIdl = ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) } )
Theorem	idlval 32246*	The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. RingOps -> ( Idl ` R ) = { i e. ~P X | ( Z e. i /\ A. x e. i ( A. y e. i ( x G y ) e. i /\ A. z e. X ( ( z H x ) e. i /\ ( x H z ) e. i ) ) ) } )
Theorem	isidl 32247*	The predicate "is an ideal of the ring R." (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. RingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) ) )
Theorem	isidlc 32248*	The predicate "is an ideal of the commutative ring R." (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. CRingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) ) )
Theorem	idlss 32249	An ideal of R is a subset of R. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> I C_ X )
Theorem	idlcl 32250	An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> A e. X )
Theorem	idl0cl 32251	An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- Z = (GId ` G )   =>    |- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> Z e. I )
Theorem	idladdcl 32252	An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   =>    |- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A G B ) e. I )
Theorem	idllmulcl 32253	An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. X ) ) -> ( B H A ) e. I )
Theorem	idlrmulcl 32254	An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. X ) ) -> ( A H B ) e. I )
Theorem	idlnegcl 32255	An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- N = ( inv ` G )   =>    |- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> ( N ` A ) e. I )
Theorem	idlsubcl 32256	An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- D = ( /g ` G )   =>    |- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A D B ) e. I )
Theorem	rngoidl 32257	A ring R is an R ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> X e. ( Idl ` R ) )
Theorem	0idl 32258	The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- Z = (GId ` G )   =>    |- ( R e. RingOps -> { Z } e. ( Idl ` R ) )
Theorem	1idl 32259	Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( U e. I <-> I = X ) )
Theorem	0rngo 32260	In a ring, 0 = 1 iff the ring contains only 0. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( R e. RingOps -> ( Z = U <-> X = { Z } ) )
Theorem	divrngidl 32261	The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. DivRingOps -> ( Idl ` R ) = { { Z } , X } )
Theorem	intidl 32262	The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> |^| C e. ( Idl ` R ) )
Theorem	inidl 32263	The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> ( I i^i J ) e. ( Idl ` R ) )
Theorem	unichnidl 32264*	The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- ( ( R e. RingOps /\ ( C =/= (/) /\ C C_ ( Idl ` R ) /\ A. i e. C A. j e. C ( i C_ j \/ j C_ i ) ) ) -> U. C e. ( Idl ` R ) )
Theorem	keridl 32265	The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.)
|- G = ( 1st ` S )   &    |- Z = (GId ` G )   =>    |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( `' F " { Z } ) e. ( Idl ` R ) )
Theorem	pridlval 32266*	The class of prime ideals of a ring R. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( PrIdl ` R ) = { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
Theorem	ispridl 32267*	The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
Theorem	pridlidl 32268	A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> P e. ( Idl ` R ) )
Theorem	pridlnr 32269	A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> P =/= X )
Theorem	pridl 32270*	The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- H = ( 2nd ` R )   =>    |- ( ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( Idl ` R ) /\ B e. ( Idl ` R ) /\ A. x e. A A. y e. B ( x H y ) e. P ) ) -> ( A C_ P \/ B C_ P ) )
Theorem	ispridl2 32271*	A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 32303 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) ) -> P e. ( PrIdl ` R ) )
Theorem	maxidlval 32272*	The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( MaxIdl ` R ) = { i e. ( Idl ` R ) | ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } )
Theorem	ismaxidl 32273*	The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( M e. ( MaxIdl ` R ) <-> ( M e. ( Idl ` R ) /\ M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) ) )
Theorem	maxidlidl 32274	A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M e. ( Idl ` R ) )
Theorem	maxidlnr 32275	A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M =/= X )
Theorem	maxidlmax 32276	A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) /\ ( I e. ( Idl ` R ) /\ M C_ I ) ) -> ( I = M \/ I = X ) )
Theorem	maxidln1 32277	One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.)
|- H = ( 2nd ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> -. U e. M )
Theorem	maxidln0 32278	A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> U =/= Z )
21.18.18  Prime rings and integral domains
Syntax	cprrng 32279	Extend class notation with the class of prime rings.
class PrRing
Syntax	cdmn 32280	Extend class notation with the class of domains.
class Dmn
Definition	df-prrngo 32281	Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- PrRing = { r e. RingOps | { (GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }
Definition	df-dmn 32282	Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- Dmn = ( PrRing i^i Com2 )
Theorem	isprrngo 32283	The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- Z = (GId ` G )   =>    |- ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )
Theorem	prrngorngo 32284	A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. PrRing -> R e. RingOps )
Theorem	smprngopr 32285	A simple ring (one whose only ideals are 0 and R) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. PrRing )
Theorem	divrngpr 32286	A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ( R e. DivRingOps -> R e. PrRing )
Theorem	isdmn 32287	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. Dmn <-> ( R e. PrRing /\ R e. Com2 ) )
Theorem	isdmn2 32288	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. Dmn <-> ( R e. PrRing /\ R e. CRingOps ) )
Theorem	dmncrng 32289	A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ( R e. Dmn -> R e. CRingOps )
Theorem	dmnrngo 32290	A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ( R e. Dmn -> R e. RingOps )
Theorem	flddmn 32291	A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( K e. Fld -> K e. Dmn )
21.18.19  Ideal generators
Syntax	cigen 32292	Extend class notation with the ideal generation function.
class IdlGen
Definition	df-igen 32293*	Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- IdlGen = ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )
Theorem	igenval 32294*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
Theorem	igenss 32295	A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> S C_ ( R IdlGen S ) )
Theorem	igenidl 32296	The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) e. ( Idl ` R ) )
Theorem	igenmin 32297	The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> ( R IdlGen S ) C_ I )
Theorem	igenidl2 32298	The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( R IdlGen I ) = I )
Theorem	igenval2 32299*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> ( ( R IdlGen S ) = I <-> ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) )
Theorem	prnc 32300*	A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. CRingOps /\ A e. X ) -> ( R IdlGen { A } ) = { x e. X | E. y e. X x = ( y H A ) } )