P. 383 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38201-38300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	crngoiso 38201	Extend class notation with the class of ring isomorphisms.
class RingOpsIso
Syntax	crisc 38202	Extend class notation with the ring isomorphism relation.
class ≃𝑟
Definition	df-rngohom 38203*	Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ RingOpsHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))})
Theorem	rngohomval 38204*	The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})
Theorem	isrngohom 38205*	The predicate "is a ring homomorphism from 𝑅 to 𝑆". (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))))))
Theorem	rngohomf 38206	A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:𝑋⟶𝑌)
Theorem	rngohomcl 38207	Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌)
Theorem	rngohom1 38208	A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.)
⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑈) = 𝑉)
Theorem	rngohomadd 38209	Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵)))
Theorem	rngohommul 38210	Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝐾 = (2nd ‘𝑆)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))
Theorem	rngogrphom 38211	A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐽 = (1st ‘𝑆)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹 ∈ (𝐺 GrpOpHom 𝐽))
Theorem	rngohom0 38212	A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑊 = (GId‘𝐽)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑍) = 𝑊)
Theorem	rngohomsub 38213	Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐻 = ( /𝑔 ‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = ( /𝑔 ‘𝐽)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))
Theorem	rngohomco 38214	The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇))
Theorem	rngokerinj 38215	A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = (GId‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑍 = (GId‘𝐽)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑍}) = {𝑊}))
Definition	df-rngoiso 38216*	Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran (1st ‘𝑠)})
Theorem	rngoisoval 38217*	The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsIso 𝑆) = {𝑓 ∈ (𝑅 RingOpsHom 𝑆) ∣ 𝑓:𝑋–1-1-onto→𝑌})
Theorem	isrngoiso 38218	The predicate "is a ring isomorphism between 𝑅 and 𝑆". (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–1-1-onto→𝑌)))
Theorem	rngoiso1o 38219	A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌)
Theorem	rngoisohom 38220	A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆))
Theorem	rngoisocnv 38221	The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → ◡𝐹 ∈ (𝑆 RingOpsIso 𝑅))
Theorem	rngoisoco 38222	The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇))
Definition	df-risc 38223*	Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))}
Theorem	isriscg 38224*	The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆))))
Theorem	isrisc 38225*	The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (𝑅 ≃𝑟 𝑆 ↔ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆)))
Theorem	risc 38226*	The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 ≃𝑟 𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅 RingOpsIso 𝑆)))
Theorem	risci 38227	Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝑅 ≃𝑟 𝑆)
Theorem	riscer 38228	Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ≃𝑟 Er dom ≃𝑟
21.24.19  Commutative rings
Syntax	ccm2 38229	Extend class notation with a class that adds commutativity to various flavors of rings.
class Com2
Definition	df-com2 38230*	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 38231	Extend class notation with the class of all fields.
class Fld
Definition	df-fld 38232	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 38233	Extend class notation with the class of commutative rings.
class CRingOps
Definition	df-crngo 38234	Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ CRingOps = (RingOps ∩ Com2)
Theorem	iscom2 38235*	A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
⊢ ((𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐵) → (⟨𝐺, 𝐻⟩ ∈ Com2 ↔ ∀𝑎 ∈ ran 𝐺∀𝑏 ∈ ran 𝐺(𝑎𝐻𝑏) = (𝑏𝐻𝑎)))
Theorem	iscrngo 38236	The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2))
Theorem	iscrngo2 38237*	The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
Theorem	iscringd 38238*	Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ (𝜑 → 𝐺 ∈ AbelOp)    &   ⊢ (𝜑 → 𝑋 = ran 𝐺)    &   ⊢ (𝜑 → 𝐻:(𝑋 × 𝑋)⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝑈) = 𝑦)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐻𝑦) = (𝑦𝐻𝑥))    ⇒   ⊢ (𝜑 → ⟨𝐺, 𝐻⟩ ∈ CRingOps)
Theorem	flddivrng 38239	A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ DivRingOps)
Theorem	crngorngo 38240	A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
Theorem	crngocom 38241	The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) = (𝐵𝐻𝐴))
Theorem	crngm23 38242	Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐻𝐵))
Theorem	crngm4 38243	Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻(𝐶𝐻𝐷)) = ((𝐴𝐻𝐶)𝐻(𝐵𝐻𝐷)))
Theorem	fldcrngo 38244	A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps)
Theorem	isfld2 38245	The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps))
Theorem	crngohomfo 38246	The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐹:𝑋–onto→𝑌)) → 𝑆 ∈ CRingOps)
21.24.20  Ideals
Syntax	cidl 38247	Extend class notation with the class of ideals.
class Idl
Syntax	cpridl 38248	Extend class notation with the class of prime ideals.
class PrIdl
Syntax	cmaxidl 38249	Extend class notation with the class of maximal ideals.
class MaxIdl
Definition	df-idl 38250*	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.)
⊢ Idl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ 𝒫 ran (1st ‘𝑟) ∣ ((GId‘(1st ‘𝑟)) ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥(1st ‘𝑟)𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ ran (1st ‘𝑟)((𝑧(2nd ‘𝑟)𝑥) ∈ 𝑖 ∧ (𝑥(2nd ‘𝑟)𝑧) ∈ 𝑖)))})
Definition	df-pridl 38251*	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 38278 and ispridlc 38310. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Definition	df-maxidl 38252*	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.)
⊢ MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})
Theorem	idlval 38253*	The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → (Idl‘𝑅) = {𝑖 ∈ 𝒫 𝑋 ∣ (𝑍 ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥𝐺𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝑖 ∧ (𝑥𝐻𝑧) ∈ 𝑖)))})
Theorem	isidl 38254*	The predicate "is an ideal of the ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)))))
Theorem	isidlc 38255*	The predicate "is an ideal of the commutative ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
Theorem	idlss 38256	An ideal of 𝑅 is a subset of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝐼 ⊆ 𝑋)
Theorem	idlcl 38257	An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝑋)
Theorem	idl0cl 38258	An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝐼)
Theorem	idladdcl 38259	An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼)
Theorem	idllmulcl 38260	An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐵𝐻𝐴) ∈ 𝐼)
Theorem	idlrmulcl 38261	An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝐼)
Theorem	idlnegcl 38262	An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → (𝑁‘𝐴) ∈ 𝐼)
Theorem	idlsubcl 38263	An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐷𝐵) ∈ 𝐼)
Theorem	rngoidl 38264	A ring 𝑅 is an 𝑅 ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅))
Theorem	0idl 38265	The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
Theorem	1idl 38266	Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋))
Theorem	0rngo 38267	In a ring, 0 = 1 iff the ring contains only 0. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑍 = 𝑈 ↔ 𝑋 = {𝑍}))
Theorem	divrngidl 38268	The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ DivRingOps → (Idl‘𝑅) = {{𝑍}, 𝑋})
Theorem	intidl 38269	The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅))
Theorem	inidl 38270	The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅))
Theorem	unichnidl 38271*	The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))
Theorem	keridl 38272	The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑆)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅))
Theorem	pridlval 38273*	The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (PrIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Theorem	ispridl 38274*	The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃)))))
Theorem	pridlidl 38275	A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅))
Theorem	pridlnr 38276	A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋)
Theorem	pridl 38277*	The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐻 = (2nd ‘𝑅)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃))
Theorem	ispridl2 38278*	A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38310 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
Theorem	maxidlval 38279*	The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))})
Theorem	ismaxidl 38280*	The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋)))))
Theorem	maxidlidl 38281	A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅))
Theorem	maxidlnr 38282	A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋)
Theorem	maxidlmax 38283	A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋))
Theorem	maxidln1 38284	One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀)
Theorem	maxidln0 38285	A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑈 ≠ 𝑍)
21.24.21  Prime rings and integral domains
Syntax	cprrng 38286	Extend class notation with the class of prime rings.
class PrRing
Syntax	cdmn 38287	Extend class notation with the class of domains.
class Dmn
Definition	df-prrngo 38288	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 = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)}
Definition	df-dmn 38289	Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ Dmn = (PrRing ∩ Com2)
Theorem	isprrngo 38290	The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
Theorem	prrngorngo 38291	A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps)
Theorem	smprngopr 38292	A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)
Theorem	divrngpr 38293	A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing)
Theorem	isdmn 38294	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2))
Theorem	isdmn2 38295	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps))
Theorem	dmncrng 38296	A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps)
Theorem	dmnrngo 38297	A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps)
Theorem	flddmn 38298	A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn)
21.24.22  Ideal generators
Syntax	cigen 38299	Extend class notation with the ideal generation function.
class IdlGen
Definition	df-igen 38300*	Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})