P. 148 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isridl 14701*	A right ideal is a left ideal of the opposite ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑦 · 𝑥) ∈ 𝐼)))
Theorem	2idlelb 14702	Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ (𝑈 ∈ 𝑇 ↔ (𝑈 ∈ 𝐼 ∧ 𝑈 ∈ 𝐽))
Theorem	2idllidld 14703	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
Theorem	2idlridld 14704	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂))
Theorem	df2idl2rng 14705*	Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
⊢ 𝑈 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrp‘𝑅)) → (𝐼 ∈ 𝑈 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼)))
Theorem	df2idl2 14706*	Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
⊢ 𝑈 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼))))
Theorem	ridl0 14707	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	ridl1 14708	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	2idl0 14709	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝐼)
Theorem	2idl1 14710	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝐼)
Theorem	2idlss 14711	A two-sided ideal is a subset of the base set. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (2Ideal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	2idlbas 14712	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐼)
Theorem	2idlelbas 14713	The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → (𝐵 ∈ (LIdeal‘𝑅) ∧ 𝐵 ∈ (LIdeal‘(oppr‘𝑅))))
Theorem	rng2idlsubrng 14714	A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅))
Theorem	rng2idlnsg 14715	A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))
Theorem	rng2idl0 14716	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng)    ⇒   ⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼)
Theorem	rng2idlsubgsubrng 14717	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅))
Theorem	rng2idlsubgnsg 14718	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))
Theorem	rng2idlsubg0 14719	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅))    ⇒   ⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼)
Theorem	2idlcpblrng 14720	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝑅 ~QG 𝑆)    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
Theorem	2idlcpbl 14721	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝑅 ~QG 𝑆)    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
Theorem	qus2idrng 14722	The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 14724 analog). (Contributed by AV, 23-Feb-2025.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → 𝑈 ∈ Rng)
Theorem	qus1 14723	The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → (𝑈 ∈ Ring ∧ [ 1 ](𝑅 ~QG 𝑆) = (1r‘𝑈)))
Theorem	qusring 14724	If 𝑆 is a two-sided ideal in 𝑅, then 𝑈 = 𝑅 / 𝑆 is a ring, called the quotient ring of 𝑅 by 𝑆. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ Ring)
Theorem	qusrhm 14725*	If 𝑆 is a two-sided ideal in 𝑅, then the "natural map" from elements to their cosets is a ring homomorphism from 𝑅 to 𝑅 / 𝑆. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝑅 ~QG 𝑆))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑈))
Theorem	qusmul2 14726	Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝑄)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ([𝑋](𝑅 ~QG 𝐼) × [𝑌](𝑅 ~QG 𝐼)) = [(𝑋 · 𝑌)](𝑅 ~QG 𝐼))
Theorem	crngridl 14727	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂))
Theorem	crng2idl 14728	In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (2Ideal‘𝑅))
Theorem	qusmulrng 14729	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14730. Similar to qusmul2 14726. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
⊢ ∼ = (𝑅 ~QG 𝑆)    &   ⊢ 𝐻 = (𝑅 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝐻)    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝑆 ∈ (2Ideal‘𝑅) ∧ 𝑆 ∈ (SubGrp‘𝑅)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	quscrng 14730	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ CRing)
7.6.4  Principal ideal rings. Divisibility in the integers
Theorem	rspsn 14731*	Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐾‘{𝐺}) = {𝑥 ∣ 𝐺 ∥ 𝑥})
7.7  The complex numbers as an algebraic extensible structure
7.7.1  Definition and basic properties
Syntax	cpsmet 14732	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 14733	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 14734	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 14735	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 14736	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 14737	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 14738	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 14739	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 14740*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-xmet 14741*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 14742, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-met 14742*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.)
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
Definition	df-bl 14743*	Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
Definition	df-mopn 14744	Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.)
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
Definition	df-fbas 14745*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})
Definition	df-fg 14746*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
Definition	df-metu 14747*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))
Theorem	blfn 14748	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
⊢ ball Fn V
Theorem	mopnset 14749	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
⊢ (𝐷 ∈ 𝑉 → (MetOpen‘𝐷) ∈ V)
Theorem	cndsex 14750	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
⊢ (abs ∘ − ) ∈ V
Theorem	cntopex 14751	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
⊢ (MetOpen‘(abs ∘ − )) ∈ V
Theorem	metuex 14752	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
⊢ (𝐴 ∈ 𝑉 → (metUnif‘𝐴) ∈ V)
Syntax	ccnfld 14753	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 14754*	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator. The contract of this set is defined entirely by cnfldex 14756, cnfldadd 14759, cnfldmul 14761, cnfldcj 14762, cnfldtset 14763, cnfldle 14764, cnfldds 14765, and cnfldbas 14757. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)
⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
Theorem	cnfldstr 14755	The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
⊢ ℂfld Struct ⟨1, ;13⟩
Theorem	cnfldex 14756	The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
⊢ ℂfld ∈ V
Theorem	cnfldbas 14757	The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
⊢ ℂ = (Base‘ℂfld)
Theorem	mpocnfldadd 14758*	The addition operation of the field of complex numbers. Version of cnfldadd 14759 using maps-to notation, which does not require ax-addf 8254. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld)
Theorem	cnfldadd 14759	The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
⊢ + = (+g‘ℂfld)
Theorem	mpocnfldmul 14760*	The multiplication operation of the field of complex numbers. Version of cnfldmul 14761 using maps-to notation, which does not require ax-mulf 8255. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld)
Theorem	cnfldmul 14761	The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
⊢ · = (.r‘ℂfld)
Theorem	cnfldcj 14762	The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.)
⊢ ∗ = (*𝑟‘ℂfld)
Theorem	cnfldtset 14763	The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 31-Mar-2025.)
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld)
Theorem	cnfldle 14764	The ordering of the field of complex numbers. Note that this is not actually an ordering on ℂ, but we put it in the structure anyway because restricting to ℝ does not affect this component, so that (ℂfld ↾s ℝ) is an ordered field even though ℂfld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14754. (Revised by GG, 31-Mar-2025.)
⊢ ≤ = (le‘ℂfld)
Theorem	cnfldds 14765	The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14754. (Revised by GG, 31-Mar-2025.)
⊢ (abs ∘ − ) = (dist‘ℂfld)
Theorem	cncrng 14766	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
⊢ ℂfld ∈ CRing
Theorem	cnring 14767	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ Ring
Theorem	cnfld0 14768	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 0 = (0g‘ℂfld)
Theorem	cnfld1 14769	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘ℂfld)
Theorem	cnfldneg 14770	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋)
Theorem	cnfldplusf 14771	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ + = (+𝑓‘ℂfld)
Theorem	cnfldsub 14772	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘ℂfld)
Theorem	cnfldmulg 14773	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))
Theorem	cnfldexp 14774	The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐵(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑𝐵))
Theorem	cnsubmlem 14775*	Lemma for nn0subm 14780 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ 0 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubMnd‘ℂfld)
Theorem	cnsubglem 14776*	Lemma for cnsubrglem 14777 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 𝐵 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubGrp‘ℂfld)
Theorem	cnsubrglem 14777*	Lemma for zsubrg 14778 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubRing‘ℂfld)
Theorem	zsubrg 14778	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ ∈ (SubRing‘ℂfld)
Theorem	gzsubrg 14779	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ[i] ∈ (SubRing‘ℂfld)
Theorem	nn0subm 14780	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ℕ0 ∈ (SubMnd‘ℂfld)
Theorem	rege0subm 14781	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
Theorem	zsssubrg 14782	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅)
Theorem	gsumfzfsumlem0 14783*	Lemma for gsumfzfsum 14785. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 < 𝑀)    ⇒   ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
Theorem	gsumfzfsumlemm 14784*	Lemma for gsumfzfsum 14785. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
Theorem	gsumfzfsum 14785*	Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
Theorem	cnfldui 14786	The invertible complex numbers are exactly those apart from zero. This is recapb 8950 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} = (Unit‘ℂfld)
7.7.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 14790 it is shown that this restriction is a ring, and zringbas 14793 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 14788 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) 14788).
Syntax	czring 14787	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 14788	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
⊢ ℤring = (ℂfld ↾s ℤ)
Theorem	zringcrng 14789	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ CRing
Theorem	zringring 14790	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	zringabl 14791	The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ Abel
Theorem	zringgrp 14792	The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.)
⊢ ℤring ∈ Grp
Theorem	zringbas 14793	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 14794	The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.)
⊢ + = (+g‘ℤring)
Theorem	zringmulg 14795	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 14796	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 14797	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 14798	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 14799	The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.)
⊢ ℤring ∈ NzRing
Theorem	dvdsrzring 14800	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)