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	sraaddgOLD 20801	Obsolete proof of sraaddg 20800 as of 29-Oct-2024. Additive 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‘𝑊))    ⇒   ⊢ (𝜑 → (+g‘𝑊) = (+g‘𝐴))
Theorem	sramulr 20802	Multiplicative 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.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (.r‘𝐴))
Theorem	sramulrOLD 20803	Obsolete proof of sramulr 20802 as of 29-Oct-2024. Multiplicative 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‘𝑊) = (.r‘𝐴))
Theorem	srasca 20804	The set of scalars 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 shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴))
Theorem	srascaOLD 20805	Obsolete proof of srasca 20804 as of 12-Nov-2024. The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 12-Nov-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴))
Theorem	sravsca 20806	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 shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = ( ·𝑠 ‘𝐴))
Theorem	sravscaOLD 20807	Obsolete proof of sravsca 20806 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 20808	The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (·𝑖‘𝐴))
Theorem	sratset 20809	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 20810	Obsolete proof of sratset 20809 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 20811	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 20812	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 20813	Obsolete proof of srads 20812 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 20814	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring)
Theorem	sralmod 20815	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    ⇒   ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod)
Theorem	sralmod0 20816	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 20817*	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 20818	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod Fn V
Theorem	rlmval 20819	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))
Theorem	lidlval 20820	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))
Theorem	rspval 20821	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊))
Theorem	rlmval2 20822	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 20823	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (Base‘𝑅) = (Base‘(ringLMod‘𝑅))
Theorem	rlmplusg 20824	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (+g‘𝑅) = (+g‘(ringLMod‘𝑅))
Theorem	rlm0 20825	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 20826	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (-g‘𝑅) = (-g‘(ringLMod‘𝑅))
Theorem	rlmmulr 20827	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (.r‘𝑅) = (.r‘(ringLMod‘𝑅))
Theorem	rlmsca 20828	Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ 𝑋 → 𝑅 = (Scalar‘(ringLMod‘𝑅)))
Theorem	rlmsca2 20829	Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅))
Theorem	rlmvsca 20830	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅))
Theorem	rlmtopn 20831	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅))
Theorem	rlmds 20832	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (dist‘𝑅) = (dist‘(ringLMod‘𝑅))
Theorem	rlmlmod 20833	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod)
Theorem	rlmlvec 20834	The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ DivRing → (ringLMod‘𝑅) ∈ LVec)
Theorem	rlmlsm 20835	Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024.)
⊢ (𝑅 ∈ 𝑉 → (LSSum‘𝑅) = (LSSum‘(ringLMod‘𝑅)))
Theorem	rlmvneg 20836	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 20837	Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (+𝑓‘(mulGrp‘𝑅)) = ( ·sf ‘(ringLMod‘𝑅))
Theorem	ixpsnbasval 20838*	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 20839	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	islidl 20840*	Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼))
Theorem	lidl0cl 20841	An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼)
Theorem	lidlacl 20842	An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼)
Theorem	lidlnegcl 20843	An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼)
Theorem	lidlsubg 20844	An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅))
Theorem	lidlsubcl 20845	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 20846	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 20847	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 20848*	Lemma for dflidl2 20849: a sufficient condition for a set to be a left ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑥 · 𝑦) ∈ 𝐼) → 𝐼 ∈ 𝑈)
Theorem	dflidl2 20849*	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 20850	Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	lidl1 20851	Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	lidlacs 20852	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 20853	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 20854	The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺))
Theorem	rsp1 20855	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 20856	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 20857	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 20858	Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐹 = (mrCls‘𝑈)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐾 = 𝐹)
Theorem	lidlnz 20859*	A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑥 ∈ 𝐼 𝑥 ≠ 0 )
Theorem	drngnidl 20860	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 20861*	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 20862	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 20863	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 20864	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ 𝑇 = (𝐼 ∩ 𝐽)
Theorem	isridl 20865*	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 20866*	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 20867	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	ridl1 20868	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	2idl0 20869	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝐼)
Theorem	2idl1 20870	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
⊢ 𝐼 = (2Ideal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝐼)
Theorem	2idlelb 20871	Membership in a two-sided ideal. Formerly part of proof for 2idlcpbl 20877. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐽 = (LIdeal‘𝑂)    &   ⊢ 𝑇 = (2Ideal‘𝑅)    ⇒   ⊢ (𝑈 ∈ 𝑇 ↔ (𝑈 ∈ 𝐼 ∧ 𝑈 ∈ 𝐽))
Theorem	2idllidld 20872	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
Theorem	2idlridld 20873	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑂))
Theorem	2idlss 20874	A two-sided ideal is a subset of the base set. Formerly part of proof for 2idlcpbl 20877. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (2Ideal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	2idlbas 20875	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐽 = (𝑅 ↾s 𝐼)    &   ⊢ 𝐵 = (Base‘𝐽)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐼)
Theorem	2idlelbas 20876	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 20877	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 20878	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 20879	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 20880*	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 20881	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 20882	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐼 = (LIdeal‘𝑂))
Theorem	crng2idl 20883	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 20884	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 20885	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 20886	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 20887*	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 20888	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 20889*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})})
Theorem	islpidl 20890*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐼 ∈ 𝑃 ↔ ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
Theorem	lpi0 20891	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑃)
Theorem	lpi1 20892	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑃)
Theorem	islpir 20893	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 = 𝑃))
Theorem	lpiss 20894	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝑈)
Theorem	islpir2 20895	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑃 = (LPIdeal‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝑈 ⊆ 𝑃))
Theorem	lpirring 20896	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ Ring)
Theorem	drnglpir 20897	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ LPIR)
Theorem	rspsn 20898*	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 20899*	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 20900*	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 ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 𝑥 ∥ 𝑦))