P. 215 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	lspsolv 21401	If 𝑋 is in the span of 𝐴 ∪ {𝑌} but not 𝐴, then 𝑌 is in the span of 𝐴 ∪ {𝑋}. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑌 ∈ (𝑁‘(𝐴 ∪ {𝑋})))
Theorem	lssacsex 21402*	In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 21222 by lspsolv 21401. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝑋 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐴 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))))
Theorem	lspsnat 21403	There is no subspace strictly between the zero subspace and the span of a vector (i.e. a 1-dimensional subspace is an atom). (h1datomi 32165 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 = (𝑁‘{𝑋}) ∨ 𝑈 = { 0 }))
Theorem	lspsncv0 21404*	The span of a singleton covers the zero subspace, using Definition 3.2.18 of [PtakPulmannova] p. 68 for "covers".) (Contributed by NM, 12-Aug-2014.) (Revised by AV, 13-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ¬ ∃𝑦 ∈ 𝑆 ({ 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ (𝑁‘{𝑋})))
Theorem	lsppratlem1 21405	Lemma for lspprat 21411. Let 𝑥 ∈ (𝑈 ∖ {0}) (if there is no such 𝑥 then 𝑈 is the zero subspace), and let 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})) (assuming the conclusion is false). The goal is to write 𝑋, 𝑌 in terms of 𝑥, 𝑦, which would normally be done by solving the system of linear equations. The span equivalent of this process is lspsolv 21401 (hence the name), which we use extensively below. In this lemma, we show that since 𝑥 ∈ (𝑁‘{𝑋, 𝑌}), either 𝑥 ∈ (𝑁‘{𝑌}) or 𝑋 ∈ (𝑁‘{𝑥, 𝑌}). (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝑁‘{𝑌}) ∨ 𝑋 ∈ (𝑁‘{𝑥, 𝑌})))
Theorem	lsppratlem2 21406	Lemma for lspprat 21411. Show that if 𝑋 and 𝑌 are both in (𝑁‘{𝑥, 𝑦}) (which will be our goal for each of the two cases above), then (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈, contradicting the hypothesis for 𝑈. (Contributed by NM, 29-Aug-2014.) (Revised by Mario Carneiro, 5-Sep-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑦}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈)
Theorem	lsppratlem3 21407	Lemma for lspprat 21411. In the first case of lsppratlem1 21405, since 𝑥 ∉ (𝑁‘∅), also 𝑌 ∈ (𝑁‘{𝑥}), and since 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑋, 𝑥}) and 𝑦 ∉ (𝑁‘{𝑥}), we have 𝑋 ∈ (𝑁‘{𝑥, 𝑦}) as desired. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑥 ∈ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦})))
Theorem	lsppratlem4 21408	Lemma for lspprat 21411. In the second case of lsppratlem1 21405, 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌}) and 𝑦 ∉ (𝑁‘{𝑥}) implies 𝑌 ∈ (𝑁‘{𝑥, 𝑦}) and thus 𝑋 ∈ (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦}) as well. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦})))
Theorem	lsppratlem5 21409	Lemma for lspprat 21411. Combine the two cases and show a contradiction to 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}) under the assumptions on 𝑥 and 𝑦. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈)
Theorem	lsppratlem6 21410	Lemma for lspprat 21411. Negating the assumption on 𝑦, we arrive close to the desired conclusion. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝑈 ∖ { 0 }) → 𝑈 = (𝑁‘{𝑥})))
Theorem	lspprat 21411*	A proper subspace of the span of a pair of vectors is the span of a singleton (an atom) or the zero subspace (if 𝑧 is zero). Proof suggested by Mario Carneiro, 28-Aug-2014. (Contributed by NM, 29-Aug-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑈 = (𝑁‘{𝑧}))
Theorem	islbs2 21412*	An equivalent formulation of the basis predicate in a vector space: a subset is a basis iff no element is in the span of the rest of the set. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
Theorem	islbs3 21413*	An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑠(𝑠 ⊊ 𝐵 → (𝑁‘𝑠) ⊊ 𝑉))))
Theorem	lbsacsbs 21414	Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 21412. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝐼 ∧ (𝑁‘𝑆) = 𝑋)))
Theorem	lvecdim 21415	The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 21402 and lbsacsbs 21414 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 18713. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽) → 𝑆 ≈ 𝑇)
Theorem	lbsextlem1 21416*	Lemma for lbsext 21421. The set 𝑆 is the set of all linearly independent sets containing 𝐶; we show here that it is nonempty. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    ⇒   ⊢ (𝜑 → 𝑆 ≠ ∅)
Theorem	lbsextlem2 21417*	Lemma for lbsext 21421. Since 𝐴 is a chain (actually, we only need it to be closed under binary union), the union 𝑇 of the spans of each individual element of 𝐴 is a subspace, and it contains all of ∪ 𝐴 (except for our target vector 𝑥- we are trying to make 𝑥 a linear combination of all the other vectors in some set from 𝐴). (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ 𝑃 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝐴)    &   ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))    ⇒   ⊢ (𝜑 → (𝑇 ∈ 𝑃 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇))
Theorem	lbsextlem3 21418*	Lemma for lbsext 21421. A chain in 𝑆 has an upper bound in 𝑆. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ 𝑃 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝐴)    &   ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑆)
Theorem	lbsextlem4 21419*	Lemma for lbsext 21421. lbsextlem3 21418 satisfies the conditions for the application of Zorn's lemma zorn 10566 (thus invoking AC), and so there is a maximal linearly independent set extending 𝐶. Here we prove that such a set is a basis. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))    &   ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}    &   ⊢ (𝜑 → 𝒫 𝑉 ∈ dom card)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠)
Theorem	lbsextg 21420*	For any linearly independent subset 𝐶 of 𝑉, there is a basis containing the vectors in 𝐶. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (((𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card) ∧ 𝐶 ⊆ 𝑉 ∧ ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠)
Theorem	lbsext 21421*	For any linearly independent subset 𝐶 of 𝑉, there is a basis containing the vectors in 𝐶. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐶 ⊆ 𝑉 ∧ ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠)
Theorem	lbsexg 21422	Every vector space has a basis. This theorem is an AC equivalent; this is the forward implication. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ ((CHOICE ∧ 𝑊 ∈ LVec) → 𝐽 ≠ ∅)
Theorem	lbsex 21423	Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ 𝐽 = (LBasis‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐽 ≠ ∅)
Theorem	lvecprop2d 21424*	If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd 21425 also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ 𝐹 = (Scalar‘𝐾)    &   ⊢ 𝐺 = (Scalar‘𝐿)    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(.r‘𝐹)𝑦) = (𝑥(.r‘𝐺)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec))
Theorem	lvecpropd 21425*	If two structures have the same components (properties), one is a left vector space iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐾))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿))    &   ⊢ 𝑃 = (Base‘𝐹)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec))
10.7  Subring algebras and ideals
10.7.1  Subring algebras
Syntax	csra 21426	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 21427	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 21428*	Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))
Definition	df-rgmod 21429	Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod = (𝑤 ∈ V ↦ ((subringAlg ‘𝑤)‘(Base‘𝑤)))
Theorem	sraval 21430	Lemma for srabase 21432 through sravsca 21436. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet ⟨(Scalar‘ndx), (𝑊 ↾s 𝑆)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑊)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑊)⟩))
Theorem	sralem 21431	Lemma for srabase 21432 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (Scalar‘ndx) ≠ (𝐸‘ndx)    &   ⊢ ( ·𝑠 ‘ndx) ≠ (𝐸‘ndx)    &   ⊢ (·𝑖‘ndx) ≠ (𝐸‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴))
Theorem	srabase 21432	Base set 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‘𝑊))    ⇒   ⊢ (𝜑 → (Base‘𝑊) = (Base‘𝐴))
Theorem	sraaddg 21433	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.) (Revised by AV, 29-Oct-2024.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (+g‘𝑊) = (+g‘𝐴))
Theorem	sramulr 21434	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	srasca 21435	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	sravsca 21436	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	sraip 21437	The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.r‘𝑊) = (·𝑖‘𝐴))
Theorem	sratset 21438	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	sratopn 21439	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 21440	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 21441	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring)
Theorem	sralmod 21442	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    ⇒   ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod)
Theorem	sralmod0 21443	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 21444*	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 21445	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ ringLMod Fn V
Theorem	rlmval 21446	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))
Theorem	rlmval2 21447	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 21448	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (Base‘𝑅) = (Base‘(ringLMod‘𝑅))
Theorem	rlmplusg 21449	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (+g‘𝑅) = (+g‘(ringLMod‘𝑅))
Theorem	rlm0 21450	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 21451	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (-g‘𝑅) = (-g‘(ringLMod‘𝑅))
Theorem	rlmmulr 21452	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (.r‘𝑅) = (.r‘(ringLMod‘𝑅))
Theorem	rlmsca 21453	Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ 𝑋 → 𝑅 = (Scalar‘(ringLMod‘𝑅)))
Theorem	rlmsca2 21454	Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅))
Theorem	rlmvsca 21455	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅))
Theorem	rlmtopn 21456	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅))
Theorem	rlmds 21457	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (dist‘𝑅) = (dist‘(ringLMod‘𝑅))
Theorem	rlmlmod 21458	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod)
Theorem	rlmlvec 21459	The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ DivRing → (ringLMod‘𝑅) ∈ LVec)
Theorem	rlmlsm 21460	Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024.)
⊢ (𝑅 ∈ 𝑉 → (LSSum‘𝑅) = (LSSum‘(ringLMod‘𝑅)))
Theorem	rlmvneg 21461	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 21462	Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (+𝑓‘(mulGrp‘𝑅)) = ( ·sf ‘(ringLMod‘𝑅))
Theorem	ixpsnbasval 21463*	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‘𝑅))})
10.7.2  Left ideals and spans Remark: Usually, (left) ideals are defined as a subset of a (unital or non-unital) ring that is a subgroup of the additive group of the ring that "absorbs multiplication from the left by elements of the ring", see Wikipedia https://en.wikipedia.org/wiki/Ideal_(ring_theory) (19.02.2025), or the definition 4 in [BourbakiAlg1] p. 103 and the definition in [Lang] p.86, although a ring is to be considered unital (and commutative!) here, see definition 1 in [BourbakiAlg1] p. 96 resp. the definition in [Lang] p. 83, or definition in [Roman] p. 20. In contrast, the definition of (LIdeal‘𝑅), does not require the subset to be a subgroup of the additive group, as can be seen by islidl 21474. If 𝑅 is a unital ring, however, it can be proven that each ideal in (LIdeal‘𝑅) is a subgroup of the additive group of the ring, see lidlsubg 21482. This is not possible for arbitrary non-unital rings, because the proof uses the existence of the ring unity.
Syntax	clidl 21464	Ring left-ideal function.
class LIdeal
Syntax	crsp 21465	Ring span function.
class RSpan
Definition	df-lidl 21466	Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. For 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, see dflidl2rng 21477 and dflidl2 21487. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ LIdeal = (LSubSp ∘ ringLMod)
Definition	df-rsp 21467	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ RSpan = (LSpan ∘ ringLMod)
Theorem	lidlval 21468	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))
Theorem	rspval 21469	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊))
Theorem	lidlss 21470	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵)
Theorem	lidlbasel 21471	An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by AV, 27-Jun-2026.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐼 = (LIdeal‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝐵)
Theorem	lidlssbas 21472	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 21473	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	islidl 21474*	Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼))
Theorem	rnglidlmcl 21475	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 as in lidlmcl 21484. (Contributed by AV, 18-Feb-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼)) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	rngridlmcl 21476	A right ideal (which is a left ideal over the opposite ring) containing the zero element is closed under right-multiplication by elements of the full non-unital ring. (Contributed by AV, 19-Feb-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘(oppr‘𝑅))    ⇒   ⊢ (((𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼)) → (𝑌 · 𝑋) ∈ 𝐼)
Theorem	dflidl2rng 21477*	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 21478*	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 21479	An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼)
Theorem	lidlacl 21480	An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼)
Theorem	lidlnegcl 21481	An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼)
Theorem	lidlsubg 21482	An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅))
Theorem	lidlsubcl 21483	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 21484	An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Proof shortened by AV, 31-Mar-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼)) → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	lidl1el 21485	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	lidlmcld 21486	An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐼)
Theorem	dflidl2 21487*	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	lidl0ALT 21488	Alternate proof for lidl0 21490 not using rnglidl0 21489: Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	rnglidl0 21489	Every non-unital ring contains a zero ideal. (Contributed by AV, 19-Feb-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → { 0 } ∈ 𝑈)
Theorem	lidl0 21490	Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Proof shortened by AV, 18-Apr-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈)
Theorem	lidl1ALT 21491	Alternate proof for lidl1 21493 not using rnglidl1 21492: Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	rnglidl1 21492	The base set of every non-unital ring is an ideal. For unital rings, such ideals are called "unit ideals", see lidl1 21493. (Contributed by AV, 19-Feb-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐵 ∈ 𝑈)
Theorem	lidl1 21493	Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Proof shortened by AV, 18-Apr-2025.)
⊢ 𝑈 = (LIdeal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈)
Theorem	0ringidl 21494	The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (LIdeal‘𝑅) = {{ 0 }})
Theorem	lidlunin0 21495	The union of a nonempty subset of ideals in a ring is nonempty. (Contributed by AV, 28-Jun-2026.)
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∪ 𝐶 ≠ ∅)
Theorem	unichnlidl 21496*	The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by AV, 28-Jun-2026.)
⊢ ((𝑅 ∈ Ring ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (LIdeal‘𝑅))
Theorem	lidlacs 21497	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 21498	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 21499	The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺))
Theorem	rsp1 21500	The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐾‘{ 1 }) = 𝐵)