P. 215 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21401-21500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gzsubrg 21401	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ[i] ∈ (SubRing‘ℂfld)
Theorem	nn0subm 21402	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ℕ0 ∈ (SubMnd‘ℂfld)
Theorem	rege0subm 21403	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
Theorem	absabv 21404	The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ abs ∈ (AbsVal‘ℂfld)
Theorem	zsssubrg 21405	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅)
Theorem	qsssubdrg 21406	The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝑅) ∈ DivRing) → ℚ ⊆ 𝑅)
Theorem	cnsubrg 21407	There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ})
Theorem	cnmgpabl 21408	The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ 𝑀 ∈ Abel
Theorem	cnmgpid 21409	The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by AV, 26-Aug-2021.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ (0g‘𝑀) = 1
Theorem	cnmsubglem 21410*	Lemma for rpmsubg 21411 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubGrp‘𝑀)
Theorem	rpmsubg 21411	The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ ℝ+ ∈ (SubGrp‘𝑀)
Theorem	gzrngunitlem 21412	Lemma for gzrngunit 21413. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴))
Theorem	gzrngunit 21413	The units on ℤ[i] are the gaussian integers with norm 1. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑍 = (ℂfld ↾s ℤ[i])    ⇒   ⊢ (𝐴 ∈ (Unit‘𝑍) ↔ (𝐴 ∈ ℤ[i] ∧ (abs‘𝐴) = 1))
Theorem	gsumfsum 21414*	Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	regsumfsum 21415*	Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 21414. (Contributed by Thierry Arnoux, 7-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)
Theorem	expmhm 21416*	Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑁 = (ℂfld ↾s ℕ0)    &   ⊢ 𝑀 = (mulGrp‘ℂfld)    ⇒   ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀))
Theorem	nn0srg 21417	The nonnegative integers form a semiring (commutative by subcmn 19812). (Contributed by Thierry Arnoux, 1-May-2018.)
⊢ (ℂfld ↾s ℕ0) ∈ SRing
Theorem	rge0srg 21418	The nonnegative real numbers form a semiring (commutative by subcmn 19812). (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ (ℂfld ↾s (0[,)+∞)) ∈ SRing
Theorem	xrge0plusg 21419	The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ +𝑒 = (+g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrs1mnd 21420	The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 21389. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	xrs10 21421	The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	xrs1cmn 21422	The extended real numbers restricted to ℝ* ∖ {-∞} form a commutative monoid. They are not a group because 1 + +∞ = 2 + +∞ even though 1 ≠ 2. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 𝑅 ∈ CMnd
Theorem	xrge0subm 21423	The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ (0[,]+∞) ∈ (SubMnd‘𝑅)
Theorem	xrge0cmn 21424	The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
Theorem	xrge0omnd 21425	The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd
10.8.2  Ring of integers According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring 𝑍." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (ℂfld ↾s ℤ), the field of complex numbers restricted to the integers. In zringring 21429 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 21447), and zringbas 21433 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 21427 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to ℂfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra) 21427).
Syntax	czring 21426	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 21427	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
⊢ ℤring = (ℂfld ↾s ℤ)
Theorem	zringcrng 21428	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ CRing
Theorem	zringring 21429	The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.)
⊢ ℤring ∈ Ring
Theorem	zringrng 21430	The ring of integers is a non-unital ring. (Contributed by AV, 17-Mar-2025.)
⊢ ℤring ∈ Rng
Theorem	zringabl 21431	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 21432	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 21433	The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
⊢ ℤ = (Base‘ℤring)
Theorem	zringplusg 21434	The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ + = (+g‘ℤring)
Theorem	zringsub 21435	The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmulg 21436	The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴(.g‘ℤring)𝐵) = (𝐴 · 𝐵))
Theorem	zringmulr 21437	The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ · = (.r‘ℤring)
Theorem	zring0 21438	The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 0 = (0g‘ℤring)
Theorem	zring1 21439	The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ 1 = (1r‘ℤring)
Theorem	zringnzr 21440	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 21441	Ring divisibility in the ring of integers corresponds to ordinary divisibility in ℤ. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
⊢ ∥ = (∥r‘ℤring)
Theorem	zringlpirlem1 21442	Lemma for zringlpir 21447. A nonzero ideal of integers contains some positive integers. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))    &   ⊢ (𝜑 → 𝐼 ≠ {0})    ⇒   ⊢ (𝜑 → (𝐼 ∩ ℕ) ≠ ∅)
Theorem	zringlpirlem2 21443	Lemma for zringlpir 21447. A nonzero ideal of integers contains the least positive element. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Revised by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))    &   ⊢ (𝜑 → 𝐼 ≠ {0})    &   ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐼)
Theorem	zringlpirlem3 21444	Lemma for zringlpir 21447. All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))    &   ⊢ (𝜑 → 𝐼 ≠ {0})    &   ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝐺 ∥ 𝑋)
Theorem	zringinvg 21445	The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ (𝐴 ∈ ℤ → -𝐴 = ((invg‘ℤring)‘𝐴))
Theorem	zringunit 21446	The units of ℤ are the integers with norm 1, i.e. 1 and -1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1))
Theorem	zringlpir 21447	The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.)
⊢ ℤring ∈ LPIR
Theorem	zringndrg 21448	The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.)
⊢ ℤring ∉ DivRing
Theorem	zringcyg 21449	The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.)
⊢ ℤring ∈ CycGrp
Theorem	zringsubgval 21450	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
⊢ − = (-g‘ℤring)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	zringmpg 21451	The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.)
⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring)
Theorem	prmirredlem 21452	A positive integer is irreducible over ℤ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ 𝐼 = (Irred‘ℤring)    ⇒   ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ))
Theorem	dfprm2 21453	The positive irreducible elements of ℤ are the prime numbers. This is an alternative way to define ℙ. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ 𝐼 = (Irred‘ℤring)    ⇒   ⊢ ℙ = (ℕ ∩ 𝐼)
Theorem	prmirred 21454	The irreducible elements of ℤ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
⊢ 𝐼 = (Irred‘ℤring)    ⇒   ⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ))
Theorem	expghm 21455*	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ 𝑈 = (𝑀 ↾s (ℂ ∖ {0}))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈))
Theorem	mulgghm2 21456*	The powers of a group element give a homomorphism from ℤ to a group. The name 1 should not be taken as a constraint as it may be any group element. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅))
Theorem	mulgrhm 21457*	The powers of the element 1 give a ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring RingHom 𝑅))
Theorem	mulgrhm2 21458*	The powers of the element 1 give the unique ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ · = (.g‘𝑅)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (ℤring RingHom 𝑅) = {𝐹})
Theorem	irinitoringc 21459	The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ℤring ∈ 𝑈)    &   ⊢ 𝐶 = (RingCat‘𝑈)    ⇒   ⊢ (𝜑 → ℤring ∈ (InitO‘𝐶))
Theorem	nzerooringczr 21460	There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → ℤring ∈ 𝑈)    ⇒   ⊢ (𝜑 → (ZeroO‘𝐶) = ∅)
10.8.2.1  Example for a condition for a non-unital ring to be unital In this subsubsection, an example is given for a condition for a non-unital ring to be unital. This example is already mentioned in the comment for df-subrg 20547: " The subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity ⟨1, 0⟩ which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring." The theorems in this subsubsection do not assume that 𝑅 = (ℤring ×s ℤring) is a ring (which can be proven directly very easily, see pzriprng 21477), but provide the prerequisites for ring2idlqusb 21308 to show that 𝑅 is a unital ring, and for ring2idlqus1 21317 to show that ⟨1, 1⟩ is its ring unity.
Theorem	pzriprnglem1 21461	Lemma 1 for pzriprng 21477: 𝑅 is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    ⇒   ⊢ 𝑅 ∈ Rng
Theorem	pzriprnglem2 21462	Lemma 2 for pzriprng 21477: The base set of 𝑅 is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    ⇒   ⊢ (Base‘𝑅) = (ℤ × ℤ)
Theorem	pzriprnglem3 21463*	Lemma 3 for pzriprng 21477: An element of 𝐼 is an ordered pair. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑥 ∈ ℤ 𝑋 = ⟨𝑥, 0⟩)
Theorem	pzriprnglem4 21464	Lemma 4 for pzriprng 21477: 𝐼 is a subgroup of 𝑅. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ 𝐼 ∈ (SubGrp‘𝑅)
Theorem	pzriprnglem5 21465	Lemma 5 for pzriprng 21477: 𝐼 is a subring of the non-unital ring 𝑅. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    ⇒   ⊢ 𝐼 ∈ (SubRng‘𝑅)
Theorem	pzriprnglem6 21466	Lemma 6 for pzriprng 21477: 𝐽 has a ring unity. (Contributed by AV, 19-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ (𝑋 ∈ 𝐼 → ((⟨1, 0⟩(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)⟨1, 0⟩) = 𝑋))
Theorem	pzriprnglem7 21467	Lemma 7 for pzriprng 21477: 𝐽 is a unital ring. (Contributed by AV, 19-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ 𝐽 ∈ Ring
Theorem	pzriprnglem8 21468	Lemma 8 for pzriprng 21477: 𝐼 resp. 𝐽 is a two-sided ideal of the non-unital ring 𝑅. (Contributed by AV, 21-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    ⇒   ⊢ 𝐼 ∈ (2Ideal‘𝑅)
Theorem	pzriprnglem9 21469	Lemma 9 for pzriprng 21477: The ring unity of the ring 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    ⇒   ⊢ 1 = ⟨1, 0⟩
Theorem	pzriprnglem10 21470	Lemma 10 for pzriprng 21477: The equivalence classes of 𝑅 modulo 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    ⇒   ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → [⟨𝑋, 𝑌⟩] ∼ = (ℤ × {𝑌}))
Theorem	pzriprnglem11 21471*	Lemma 11 for pzriprng 21477: The base set of the quotient of 𝑅 and 𝐽. (Contributed by AV, 22-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ (Base‘𝑄) = ∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})}
Theorem	pzriprnglem12 21472	Lemma 12 for pzriprng 21477: 𝑄 has a ring unity. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ (𝑋 ∈ (Base‘𝑄) → (((ℤ × {1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋))
Theorem	pzriprnglem13 21473	Lemma 13 for pzriprng 21477: 𝑄 is a unital ring. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ 𝑄 ∈ Ring
Theorem	pzriprnglem14 21474	Lemma 14 for pzriprng 21477: The ring unity of the ring 𝑄. (Contributed by AV, 23-Mar-2025.)
⊢ 𝑅 = (ℤring ×s ℤring)    &   ⊢ 𝐼 = (ℤ × {0})    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 1 = (1r‘𝐽)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ (1r‘𝑄) = (ℤ × {1})
Theorem	pzriprngALT 21475	The non-unital ring (ℤring ×s ℤring) is unital because it has the two-sided ideal (ℤ × {0}), which is unital, and the quotient of the ring and the ideal is also unital (using ring2idlqusb 21308). (Contributed by AV, 23-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ℤring ×s ℤring) ∈ Ring
Theorem	pzriprng1ALT 21476	The ring unity of the ring (ℤring ×s ℤring) constructed from the ring unity of the two-sided ideal (ℤ × {0}) and the ring unity of the quotient of the ring and the ideal (using ring2idlqus1 21317). (Contributed by AV, 24-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1r‘(ℤring ×s ℤring)) = ⟨1, 1⟩
Theorem	pzriprng 21477	The non-unital ring (ℤring ×s ℤring) is unital. Direct proof in contrast to pzriprngALT 21475. (Contributed by AV, 25-Mar-2025.)
⊢ (ℤring ×s ℤring) ∈ Ring
Theorem	pzriprng1 21478	The ring unity of the ring (ℤring ×s ℤring). Direct proof in contrast to pzriprng1ALT 21476. (Contributed by AV, 25-Mar-2025.)
⊢ (1r‘(ℤring ×s ℤring)) = ⟨1, 1⟩
10.8.3  Algebraic constructions based on the complex numbers
Syntax	czrh 21479	Map the rationals into a field, or the integers into a ring.
class ℤRHom
Syntax	czlm 21480	Augment an abelian group with vector space operations to turn it into a ℤ-module.
class ℤMod
Syntax	cchr 21481	Syntax for ring characteristic.
class chr
Syntax	czn 21482	The ring of integers modulo 𝑛.
class ℤ/nℤ
Definition	df-zrh 21483	Define the unique homomorphism from the integers into a ring. This encodes the usual notation of 𝑛 = 1r + 1r + ... + 1r for integers (see also df-mulg 19044). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟))
Definition	df-zlm 21484	Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩))
Definition	df-chr 21485	The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ chr = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔)))
Definition	df-zn 21486*	Define the ring of integers mod 𝑛. This is literally the quotient ring of ℤ by the ideal 𝑛ℤ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet ⟨(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)⟩))
Theorem	zrhval 21487	Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ 𝐿 = ∪ (ℤring RingHom 𝑅)
Theorem	zrhval2 21488*	Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )))
Theorem	zrhmulg 21489	Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 ))
Theorem	zrhrhmb 21490	The ℤRHom homomorphism is the unique ring homomorphism from ℤ. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐹 ∈ (ℤring RingHom 𝑅) ↔ 𝐹 = 𝐿))
Theorem	zrhrhm 21491	The ℤRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
Theorem	zrh1 21492	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 )
Theorem	zrh0 21493	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 )
Theorem	zrhpropd 21494*	The ℤ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (ℤRHom‘𝐾) = (ℤRHom‘𝐿))
Theorem	zlmval 21495	Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
Theorem	zlmlem 21496	Lemma for zlmbas 21497 and zlmplusg 21498. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx)    &   ⊢ (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx)    ⇒   ⊢ (𝐸‘𝐺) = (𝐸‘𝑊)
Theorem	zlmbas 21497	Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (Base‘𝑊)
Theorem	zlmplusg 21498	Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (+g‘𝑊)
Theorem	zlmmulr 21499	Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ · = (.r‘𝑊)
Theorem	zlmsca 21500	Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊))