P. 388 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38701-38800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngoneglmul 38701	Obsolete theorem, use ringmneg1 20452 instead. Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁‘𝐴)𝐻𝐵))
Theorem	rngonegrmul 38702	Obsolete theorem, use ringmneg2 20453 instead. Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁‘𝐵)))
Theorem	rngosubdi 38703	Obsolete theorem, use ringsubdi 20455 instead. Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶)))
Theorem	rngosubdir 38704	Obsolete theorem, use ringsubdir 20456 instead. Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)))
Theorem	zerdivemp1x 38705*	Obsolete theorem, use ringinvnzdiv 20449 instead. In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20449. (Contributed by Jeff Madsen, 18-Apr-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃𝑎 ∈ 𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵 ∈ 𝑋 → ((𝐴𝐻𝐵) = 𝑍 → 𝐵 = 𝑍)))
21.25.17  Division Rings
Syntax	cdrng 38706	Extend class notation with the class of all division rings.
class DivRingOps
Definition	df-drngo 38707*	Obsolete defintion, use df-drng 20898 instead. 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 = {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
Theorem	isdivrngo 38708	Obsolete theorem, use isdrng2 20912 instead. The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐻 ∈ 𝐴 → (⟨𝐺, 𝐻⟩ ∈ DivRingOps ↔ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)))
Theorem	drngoi 38709	Obsolete theorem, use drngring 20903 and drngmgp 20914 instead. The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
Theorem	gidsn 38710	Obsolete as of 23-Jan-2020. Use mnd1id 18893 instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (GId‘{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) = 𝐴
Theorem	zrdivrng 38711	Obsolete theorem, use zrdrng 20941 instead. The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ¬ ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ∈ DivRingOps
Theorem	dvrunz 38712	Obsolete theorem, use drngunz 20916 instead. In a division ring the ring unit is different from the zero. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍)
Theorem	isgrpda 38713*	Obsolete theorem, use isgrpde 19087 instead. Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑋 ∈ V)    &   ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑈𝐺𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ 𝑋 (𝑛𝐺𝑥) = 𝑈)    ⇒   ⊢ (𝜑 → 𝐺 ∈ GrpOp)
Theorem	isdrngo1 38714	Obsolete theorem, use isdrng2 20912 instead. The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
Theorem	divrngcl 38715	Obsolete theorem, use drngmcl 20924 instead. The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ DivRingOps ∧ 𝐴 ∈ (𝑋 ∖ {𝑍}) ∧ 𝐵 ∈ (𝑋 ∖ {𝑍})) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ {𝑍}))
Theorem	isdrngo2 38716*	Obsolete theorem, use isdrng3 20922 instead. A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
Theorem	isdrngo3 38717*	Obsolete theorem, use isdrng5 20923 instead. A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
21.25.18  Ring homomorphisms
Syntax	crngohom 38718	Extend class notation with the class of ring homomorphisms.
class RingOpsHom
Syntax	crngoiso 38719	Extend class notation with the class of ring isomorphisms.
class RingOpsIso
Syntax	crisc 38720	Extend class notation with the ring isomorphism relation.
class ≃𝑟
Definition	df-rngohom 38721*	Obsolete defintion, use df-rhm 20619 instead. Define the function which gives the set of ring homomorphisms between two given rings. (New usage is discouraged.) (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 38722*	Obsolete theorem, use rhmval0 20622 instead. The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})
Theorem	isrngohom 38723*	Obsolete theorem, use isrhm0 20623 instead. The predicate "is a ring homomorphism from 𝑅 to 𝑆". (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))))))
Theorem	rngohomf 38724	Obsolete theorem, use rhmf 20632 instead. A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:𝑋⟶𝑌)
Theorem	rngohomcl 38725	Obsolete theorem, use rhmcl 20633 instead. Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌)
Theorem	rngohom1 38726	Obsolete theorem, use rhm1 20641 instead. A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    &   ⊢ 𝐾 = (2nd ‘𝑆)    &   ⊢ 𝑉 = (GId‘𝐾)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑈) = 𝑉)
Theorem	rngohomadd 38727	Obsolete theorem, use rhmadd 20635 instead. Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵)))
Theorem	rngohommul 38728	Obsolete theorem, use rhmmul 20637 instead. Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝐾 = (2nd ‘𝑆)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))
Theorem	rngogrphom 38729	Obsolete theorem, use rhmghm 20631 instead. A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐽 = (1st ‘𝑆)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹 ∈ (𝐺 GrpOpHom 𝐽))
Theorem	rngohom0 38730	Obsolete theorem, use rhm0 20640 instead. A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑊 = (GId‘𝐽)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘𝑍) = 𝑊)
Theorem	rngohomsub 38731	Obsolete theorem, use rhmsub 20636 instead. Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐻 = ( /𝑔 ‘𝐺)    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝐾 = ( /𝑔 ‘𝐽)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))
Theorem	rngohomco 38732	Obsolete theorem, use rhmco 20656 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 38733	Obsolete theorem, use rhmkerinj 20657 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 38734*	Obsolete defintion, use df-rim 20620 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 38735*	Obsolete theorem, use rimval 20647 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 38736	Obsolete theorem, use isrim 20645 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 38737	Obsolete theorem, use rimf1o 20646 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 38738	Obsolete theorem, use rimrhm 20648 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 38739	Obsolete theorem, use rimcnv 20634 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 38740	Obsolete theorem, use rimco 20664 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 38741*	Obsolete defintion, use df-ric 20660 instead. Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (New usage is discouraged.)
⊢ ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))}
Theorem	isriscg 38742*	Obsolete theorem, use isbrric2 20670 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 38743*	Obsolete theorem, use isbrric2 20670 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 38744*	Obsolete theorem, use brric2 20671 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 38745	Obsolete theorem, use brrici 20663 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 38746	Obsolete theorem, use ricer 20673 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.25.19  Commutative rings
Syntax	ccm2 38747	Extend class notation with a class that adds commutativity to various flavors of rings.
class Com2
Definition	df-com2 38748*	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 38749	Extend class notation with the class of all fields.
class Fld
Definition	df-fld 38750	Obsolete defintion, use df-field 20899 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 38751	Extend class notation with the class of commutative rings.
class CRingOps
Definition	df-crngo 38752	Obsolete defintion, use df-cring 20381 instead. Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) (New usage is discouraged.)
⊢ CRingOps = (RingOps ∩ Com2)
Theorem	iscom2 38753*	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 38754	Obsolete theorem, use iscrng 20385 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 38755*	Obsolete theorem, use iscrng2 20397 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 38756*	Obsolete theorem, use iscrngd 20440 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 38757	Obsolete theorem, use flddrngd 20910 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 38758	Obsolete theorem, use crngringd 20391 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 38759	Obsolete theorem, use crngcom 20396 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 38760	Obsolete theorem, use crng32d 20405 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 38761	Obsolete theorem, use crng4 20406 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 38762	Obsolete theorem, use fldcrngd 20911 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 38763	Obsolete theorem, use isfld 20909 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 38764	Obsolete theorem, use crngrhmfo 20643 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.25.20  Ideals
Syntax	cidl 38765	Extend class notation with the class of ideals.
class Idl
Syntax	cpridl 38766	Extend class notation with the class of prime ideals.
class PrIdl
Syntax	cmaxidl 38767	Extend class notation with the class of maximal ideals.
class MaxIdl
Definition	df-idl 38768*	Obsolete defintion, use df-2idl 21458 (or df-lidl 21401) 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 38769*	Obsolete defintion, use df-prmidl 21530 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 38796 and ispridlc 38828. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)
⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Definition	df-maxidl 38770*	Obsolete defintion, use df-mxidl 33871 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 38771*	Obsolete theorem, use 2idlval 21459 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 38772*	Obsolete theorem, use df2idl2 21465 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 38773*	Obsolete theorem, use df2idl2crng 21490 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 38774	Obsolete theorem, use 2idlss 21470 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 38775	Obsolete theorem, use 2idllidld 21462 and lidlbasel 21406 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 38776	Obsolete theorem, use ringrng 20432 and rng2idl0 21475 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 38777	Obsolete theorem, use 2idllidld 21462 and lidlacl 21415 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 38778	Obsolete theorem, use 2idllidld 21462 and lidlmcl 21419 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 38779	Obsolete theorem, use 2idlridld 21463 and lidlmcl 21419 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 38780	Obsolete theorem, use 2idllidld 21462 and lidlnegcl 21416 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 38781	Obsolete theorem, use 2idllidld 21462 and lidlsubcl 21418 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 38782	Obsolete theorem, use 2idl1 21469 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 38783	Obsolete theorem, use 2idl0 21468 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 38784	Obsolete theorem, use 2idllidld 21462 and lidl1el 21420 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 38785	Obsolete theorem, use 0ring01eqbi2 20699 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 38786	Obsolete theorem, use drngnidl 21446 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 38787	Obsolete theorem, use intlidl 33856 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 38788	Obsolete theorem, use inlidl 33857 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 38789*	Obsolete theorem, use unichnlidl 21431 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 38790	Obsolete theorem, use kerlidl 21486 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 38791*	Obsolete theorem, use prmidlval 21531 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 38792*	Obsolete theorem, use isprmidl 21532 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 38793	Obsolete theorem, use prmidlidl 21538 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 38794	Obsolete theorem, use prmidlnr 21533 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 38795*	Obsolete theorem, use isprmidlc 21541 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 38796*	Obsolete theorem, use prmidl2 21535 instead. A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38828 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 38797*	Obsolete theorem, use mxidlval 33872 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 38798*	Obsolete theorem, use ismxidl 33873 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 38799	Obsolete theorem, use mxidlidl 33874 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 38800	Obsolete theorem, use mxidlnr 33875 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‘𝑅)) → 𝑀 ≠ 𝑋)