P. 498 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49701-49800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fldcatALTV 49701*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCatALTV‘𝑈) ↾cat 𝐹) ∈ Cat)
Theorem	fldcALTV 49702*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → (((RingCatALTV‘𝑈) ↾cat 𝐽) ↾cat 𝐹) ∈ Cat)
Theorem	fldhmsubcALTV 49703*	According to df-subc 18037, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 18065 and subcss2 18068). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐹 ∈ (Subcat‘((RingCatALTV‘𝑈) ↾cat 𝐽)))
21.52.18.7  Subrings of the complex numbers
Theorem	subrgccsscc 49704	A subring of the complex numbers is a subset of the complex numbers. (Contributed by AV, 26-Oct-2026.)
⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
Theorem	subrgcccrng 49705	A subring of the complex numbers is a commutative ring. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 ∈ (SubRing‘ℂfld)    ⇒   ⊢ 𝑅 ∈ CRing
Theorem	subrgcccrng0 49706	The zero of a subring of the complex numbers. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 ∈ (SubRing‘ℂfld)    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	subrgcccrng1 49707	The one of a subring of the complex numbers. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 ∈ (SubRing‘ℂfld)    ⇒   ⊢ 1 = (1r‘𝑅)
Theorem	subrgccnzr 49708	A subring of the complex numbers is a nonzero ring. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 ∈ (SubRing‘ℂfld)    ⇒   ⊢ 𝑅 ∈ NzRing
Theorem	subrgccdom 49709	A subring of the complex numbers is a domain. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 ∈ (SubRing‘ℂfld)    ⇒   ⊢ 𝑅 ∈ Domn
Theorem	subrgccidom 49710	A subring of the complex numbers is an integral domain. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 ∈ (SubRing‘ℂfld)    ⇒   ⊢ 𝑅 ∈ IDomn
21.52.18.8  Elementary properties of complex polynomials (extension)
Theorem	linplyfv 49711*	The evaluation of a linear polynomial over a subset of the complex numbers at a complex number. (Contributed by AV, 31-Oct-2026.)
⊢ 𝑃 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...1)((𝐶‘𝑘) · (𝑧↑𝑘)))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐶 ∈ (𝑆 ↑m ℕ0) ∧ 𝑋 ∈ ℂ) → (𝑃‘𝑋) = ((𝐶‘0) + ((𝐶‘1) · 𝑋)))
Theorem	linply2cfv 49712*	The evaluation of a linear polynomial over a subset of the complex numbers with explicit coefficients at a complex number. (Contributed by AV, 31-Oct-2026.)
⊢ 𝑃 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...1)((𝐶‘𝑘) · (𝑧↑𝑘)))    &   ⊢ 𝐶 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 𝐴, 𝐵))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝑋 ∈ ℂ) → (𝑃‘𝑋) = (𝐴 + (𝐵 · 𝑋)))
Theorem	linply 49713*	A linear polynomial over a subset of the complex numbers is a polynomial over the subset of the complex numbers. (Contributed by AV, 31-Oct-2026.)
⊢ 𝑃 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...1)((𝐶‘𝑘) · (𝑧↑𝑘)))    ⇒   ⊢ ((𝑆 ⊆ ℂ ∧ 𝐶 ∈ (𝑆 ↑m ℕ0)) → 𝑃 ∈ (Poly‘𝑆))
21.52.18.9  Adjunction of a complex number to the ring of integers
Syntax	caz 49714	Extend class notation with the adjunctions of a complex number to the ring of integers.
class Z[]
Definition	df-az 49715	Define the mapping yielding the adjunctions of a complex number to the ring of integers. See also Wikipedia https://en.wikipedia.org/wiki/Subring#Adjoining. (Proposed by TA, 29-Oct-2026.) (Contributed by AV, 30-Oct-2026.)
⊢ Z[] = (𝑠 ∈ ℂ ↦ ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑠})))
Theorem	azval 49716	An adjunction of a complex number to the ring of integers. (Contributed by AV, 30-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (Z[]‘𝑆) = ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑆})))
Theorem	elaz 49717	Elementhood in an adjunction of a complex number to the ring of integers. Such an element is called "extended integer" in the following. (Contributed by AV, 30-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (𝐴 ∈ (Z[]‘𝑆) ↔ 𝐴 ∈ ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑆}))))
Theorem	azssid 49718	The union of the integers and the adjoined complex number are a subset of the adjunction. (Contributed by AV, 31-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (ℤ ∪ {𝑆}) ⊆ (Z[]‘𝑆))
Theorem	elazim 49719	Representation of an extended integer. (Contributed by AV, 31-Oct-2026.)
⊢ ((𝑆 ∈ ℂ ∧ 𝐴 ∈ (Z[]‘𝑆)) → 𝐴 ∈ ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑆})))
Theorem	azcn 49720	An extended integer is a complex number. (Contributed by AV, 31-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (𝐴 ∈ (Z[]‘𝑆) → 𝐴 ∈ ℂ))
Theorem	zelaz 49721	An integer is an extended integer. (Contributed by AV, 31-Oct-2026.)
⊢ ((𝑆 ∈ ℂ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈ (Z[]‘𝑆))
Theorem	adcnelaz 49722	The adjoined complex number is an extended integer. (Contributed by AV, 31-Oct-2026.)
⊢ (𝑆 ∈ ℂ → 𝑆 ∈ (Z[]‘𝑆))
Syntax	claz 49723	Extend class notation with the linear adjunctions of a complex number to the ring of integers.
class Z[]l
Definition	df-laz 49724*	Define the mapping yielding the adjunctions of a complex number to the ring of integers. Analogous to df-gz 17152. (Contributed by AV, 24-Oct-2026.)
⊢ Z[]l = (𝑠 ∈ ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))})
Theorem	lazval 49725*	An adjunction of a complex number to the ring of integers. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (Z[]l‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑆))})
Theorem	ellaz 49726*	Elementhood in an adjunction of a complex number to the ring of integers. Such an element is also called "extended integer" in the following. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (𝐴 ∈ (Z[]l‘𝑆) ↔ (𝐴 ∈ ℂ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝐴 = (𝑎 + (𝑏 · 𝑆)))))
Theorem	ellazim 49727*	Representation of an "extended integer". (Contributed by AV, 25-Oct-2026.)
⊢ ((𝑆 ∈ ℂ ∧ 𝐴 ∈ (Z[]l‘𝑆)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝐴 = (𝑎 + (𝑏 · 𝑆)))
Theorem	lazcn 49728	An extended integer is a complex number. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (𝐴 ∈ (Z[]l‘𝑆) → 𝐴 ∈ ℂ))
Theorem	zellaz 49729	An integer is an extended integer. (Contributed by AV, 24-Oct-2026.)
⊢ ((𝑆 ∈ ℂ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈ (Z[]l‘𝑆))
Theorem	lazssaz 49730	A linear adjunction of a complex number to the ring of integers is a subset of the adjunction of the complex number to the ring of integers. (Contributed by AV, 31-Oct-2026.)
⊢ (𝑆 ∈ ℂ → (Z[]l‘𝑆) ⊆ (Z[]‘𝑆))
Theorem	adcnmulzlaz 49731	The extended complex number multiplied with an integer is an extended integer. (Contributed by AV, 25-Oct-2026.)
⊢ ((𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ) → (𝐶 · 𝑆) ∈ (Z[]l‘𝑆))
Theorem	adcnellaz 49732	The adjoined complex number is an extended integer. (Contributed by AV, 25-Oct-2026.)
⊢ (𝑆 ∈ ℂ → 𝑆 ∈ (Z[]l‘𝑆))
Theorem	lazlinz 49733	Construct an extended integer. (Contributed by AV, 25-Oct-2026.)
⊢ (𝑆 ∈ ℂ → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (𝐵 · 𝑆)) ∈ (Z[]l‘𝑆)))
Theorem	adcnlaz 49734	The adjunction of an integer to the ring of integers yields the integers. (Contributed by AV, 25-Oct-2026.)
⊢ (𝑆 ∈ ℤ → (Z[]l‘𝑆) = ℤ)
Theorem	gzilaz 49735	The Gaussian integers are the adjunction of i to the ring of integers. (Contributed by AV, 25-Oct-2026.)
⊢ ℤ[i] = (Z[]l‘i)
Theorem	laznegcl 49736	The extended integers are closed under negation. (Contributed by AV, 25-Oct-2026.)
⊢ 𝑅 = (Z[]l‘𝑆)    ⇒   ⊢ (𝑆 ∈ ℂ → (𝐴 ∈ 𝑅 → -𝐴 ∈ 𝑅))
Theorem	lazmulzcl 49737	The extended integers are closed under multiplication with an integer. (Contributed by AV, 25-Oct-2026.)
⊢ 𝑅 = (Z[]l‘𝑆)    ⇒   ⊢ (𝑆 ∈ ℂ → ((𝐵 ∈ ℤ ∧ 𝐴 ∈ 𝑅) → (𝐵 · 𝐴) ∈ 𝑅))
Theorem	lazaddcl 49738	The extended integers are closed under addition. (Contributed by AV, 25-Oct-2026.)
⊢ 𝑅 = (Z[]l‘𝑆)    ⇒   ⊢ (𝑆 ∈ ℂ → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → (𝐴 + 𝐵) ∈ 𝑅))
Theorem	lazsubcl 49739	The extended integers are closed under subtraction. (Contributed by AV, 25-Oct-2026.)
⊢ 𝑅 = (Z[]l‘𝑆)    ⇒   ⊢ (𝑆 ∈ ℂ → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → (𝐴 − 𝐵) ∈ 𝑅))
Theorem	lazmulcl 49740	The extended integers are closed under multiplication if the square of the adjoined complex number is an extended integer. (Contributed by AV, 25-Oct-2026.)
⊢ 𝑅 = (Z[]l‘𝑆)    ⇒   ⊢ ((𝑆 ∈ ℂ ∧ (𝑆↑2) ∈ 𝑅) → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → (𝐴 · 𝐵) ∈ 𝑅))
Theorem	lazcjcl 49741	The extended integers are closed under conjugation if the conjugation of the adjoined complex number is an extended integer. (Contributed by AV, 26-Oct-2026.)
⊢ 𝑅 = (Z[]l‘𝑆)    ⇒   ⊢ ((𝑆 ∈ ℂ ∧ (∗‘𝑆) ∈ 𝑅) → (𝐴 ∈ 𝑅 → (∗‘𝐴) ∈ 𝑅))
Theorem	gzmulclALT 49742	The gaussian integers are closed under multiplication. Alternate (shorter) proof. (Contributed by AV, 25-Oct-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i])
21.52.18.10  Basic ` N ` -th root of unity
Syntax	cbru 49743	Extend class notation with the mapping yielding the basic 𝑁-th root of unity.
class bRoU
Definition	df-bru 49744	Define the mapping yielding the basic 𝑁-th root of unity. In cxpeq 27142, this is called "the primitive 𝑁-th root of unity with the smallest positive argument". (Contributed by AV, 24-Oct-2026.)
⊢ bRoU = (𝑛 ∈ ℕ ↦ (exp‘((2 · (π · i)) / 𝑛)))
Theorem	bruval 49745	The basic 𝑁-th root of unity. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑁 ∈ ℕ → (bRoU‘𝑁) = (exp‘((2 · (π · i)) / 𝑁)))
Theorem	brucn 49746	The basic 𝑁-th root of unity is a complex number. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑁 ∈ ℕ → (bRoU‘𝑁) ∈ ℂ)
Theorem	bruval2 49747	An alternate way to express the basic 𝑁-th root of unity, see cxpeq 27142. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑁 ∈ ℕ → (bRoU‘𝑁) = ( -1↑𝑐(2 / 𝑁)))
Theorem	bruval3 49748	An alternate way to express the basic 𝑁-th root of unity. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑁 ∈ ℕ → (bRoU‘𝑁) = ((cos‘((2 · π) / 𝑁)) + (i · (sin‘((2 · π) / 𝑁)))))
Theorem	bruvalexp 49749	The 𝑁-th power of the basic 𝑁-th root of unity is 1. (Contributed by AV, 24-Oct-2026.)
⊢ (𝑁 ∈ ℕ → ((bRoU‘𝑁)↑𝑁) = 1)
Theorem	bru1 49750	The basic (and only) 1st root of unity is 1. (Contributed by AV, 24-Oct-2026.)
⊢ (bRoU‘1) = 1
Theorem	bru2 49751	The basic 2nd root of unity is -1. (Contributed by AV, 24-Oct-2026.)
⊢ (bRoU‘2) = -1
Theorem	bru4 49752	The basic 4th root of unity is i. (Contributed by AV, 27-Oct-2026.)
⊢ (bRoU‘4) = i
Theorem	bru3val 49753	An alternate way to express the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026.)
⊢ 𝑊 = (bRoU‘3)    ⇒   ⊢ 𝑊 = (( -1 + (i · (√‘3))) / 2)
Theorem	bru3cj 49754	The complex conjugate of the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026.)
⊢ 𝑊 = (bRoU‘3)    ⇒   ⊢ (∗‘𝑊) = (𝑊↑2)
Theorem	bru3sq 49755	The square of the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026.)
⊢ 𝑊 = (bRoU‘3)    ⇒   ⊢ (𝑊↑2) = (( -1 / 2) − (i · ((√‘3) / 2)))
Theorem	bru3eq 49756	The basic 3rd root of unity ω satisfies the equation ω↑2 + ω + 1 = 0. (Contributed by AV, 24-Oct-2026.)
⊢ 𝑊 = (bRoU‘3)    ⇒   ⊢ (((𝑊↑2) + 𝑊) + 1) = 0
Theorem	bru3sqbru 49757	The square of the basic 3rd root of unity expressed by the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026.)
⊢ 𝑊 = (bRoU‘3)    ⇒   ⊢ (𝑊↑2) = ( -1 − 𝑊)
21.52.18.11  Eisenstein integers According to Wikipedia ("Eisenstein integer", 27-Oct-2026, https://en.wikipedia.org/wiki/Eisenstein_integer) "the Eisenstein integers (named after Gotthold Eisenstein) ... are the complex numbers of the form 𝑧 = 𝑎 + 𝑏ω where 𝑎 and 𝑏 are integers and ω is a primitive (hence non-real) cube root of unity." With the definitions of "Basic 𝑁-th root of unity" and "Adjunction of a complex number to the ring of integers", the set of Eisenstein integers can be denoted by (Z[]l‘(bRoU‘3)). Compare with the set of Gaussian integers ℤ[i] = (Z[]l‘i) = (Z[]l‘(bRoU‘4)), see df-gz 17152, gzilaz 49735 and bru4 49752. Hint (given by TA): It can be shown that (Z[]l‘ω) = (Z[]‘ω) with ω = (bRoU‘3), as well as ℤ[i] = (Z[]‘i) for the Gaussian integers, since ω↑2 = ω − 1 (see bru3sqbru 49757) and any ω term to a degree 2 or higher can be rewritten back into a linear polynomial, same for i and the Gaussian integers since i↑2 = -1 (see i2 14386).
Theorem	bru3sqez 49758	The square of the basic 3rd root of unity is an Eisenstein integer. (Contributed by AV, 26-Oct-2026.)
⊢ ((bRoU‘3)↑2) ∈ (Z[]l‘(bRoU‘3))
Theorem	ezsubrg 49759	The Eisenstein integers form a subring of the complex numbers. (Contributed by AV, 26-Oct-2026.)
⊢ (Z[]l‘(bRoU‘3)) ∈ (SubRing‘ℂfld)
Theorem	ezsscn 49760	The Eisenstein integers are a subset of the complex numbers. (Contributed by AV, 26-Oct-2026.)
⊢ (Z[]l‘(bRoU‘3)) ⊆ ℂ
Theorem	ezidom 49761	The Eisenstein integers form an integral domain. (Contributed by AV, 26-Oct-2026.)
⊢ (ℂfld ↾s (Z[]l‘(bRoU‘3))) ∈ IDomn
21.52.19  Prime rings (and integral domains) This section contains the definitions and theorems of section "Prime rings and integral domains" in JF's mathbox, transformed into extensible structures.
Syntax	cprmrng 49762	Extend class notation with the class of prime rings.
class PrmRing
Definition	df-prmring 49763	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.) (Revised by AV, 18-Jun-2026.)
⊢ PrmRing = {𝑟 ∈ Ring ∣ {(0g‘𝑟)} ∈ (PrmIdeal‘𝑟)}
Theorem	isprmrng 49764	The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by AV, 18-Jun-2026.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ PrmRing ↔ (𝑅 ∈ Ring ∧ { 0 } ∈ 𝑃))
Theorem	prmringnzring 49765	A prime ring is a nonzero ring. (Contributed by AV, 26-Jun-2026.)
⊢ (𝑅 ∈ PrmRing → 𝑅 ∈ NzRing)
Theorem	prmrngring 49766	A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by AV, 18-Jun-2026.) (Proof shortened by AV, 26-Jun-2026.)
⊢ (𝑅 ∈ PrmRing → 𝑅 ∈ Ring)
Theorem	smprngprmrng 49767	A simple ring (a nonzero ring whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised by AV, 18-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝑈 = {{ 0 }, 𝐵}) → 𝑅 ∈ PrmRing)
Theorem	drngprmrng 49768	A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised by AV, 18-Jun-2026.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ PrmRing)
Theorem	crngprmringidom 49769	A commutative ring is a prime ring if and only if it is an integral domain. (Contributed by AV, 27-Jun-2026.)
⊢ (𝑅 ∈ CRing → (𝑅 ∈ PrmRing ↔ 𝑅 ∈ IDomn))
Theorem	crngprmringdom 49770	A commutative ring is a prime ring if and only if it is a domain. (Contributed by AV, 27-Jun-2026.)
⊢ (𝑅 ∈ CRing → (𝑅 ∈ PrmRing ↔ 𝑅 ∈ Domn))
Theorem	dfidom2 49771	Alternate definition of the class of integral domains. An integral domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by AV, 27-Jun-2026.)
⊢ IDomn = (PrmRing ∩ CRing)
Theorem	isidom2 49772	The predicate "is an integral domain": An integral domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by AV, 27-Jun-2026.)
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ PrmRing ∧ 𝑅 ∈ CRing))
Theorem	isidom3 49773*	The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by AV, 12-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 ))))
Theorem	idomnzd 49774	A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by AV, 12-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ IDomn ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 · 𝑌) = 0 )) → (𝑋 = 0 ∨ 𝑌 = 0 ))
Theorem	idomcanl 49775	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised by AV, 13-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ IDomn ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋 ≠ 0 ) → ((𝑋 · 𝑌) = (𝑋 · 𝑍) → 𝑌 = 𝑍))
Theorem	idomcanr 49776	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised by AV, 13-Jul-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ IDomn ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑍 ≠ 0 ) → ((𝑋 · 𝑍) = (𝑌 · 𝑍) → 𝑋 = 𝑌))
21.52.20  Basic algebraic structures (extension)
21.52.20.1  Auxiliary theorems
Theorem	eliunxp2 49777*	Membership in a union of Cartesian products over its second component, analogous to eliunxp 5824. (Contributed by AV, 30-Mar-2019.)
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
Theorem	mpomptx2 49778*	Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐴(𝑦) is not assumed to be constant w.r.t 𝑦, analogous to mpomptx 7564. (Contributed by AV, 30-Mar-2019.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpox2 49779*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7545 allows 𝐴 to be a function of 𝑦, analogous to cbvmpox 7544. (Contributed by AV, 30-Mar-2019.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐷)    &   ⊢ ((𝑦 = 𝑧 ∧ 𝑥 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ 𝐷, 𝑧 ∈ 𝐵 ↦ 𝐸)
Theorem	dmmpossx2 49780*	The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpossx 8112. (Contributed by AV, 30-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦})
Theorem	mpoexxg2 49781*	Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpoexxg 8123. (Contributed by AV, 30-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐵 𝐴 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	ovmpordxf 49782*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7602. (Contributed by AV, 30-Mar-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑦𝑆    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpordx 49783*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7602. (Contributed by AV, 30-Mar-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpox2 49784*	The value of an operation class abstraction. Variant of ovmpoga 7606 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐿)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐿 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	fdmdifeqresdif 49785*	The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝑌, 𝑋, (𝐺‘𝑥)))    ⇒   ⊢ (𝐺:(𝐷 ∖ {𝑌})⟶𝑅 → 𝐺 = (𝐹 ↾ (𝐷 ∖ {𝑌})))
Theorem	ofaddmndmap 49786	The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f + 𝐵) ∈ (𝑅 ↑m 𝑉))
Theorem	mapsnop 49787	A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐹 = {⟨𝑋, 𝑌⟩}    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊) → 𝐹 ∈ (𝑅 ↑m {𝑋}))
Theorem	fprmappr 49788	A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024.)
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ∈ (𝑋 ↑m {𝐴, 𝐵}))
Theorem	mapprop 49789	An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.) (Proof shortened by AV, 2-Jun-2024.)
⊢ 𝐹 = {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩}    ⇒   ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹 ∈ (𝑅 ↑m {𝑋, 𝑌}))
Theorem	ztprmneprm 49790	A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.)
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵))
Theorem	2t6m3t4e0 49791	2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.)
⊢ ((2 · 6) − (3 · 4)) = 0
Theorem	ssnn0ssfz 49792*	For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 33475. (Contributed by AV, 30-Sep-2019.)
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛))
Theorem	nn0sumltlt 49793	If the sum of two nonnegative integers is less than a third integer, then one of the summands is already less than this third integer. (Contributed by AV, 19-Oct-2019.)
⊢ ((𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑐 → 𝑏 < 𝑐))
21.52.20.2  The binomial coefficient operation (extension)
Theorem	bcpascm1 49794	Pascal's rule for the binomial coefficient, generalized to all integers 𝐾, shifted down by 1. (Contributed by AV, 8-Sep-2019.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (((𝑁 − 1)C𝐾) + ((𝑁 − 1)C(𝐾 − 1))) = (𝑁C𝐾))
Theorem	altgsumbc 49795*	The sum of binomial coefficients for a fixed positive 𝑁 with alternating signs is zero. Notice that this is not valid for 𝑁 = 0 (since (( -1↑0) · (0C0)) = (1 · 1) = 1). For a proof using Pascal's rule (bcpascm1 49794) instead of the binomial theorem (binom 16043), see altgsumbcALT 49796. (Contributed by AV, 13-Sep-2019.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) · (𝑁C𝑘)) = 0)
Theorem	altgsumbcALT 49796*	Alternate proof of altgsumbc 49795, using Pascal's rule (bcpascm1 49794) instead of the binomial theorem (binom 16043). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) · (𝑁C𝑘)) = 0)
21.52.20.3  The ` ZZ `-module ` ZZ X. ZZ `
Theorem	zlmodzxzlmod 49797	The ℤ-module ℤ × ℤ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    ⇒   ⊢ (𝑍 ∈ LMod ∧ ℤring = (Scalar‘𝑍))
Theorem	zlmodzxzel 49798	An element of the (base set of the) ℤ-module ℤ × ℤ. (Contributed by AV, 21-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∈ (Base‘𝑍))
Theorem	zlmodzxz0 49799	The 0 of the ℤ-module ℤ × ℤ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    ⇒   ⊢ 0 = (0g‘𝑍)
Theorem	zlmodzxzscm 49800	The scalar multiplication of the ℤ-module ℤ × ℤ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {⟨0, 𝐵⟩, ⟨1, 𝐶⟩}) = {⟨0, (𝐴 · 𝐵)⟩, ⟨1, (𝐴 · 𝐶)⟩})