P. 391 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39001-39100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngohomco 39001	Obsolete theorem, use rhmco 20744 instead. The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇))
Theorem	rngokerinj 39002	Obsolete theorem, use rhmkerinj 20745 instead. A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = (GId‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑍 = (GId‘𝐽)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑍}) = {𝑊}))
Definition	df-rngoiso 39003*	Obsolete defintion, use df-rim 20708 instead. Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.) (New usage is discouraged.)
⊢ RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran (1st ‘𝑠)})
Theorem	rngoisoval 39004*	Obsolete theorem, use rimval 20735 instead. The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsIso 𝑆) = {𝑓 ∈ (𝑅 RingOpsHom 𝑆) ∣ 𝑓:𝑋–1-1-onto→𝑌})
Theorem	isrngoiso 39005	Obsolete theorem, use isrim 20733 instead. The predicate "is a ring isomorphism between 𝑅 and 𝑆". (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–1-1-onto→𝑌)))
Theorem	rngoiso1o 39006	Obsolete theorem, use rimf1o 20734 instead. A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌)
Theorem	rngoisohom 39007	Obsolete theorem, use rimrhm 20736 instead. A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆))
Theorem	rngoisocnv 39008	Obsolete theorem, use rimcnv 20722 instead. The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → ◡𝐹 ∈ (𝑆 RingOpsIso 𝑅))
Theorem	rngoisoco 39009	Obsolete theorem, use rimco 20752 instead. The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇))
Definition	df-risc 39010*	Obsolete defintion, use dfric2 20762 instead. Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (New usage is discouraged.)
⊢ ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))}
Theorem	isriscg 39011*	Obsolete theorem, use isbrric2 20758 instead. The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆))))
Theorem	isrisc 39012*	Obsolete theorem, use isbrric2 20758 instead. The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆)))
Theorem	risc 39013*	Obsolete theorem, use brric2 20759 instead. The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 ≃𝑟 𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆)))
Theorem	risci 39014	Obsolete theorem, use brrici 20751 instead. Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝑅 ≃𝑟 𝑆)
Theorem	riscer 39015	Obsolete theorem, use ricer 20761 instead. Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ≃𝑟 Er dom ≃𝑟
21.26.19  Commutative rings
Syntax	ccm2 39016	Extend class notation with a class that adds commutativity to various flavors of rings.
class Com2
Definition	df-com2 39017*	Obsolete definition, used in other obsolete definitions only. A device to add commutativity to various sorts of rings. I use ran 𝑔 because I suppose 𝑔 has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
⊢ Com2 = {⟨𝑔, ℎ⟩ ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)}
Syntax	cfld 39018	Extend class notation with the class of all fields.
class Fld
Definition	df-fld 39019	Obsolete defintion, use df-field 20988 instead. 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 ∩ Com2)
Syntax	ccring 39020	Extend class notation with the class of commutative rings.
class CRingOps
Definition	df-crngo 39021	Obsolete defintion, use df-cring 20467 instead. Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) (New usage is discouraged.)
⊢ CRingOps = (RingOps ∩ Com2)
Theorem	iscom2 39022*	Obsolete theorem, used (as lemma) in other obsolete theorems only. A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵) → (⟨𝐺, 𝐻⟩ ∈ Com2 ↔ ∀𝑎 ∈ ran 𝐺∀𝑏 ∈ ran 𝐺(𝑎𝐻𝑏) = (𝑏𝐻𝑎)))
Theorem	iscrngo 39023	Obsolete theorem, use iscrng 20471 instead. The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2))
Theorem	iscrngo2 39024*	Obsolete theorem, use iscrng2 20484 instead. The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
Theorem	iscringd 39025*	Obsolete theorem, use iscrngd 20528 instead. Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐺 ∈ AbelOp)    &   ⊢ (𝜑 → 𝑋 = ran 𝐺)    &   ⊢ (𝜑 → 𝐻:(𝑋 × 𝑋)⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝑈) = 𝑦)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐻𝑦) = (𝑦𝐻𝑥))    ⇒   ⊢ (𝜑 → ⟨𝐺, 𝐻⟩ ∈ CRingOps)
Theorem	flddivrng 39026	Obsolete theorem, use flddrngd 20999 instead. A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ DivRingOps)
Theorem	crngorngo 39027	Obsolete theorem, use crngringd 20478 instead. A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
Theorem	crngocom 39028	Obsolete theorem, use crngcom 20483 instead. The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) = (𝐵𝐻𝐴))
Theorem	crngm23 39029	Obsolete theorem, use crng32d 20492 instead. Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐻𝐵))
Theorem	crngm4 39030	Obsolete theorem, use crng4 20493 instead. Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻(𝐶𝐻𝐷)) = ((𝐴𝐻𝐶)𝐻(𝐵𝐻𝐷)))
Theorem	fldcrngo 39031	Obsolete theorem, use fldcrngd 21000 instead. A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps)
Theorem	isfld2 39032	Obsolete theorem, use isfld 20998 instead. The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps))
Theorem	crngohomfo 39033	Obsolete theorem, use crngrhmfo 20731 instead. The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–onto→𝑌)) → 𝑆 ∈ CRingOps)
21.26.20  Ideals
Syntax	cidl 39034	Extend class notation with the class of ideals.
class Idl
Syntax	cpridl 39035	Extend class notation with the class of prime ideals.
class PrIdl
Syntax	cmaxidl 39036	Extend class notation with the class of maximal ideals.
class MaxIdl
Definition	df-idl 39037*	Obsolete defintion, use df-2idl 21548 (or df-lidl 21491) instead. Define the class of (two-sided) ideals of a ring 𝑅. A subset of 𝑅 is an ideal if it contains 0, is closed under addition, and is closed under multiplication on either side by any element of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)
⊢ Idl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1st ‘𝑟) ∣ ((GId‘(1st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st ‘𝑟)((𝑧(2nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd ‘𝑟)𝑧) ∈ 𝑖)))})
Definition	df-pridl 39038*	Obsolete defintion, use df-prmidl 21622 instead. Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see ispridl2 39065 and ispridlc 39097. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)
⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Definition	df-maxidl 39039*	Obsolete defintion, use df-mxidl 34031 instead. Define the class of maximal ideals of a ring 𝑅. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) (New usage is discouraged.)
⊢ MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})
Theorem	idlval 39040*	Obsolete theorem, use 2idlval 21549 instead. The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → (Idl‘𝑅) = {𝑖 ∈ 𝒫 𝑋 ∣ (𝑍 ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥𝐺𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝑖 ∧ (𝑥𝐻𝑧) ∈ 𝑖)))})
Theorem	isidl 39041*	Obsolete theorem, use df2idl2 21556 instead. The predicate "is an ideal of the ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)))))
Theorem	isidlc 39042*	Obsolete theorem, use df2idl2crng 21582 instead. The predicate "is an ideal of the commutative ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
Theorem	idlss 39043	Obsolete theorem, use 2idlss 21561 instead. An ideal of 𝑅 is a subset of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝐼 ⊆ 𝑋)
Theorem	idlcl 39044	Obsolete theorem, use 2idllidld 21552 and lidlbasel 21496 instead. An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝑋)
Theorem	idl0cl 39045	Obsolete theorem, use ringrng 20519 and rng2idl0 21566 instead. An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝐼)
Theorem	idladdcl 39046	Obsolete theorem, use 2idllidld 21552 and lidlacl 21505 instead. An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼)
Theorem	idllmulcl 39047	Obsolete theorem, use 2idllidld 21552 and lidlmcl 21509 instead. An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐵𝐻𝐴) ∈ 𝐼)
Theorem	idlrmulcl 39048	Obsolete theorem, use 2idlridld 21553 and lidlmcl 21509 instead. An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝐼)
Theorem	idlnegcl 39049	Obsolete theorem, use 2idllidld 21552 and lidlnegcl 21506 instead. An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → (𝑁‘𝐴) ∈ 𝐼)
Theorem	idlsubcl 39050	Obsolete theorem, use 2idllidld 21552 and lidlsubcl 21508 instead. An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐷𝐵) ∈ 𝐼)
Theorem	rngoidl 39051	Obsolete theorem, use 2idl1 21560 instead. A ring 𝑅 is an 𝑅 ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅))
Theorem	0idl 39052	Obsolete theorem, use 2idl0 21559 instead. The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
Theorem	1idl 39053	Obsolete theorem, use 2idl1el 21554 instead. Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋))
Theorem	0rngo 39054	Obsolete theorem, use 0ring01eqbi2 20788 instead. In a ring, 0 = 1 iff the ring contains only 0. (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑍 = 𝑈 ↔ 𝑋 = {𝑍}))
Theorem	divrngidl 39055	Obsolete theorem, use drngnidl 21536 instead. The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ DivRingOps → (Idl‘𝑅) = {{𝑍}, 𝑋})
Theorem	intidl 39056	Obsolete theorem, use intlidl 34016 instead. The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅))
Theorem	inidl 39057	Obsolete theorem, use inlidl 34017 instead. The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅))
Theorem	unichnidl 39058*	Obsolete theorem, use unichnlidl 21521 instead. The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))
Theorem	keridl 39059	Obsolete theorem, use ker2idl 21578 instead. The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑆)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅))
Theorem	pridlval 39060*	Obsolete theorem, use prmidlval 21623 instead. The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (PrIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Theorem	ispridl 39061*	Obsolete theorem, use isprmidl 21624 instead. The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃)))))
Theorem	pridlidl 39062	Obsolete theorem, use prmidlidl 21630 instead. A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅))
Theorem	pridlnr 39063	Obsolete theorem, use prmidlnr 21625 instead. A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋)
Theorem	pridl 39064*	Obsolete theorem, use isprmidlc 21633 instead. The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐻 = (2nd ‘𝑅)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃))
Theorem	ispridl2 39065*	Obsolete theorem, use prmidl2 21627 instead. A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 39097 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
Theorem	maxidlval 39066*	Obsolete theorem, use mxidlval 34032 instead. The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))})
Theorem	ismaxidl 39067*	Obsolete theorem, use ismxidl 34033 instead. The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋)))))
Theorem	maxidlidl 39068	Obsolete theorem, use mxidlidl 34034 instead. A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅))
Theorem	maxidlnr 39069	Obsolete theorem, use mxidlnr 34035 instead. A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋)
Theorem	maxidlmax 39070	Obsolete theorem, use mxidlmax 34036 instead. A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋))
Theorem	maxidln1 39071	Obsolete theorem, use mxidln1 34037 instead. One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀)
Theorem	maxidln0 39072	Obsolete theorem, use mxidlnzr 34038 instead. A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑈 ≠ 𝑍)
21.26.21  Prime rings and integral domains
Syntax	cprrng 39073	Extend class notation with the class of prime rings.
class PrRing
Syntax	cdmn 39074	Extend class notation with the class of domains.
class Dmn
Definition	df-prrngo 39075	Obsolete definition, use df-prmring 49525 instead. 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.) (New usage is discouraged.)
⊢ PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)}
Definition	df-dmn 39076	Obsolete definition, use df-idom 20953 resp. dfidom2 49533 instead. Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)
⊢ Dmn = (PrRing ∩ Com2)
Theorem	isprrngo 39077	Obsolete theorem, use isprmrng 49526 instead. The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
Theorem	prrngorngo 39078	Obsolete theorem, use prmrngring 49528 instead. A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps)
Theorem	smprngopr 39079	Obsolete theorem, use smprngprmrng 49529 instead. A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)
Theorem	divrngpr 39080	Obsolete theorem, use drngprmrng 49530 instead. A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing)
Theorem	isdmn 39081	Obsolete theorem, use isidom2 49534 instead. The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2))
Theorem	isdmn2 39082	Obsolete theorem, use isidom2 49534 instead. The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps))
Theorem	dmncrng 39083	Obsolete theorem, use idomcringd 20983 instead. A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps)
Theorem	dmnrngo 39084	Obsolete theorem, use idomringd 20984 instead. A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps)
Theorem	flddmn 39085	Obsolete theorem, use fldidom 21034 instead. A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn)
21.26.22  Ideal generators
Syntax	cigen 39086	Extend class notation with the ideal generation function.
class IdlGen
Definition	df-igen 39087*	Obsolete definition, use df-rsp 21492 instead. Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
Theorem	igenval 39088*	Obsolete theorem, use rspvalint 21528 instead. The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
Theorem	igenss 39089	Obsolete theorem, use rspssid 21524 instead. A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆))
Theorem	igenidl 39090	Obsolete theorem, use rspcl 21523 instead. The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅))
Theorem	igenmin 39091	Obsolete theorem, use rspssp 21527 instead. The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼) → (𝑅 IdlGen 𝑆) ⊆ 𝐼)
Theorem	igenidl2 39092	Obsolete theorem, use rsp2idlid 33977 instead. The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼)
Theorem	igenval2 39093*	Obsolete theorem, use rspprop 21529 instead. The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗))))
Theorem	prnc 39094*	Obsolete theorem, use rspsn0 21531 instead (holds for arbitrary rings). A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
Theorem	isfldidl 39095	Obsolete theorem, use isfieldidl 21545 instead. Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	isfldidl2 39096	Obsolete theorem, use isfieldidl2 21546 instead. Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑋 ≠ {𝑍} ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	ispridlc 39097*	Obsolete theorem, use isprmidlc 21633 instead. The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
Theorem	pridlc 39098	Obsolete theorem, use prmidlc 21634 instead. Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃))
Theorem	pridlc2 39099	Obsolete theorem, use prmidlc2 21635 instead. Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃)
Theorem	pridlc3 39100	Obsolete theorem, use cmprmidlmcl 21636 instead. Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃))