P. 339 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33801-33900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	crngm23 33801	Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐻𝐵))
Theorem	crngm4 33802	Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻(𝐶𝐻𝐷)) = ((𝐴𝐻𝐶)𝐻(𝐵𝐻𝐷)))
Theorem	fldcrng 33803	A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps)
Theorem	isfld2 33804	The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps))
Theorem	crngohomfo 33805	The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐽 = (1st ‘𝑆)    &   ⊢ 𝑌 = ran 𝐽    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:𝑋–onto→𝑌)) → 𝑆 ∈ CRingOps)
20.19.20  Ideals
Syntax	cidl 33806	Extend class notation with the class of ideals.
class Idl
Syntax	cpridl 33807	Extend class notation with the class of prime ideals.
class PrIdl
Syntax	cmaxidl 33808	Extend class notation with the class of maximal ideals.
class MaxIdl
Definition	df-idl 33809*	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 33810*	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 33837 and ispridlc 33869. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Definition	df-maxidl 33811*	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 33812*	The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → (Idl‘𝑅) = {𝑖 ∈ 𝒫 𝑋 ∣ (𝑍 ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥𝐺𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝑖 ∧ (𝑥𝐻𝑧) ∈ 𝑖)))})
Theorem	isidl 33813*	The predicate "is an ideal of the ring 𝑅." (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼)))))
Theorem	isidlc 33814*	The predicate "is an ideal of the commutative ring 𝑅." (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 (𝑧𝐻𝑥) ∈ 𝐼))))
Theorem	idlss 33815	An ideal of 𝑅 is a subset of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝐼 ⊆ 𝑋)
Theorem	idlcl 33816	An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝑋)
Theorem	idl0cl 33817	An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝐼)
Theorem	idladdcl 33818	An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼)
Theorem	idllmulcl 33819	An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐵𝐻𝐴) ∈ 𝐼)
Theorem	idlrmulcl 33820	An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝐼)
Theorem	idlnegcl 33821	An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → (𝑁‘𝐴) ∈ 𝐼)
Theorem	idlsubcl 33822	An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐷𝐵) ∈ 𝐼)
Theorem	rngoidl 33823	A ring 𝑅 is an 𝑅 ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅))
Theorem	0idl 33824	The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
Theorem	1idl 33825	Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋))
Theorem	0rngo 33826	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 33827	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 33828	The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅))
Theorem	inidl 33829	The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅))
Theorem	unichnidl 33830*	The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))
Theorem	keridl 33831	The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑆)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅))
Theorem	pridlval 33832*	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 33833*	The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃)))))
Theorem	pridlidl 33834	A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅))
Theorem	pridlnr 33835	A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋)
Theorem	pridl 33836*	The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐻 = (2nd ‘𝑅)    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃))
Theorem	ispridl2 33837*	A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 33869 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
Theorem	maxidlval 33838*	The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))})
Theorem	ismaxidl 33839*	The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋)))))
Theorem	maxidlidl 33840	A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅))
Theorem	maxidlnr 33841	A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋)
Theorem	maxidlmax 33842	A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋))
Theorem	maxidln1 33843	One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀)
Theorem	maxidln0 33844	A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑈 ≠ 𝑍)
20.19.21  Prime rings and integral domains
Syntax	cprrng 33845	Extend class notation with the class of prime rings.
class PrRing
Syntax	cdmn 33846	Extend class notation with the class of domains.
class Dmn
Definition	df-prrngo 33847	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 33848	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 33849	The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
Theorem	prrngorngo 33850	A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps)
Theorem	smprngopr 33851	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 33852	A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing)
Theorem	isdmn 33853	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2))
Theorem	isdmn2 33854	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps))
Theorem	dmncrng 33855	A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps)
Theorem	dmnrngo 33856	A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps)
Theorem	flddmn 33857	A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn)
20.19.22  Ideal generators
Syntax	cigen 33858	Extend class notation with the ideal generation function.
class IdlGen
Definition	df-igen 33859*	Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
Theorem	igenval 33860*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
Theorem	igenss 33861	A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆))
Theorem	igenidl 33862	The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅))
Theorem	igenmin 33863	The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼) → (𝑅 IdlGen 𝑆) ⊆ 𝐼)
Theorem	igenidl2 33864	The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼)
Theorem	igenval2 33865*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗))))
Theorem	prnc 33866*	A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
Theorem	isfldidl 33867	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	isfldidl2 33868	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑋 ≠ {𝑍} ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	ispridlc 33869*	The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
Theorem	pridlc 33870	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃))
Theorem	pridlc2 33871	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃)
Theorem	pridlc3 33872	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃))
Theorem	isdmn3 33873*	The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))
Theorem	dmnnzd 33874	A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍))
Theorem	dmncan1 33875	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶))
Theorem	dmncan2 33876	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐶 ≠ 𝑍) → ((𝐴𝐻𝐶) = (𝐵𝐻𝐶) → 𝐴 = 𝐵))
20.20  Mathbox for Giovanni Mascellani
20.20.1  Tools for automatic proof building The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings.
Theorem	efald2 33877	A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ 𝜑 → ⊥)    ⇒   ⊢ 𝜑
Theorem	notbinot1 33878	Simplification rule of negation across a biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓))
Theorem	bicontr 33879	Biimplication of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥)
Theorem	impor 33880	An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	orfa 33881	The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((𝜑 ∨ ⊥) ↔ 𝜑)
Theorem	notbinot2 33882	Commutation rule between negation and biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓))
Theorem	biimpor 33883	A rewriting rule for biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒))
Theorem	unitresl 33884	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	unitresr 33885	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	orfa1 33886	Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ ⊥) → 𝜓)
Theorem	orfa2 33887	Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ ((𝜑 ∨ 𝜓) → 𝜓)
Theorem	bifald 33888	Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ ⊥))
Theorem	orsild 33889	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	orsird 33890	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	orcomdd 33891	Commutativity of logic disjunction, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∨ 𝜒)))
Theorem	cnf1dd 33892	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	cnf2dd 33893	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ¬ 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	cnfn1dd 33894	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	cnfn2dd 33895	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ ¬ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	or32dd 33896	A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃) ∨ 𝜏)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) ∨ 𝜃)))
Theorem	notornotel1 33897	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → ¬ (¬ 𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	notornotel2 33898	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → ¬ (𝜓 ∨ ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	contrd 33899	A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	an12i 33900	An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.)
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒))