P. 141 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14001-14100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sratsetg 14001	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (TopSet‘𝑊) = (TopSet‘𝐴))
Theorem	sraex 14002	Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	sratopng 14003	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (TopOpen‘𝑊) = (TopOpen‘𝐴))
Theorem	sradsg 14004	Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (dist‘𝑊) = (dist‘𝐴))
Theorem	sraring 14005	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring)
Theorem	sralmod 14006	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    ⇒   ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod)
Theorem	sralmod0g 14007	The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 0 = (0g‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝐴))
Theorem	issubrgd 14008*	Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 1 = (1r‘𝐼))    &   ⊢ (𝜑 → · = (.r‘𝐼))    &   ⊢ (𝜑 → 1 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 · 𝑦) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (SubRing‘𝐼))
Theorem	rlmfn 14009	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod Fn V
Theorem	rlmvalg 14010	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (𝑊 ∈ 𝑉 → (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊)))
Theorem	rlmbasg 14011	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑅) = (Base‘(ringLMod‘𝑅)))
Theorem	rlmplusgg 14012	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (𝑅 ∈ 𝑉 → (+g‘𝑅) = (+g‘(ringLMod‘𝑅)))
Theorem	rlm0g 14013	Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (𝑅 ∈ 𝑉 → (0g‘𝑅) = (0g‘(ringLMod‘𝑅)))
Theorem	rlmsubg 14014	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (𝑅 ∈ 𝑉 → (-g‘𝑅) = (-g‘(ringLMod‘𝑅)))
Theorem	rlmmulrg 14015	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑅) = (.r‘(ringLMod‘𝑅)))
Theorem	rlmscabas 14016	Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
⊢ (𝑅 ∈ 𝑋 → (Base‘𝑅) = (Base‘(Scalar‘(ringLMod‘𝑅))))
Theorem	rlmvscag 14017	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅)))
Theorem	rlmtopng 14018	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑅 ∈ 𝑉 → (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅)))
Theorem	rlmdsg 14019	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑅 ∈ 𝑉 → (dist‘𝑅) = (dist‘(ringLMod‘𝑅)))
Theorem	rlmlmod 14020	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod)
Theorem	rlmvnegg 14021	Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
⊢ (𝑅 ∈ 𝑉 → (invg‘𝑅) = (invg‘(ringLMod‘𝑅)))
Theorem	ixpsnbasval 14022*	The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))})
7.6.2  Ideals and spans
Syntax	clidl 14023	Ring left-ideal function.
class LIdeal
Syntax	crsp 14024	Ring span function.
class RSpan
Definition	df-lidl 14025	Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ LIdeal = (LSubSp ∘ ringLMod)
Definition	df-rsp 14026	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ RSpan = (LSpan ∘ ringLMod)
Theorem	lidlvalg 14027	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (𝑊 ∈ 𝑉 → (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊)))
Theorem	rspvalg 14028	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (𝑊 ∈ 𝑉 → (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊)))
Theorem	lidlex 14029	Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
⊢ (𝑊 ∈ 𝑉 → (LIdeal‘𝑊) ∈ V)
Theorem	rspex 14030	Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
⊢ (𝑊 ∈ 𝑉 → (RSpan‘𝑊) ∈ V)
Theorem	lidlmex 14031	Existence of the set a left ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑊 ∈ V)
Theorem	lidlss 14032	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	lidlssbas 14033	The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅))
Theorem	lidlbas 14034	A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈)
Theorem	islidlm 14035*	Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ ∃𝑗 𝑗 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼))
Theorem	rnglidlmcl 14036	A (left) ideal containing the zero element is closed under left-multiplication by elements of the full non-unital ring. If the ring is not a unital ring, and the ideal does not contain the zero element of the ring, then the closure cannot be proven. (Contributed by AV, 18-Feb-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼)) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	dflidl2rng 14037*	Alternate (the usual textbook) definition of a (left) ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrp‘𝑅)) → (𝐼 ∈ 𝑈 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑥 · 𝑦) ∈ 𝐼))
Theorem	isridlrng 14038*	A right ideal is a left ideal of the opposite non-unital 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, 21-Mar-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrp‘𝑅)) → (𝐼 ∈ 𝑈 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑦 · 𝑥) ∈ 𝐼))
Theorem	lidl0cl 14039	An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼)
Theorem	lidlacl 14040	An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼)
Theorem	lidlnegcl 14041	An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼)
Theorem	lidlsubg 14042	An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅))
Theorem	lidlsubcl 14043	An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 − 𝑌) ∈ 𝐼)
Theorem	dflidl2 14044*	Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑥 · 𝑦) ∈ 𝐼)))
Theorem	lidl0 14045	Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	lidl1 14046	Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	rspcl 14047	The span of a set of ring elements is an ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ 𝑈)
Theorem	rspssid 14048	The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺))
Theorem	rsp0 14049	The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐾‘{ 0 }) = { 0 })
Theorem	rspssp 14050	The ideal span of a set of elements in a ring is contained in any subring which contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ⊆ 𝐼) → (𝐾‘𝐺) ⊆ 𝐼)
Theorem	lidlrsppropdg 14051*	The left ideals and ring span of a ring depend only on the ring components. Here 𝑊 is expected to be either 𝐵 (when closure is available) or V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((LIdeal‘𝐾) = (LIdeal‘𝐿) ∧ (RSpan‘𝐾) = (RSpan‘𝐿)))
Theorem	rnglidlmmgm 14052	The multiplicative group of a (left) ideal of a non-unital ring is a magma. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption 0 ∈ 𝑈 is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (mulGrp‘𝐼) ∈ Mgm)
Theorem	rnglidlmsgrp 14053	The multiplicative group of a (left) ideal of a non-unital ring is a semigroup. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption 0 ∈ 𝑈 is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈) → (mulGrp‘𝐼) ∈ Smgrp)
Theorem	rnglidlrng 14054	A (left) ideal of a non-unital ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption 𝑈 ∈ (SubGrp‘𝑅) is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
⊢ 𝐿 = (LIdeal‘𝑅)    &   ⊢ 𝐼 = (𝑅 ↾s 𝑈)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (SubGrp‘𝑅)) → 𝐼 ∈ Rng)
7.6.3  Two-sided ideals and quotient rings
Syntax	c2idl 14055	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 14056	Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟))))
Theorem	2idlmex 14057	Existence of the set a two-sided ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
⊢ 𝑇 = (2Ideal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝑇 → 𝑊 ∈ V)
Theorem	2idlval 14058	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ 𝑇 = (𝐼 ∩ 𝐽)
Theorem	2idlvalg 14059	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑇 = (𝐼 ∩ 𝐽))
Theorem	isridl 14060*	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 14061	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 14062	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
Theorem	2idlridld 14063	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂))
Theorem	df2idl2rng 14064*	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 14065*	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 14066	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	ridl1 14067	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	2idl0 14068	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝐼)
Theorem	2idl1 14069	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝐼)
Theorem	2idlss 14070	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 14071	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐼)
Theorem	2idlelbas 14072	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 14073	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 14074	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 14075	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 14076	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 14077	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 14078	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 14079	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 14080	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 14081	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 14083 analog). (Contributed by AV, 23-Feb-2025.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (2Ideal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → 𝑈 ∈ Rng)
Theorem	qus1 14082	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 14083	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 14084*	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 14085	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 14086	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂))
Theorem	crng2idl 14087	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 14088	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14089. Similar to qusmul2 14085. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
⊢ ∼ = (𝑅 ~QG 𝑆)    &   ⊢ 𝐻 = (𝑅 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝐻)    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝑆 ∈ (2Ideal‘𝑅) ∧ 𝑆 ∈ (SubGrp‘𝑅)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ )
Theorem	quscrng 14089	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 14090*	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 14091	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 14092	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 14093	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 14094	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 14095	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 14096	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 14097	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 14098	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 14099*	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 14100*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 14101, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})