P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sravscaOLD 20801	Obsolete proof of sravsca 20800 as of 12-Nov-2024. The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = ( ·𝑠 ‘𝐴))
Theorem	sraip 20802	The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (·𝑖‘𝐴))
Theorem	sratset 20803	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	sratsetOLD 20804	Obsolete proof of sratset 20803 as of 29-Oct-2024. Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (TopSet‘𝑊) = (TopSet‘𝐴))
Theorem	sratopn 20805	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	srads 20806	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	sradsOLD 20807	Obsolete proof of srads 20806 as of 29-Oct-2024. Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (dist‘𝑊) = (dist‘𝐴))
Theorem	sraring 20808	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring)
Theorem	sralmod 20809	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    ⇒   ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod)
Theorem	sralmod0 20810	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 20811*	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 20812	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod Fn V
Theorem	rlmval 20813	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))
Theorem	lidlval 20814	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))
Theorem	rspval 20815	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊))
Theorem	rlmval2 20816	Value of the ring module extended. (Contributed by AV, 2-Dec-2018.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝑊 ∈ 𝑋 → (ringLMod‘𝑊) = (((𝑊 sSet ⟨(Scalar‘ndx), 𝑊⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑊)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑊)⟩))
Theorem	rlmbas 20817	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (Base‘𝑅) = (Base‘(ringLMod‘𝑅))
Theorem	rlmplusg 20818	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (+g‘𝑅) = (+g‘(ringLMod‘𝑅))
Theorem	rlm0 20819	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	rlmsub 20820	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (-g‘𝑅) = (-g‘(ringLMod‘𝑅))
Theorem	rlmmulr 20821	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (.r‘𝑅) = (.r‘(ringLMod‘𝑅))
Theorem	rlmsca 20822	Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ 𝑋 → 𝑅 = (Scalar‘(ringLMod‘𝑅)))
Theorem	rlmsca2 20823	Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅))
Theorem	rlmvsca 20824	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅))
Theorem	rlmtopn 20825	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅))
Theorem	rlmds 20826	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (dist‘𝑅) = (dist‘(ringLMod‘𝑅))
Theorem	rlmlmod 20827	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod)
Theorem	rlmlvec 20828	The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ DivRing → (ringLMod‘𝑅) ∈ LVec)
Theorem	rlmlsm 20829	Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024.)
⊢ (𝑅 ∈ 𝑉 → (LSSum‘𝑅) = (LSSum‘(ringLMod‘𝑅)))
Theorem	rlmvneg 20830	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	rlmscaf 20831	Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (+𝑓‘(mulGrp‘𝑅)) = ( ·sf ‘(ringLMod‘𝑅))
Theorem	ixpsnbasval 20832*	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‘𝑅))})
Theorem	lidlss 20833	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	islidl 20834*	Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼))
Theorem	lidl0cl 20835	An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼)
Theorem	lidlacl 20836	An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼)
Theorem	lidlnegcl 20837	An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼)
Theorem	lidlsubg 20838	An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅))
Theorem	lidlsubcl 20839	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	lidlmcl 20840	An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼)) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	lidl1el 20841	An ideal contains 1 iff it is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵))
Theorem	dflidl2lem 20842*	Lemma for dflidl2 20843: a sufficient condition for a set to be a left ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑥 · 𝑦) ∈ 𝐼) → 𝐼 ∈ 𝑈)
Theorem	dflidl2 20843*	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.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑥 · 𝑦) ∈ 𝐼)))
Theorem	lidl0 20844	Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	lidl1 20845	Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	lidlacs 20846	The ideal system is an algebraic closure system on the base set. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑊 ∈ Ring → 𝐼 ∈ (ACS‘𝐵))
Theorem	rspcl 20847	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 20848	The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺))
Theorem	rsp1 20849	The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐾‘{ 1 }) = 𝐵)
Theorem	rsp0 20850	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 20851	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	mrcrsp 20852	Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐹 = (mrCls‘𝑈)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐾 = 𝐹)
Theorem	lidlnz 20853*	A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑥 ∈ 𝐼 𝑥 ≠ 0 )
Theorem	drngnidl 20854	A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 𝑈 = {{ 0 }, 𝐵})
Theorem	lidlrsppropd 20855*	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‘𝐿)))
10.7.2  Two-sided ideals and quotient rings
Syntax	c2idl 20856	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 20857	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	2idlval 20858	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ 𝑇 = (𝐼 ∩ 𝐽)
Theorem	isridl 20859*	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	df2idl2 20860*	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.)
⊢ 𝑈 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼))))
Theorem	ridl0 20861	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	ridl1 20862	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	2idl0 20863	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝐼)
Theorem	2idl1 20864	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝐼)
Theorem	2idlelb 20865	Membership in a two-sided ideal. Formerly part of proof for 2idlcpbl 20871. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ (𝑈 ∈ 𝑇 ↔ (𝑈 ∈ 𝐼 ∧ 𝑈 ∈ 𝐽))
Theorem	2idllidld 20866	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
Theorem	2idlridld 20867	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂))
Theorem	2idlss 20868	A two-sided ideal is a subset of the base set. Formerly part of proof for 2idlcpbl 20871. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (2Ideal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	2idlbas 20869	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐼)
Theorem	2idlelbas 20870	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	2idlcpbl 20871	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof ahortened by AV, 9-Mar-2025.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝑅 ~QG 𝑆)    &   ⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
Theorem	qus1 20872	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 20873	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 20874*	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 20875	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 20876	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂))
Theorem	crng2idl 20877	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	quscrng 20878	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   ⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ CRing)
10.7.3  Principal ideal rings. Divisibility in the integers
Syntax	clpidl 20879	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 20880	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 20881*	Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ LPIdeal = (𝑤 ∈ Ring ↦ ∪ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
Definition	df-lpir 20882	Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ LPIR = {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)}
Theorem	lpival 20883*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})})
Theorem	islpidl 20884*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
Theorem	lpi0 20885	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃)
Theorem	lpi1 20886	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃)
Theorem	islpir 20887	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃))
Theorem	lpiss 20888	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈)
Theorem	islpir2 20889	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃))
Theorem	lpirring 20890	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring)
Theorem	drnglpir 20891	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR)
Theorem	rspsn 20892*	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 ∧ 𝐺 ∈ 𝐵) → (𝐾‘{𝐺}) = {𝑥 ∣ 𝐺 ∥ 𝑥})
Theorem	lidldvgen 20893*	An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵) → (𝐼 = (𝐾‘{𝐺}) ↔ (𝐺 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 𝐺 ∥ 𝑥)))
Theorem	lpigen 20894*	An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 𝑥 ∥ 𝑦))
10.7.4  Left regular elements. More kinds of rings
Syntax	crlreg 20895	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 20896	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 20897	Class of integral domains.
class IDomn
Syntax	cpid 20898	Class of principal ideal domains.
class PID
Definition	df-rlreg 20899*	Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})
Definition	df-domn 20900*	A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}