![]() |
Metamath
Proof Explorer Theorem List (p. 200 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lspindp3 19901 | Independence of 2 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑋 + 𝑌)})) | ||
Theorem | lspindp4 19902 | (Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑋 + 𝑌)})) | ||
Theorem | lvecindp 19903 | Compute the 𝑋 coefficient in a sum with an independent vector 𝑋 (first conjunct), which can then be removed to continue with the remaining vectors summed in expressions 𝑌 and 𝑍 (second conjunct). Typically, 𝑈 is the span of the remaining vectors. (Contributed by NM, 5-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 19-Jul-2022.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝑌) = ((𝐵 · 𝑋) + 𝑍)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝑌 = 𝑍)) | ||
Theorem | lvecindp2 19904 | Sums of independent vectors must have equal coefficients. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝐷 ∈ 𝐾) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐶 · 𝑋) + (𝐷 · 𝑌))) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | lspsnsubn0 19905 | Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ≠ 0 ) | ||
Theorem | lsmcv 19906 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 29435 analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ (𝑁‘{𝑋}))) → 𝑈 = (𝑇 ⊕ (𝑁‘{𝑋}))) | ||
Theorem | lspsolvlem 19907* | Lemma for lspsolv 19908. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)} & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌}))) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) | ||
Theorem | lspsolv 19908 | 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 19909* | In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 19732 by lspsolv 19908. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = (LSubSp‘𝑊) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝑋 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝐴 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))) | ||
Theorem | lspsnat 19910 | 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 29364 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 = (𝑁‘{𝑋}) ∨ 𝑈 = { 0 })) | ||
Theorem | lspsncv0 19911* | 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 19912 | Lemma for lspprat 19918. 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 19908 (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 19913 | Lemma for lspprat 19918. 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 19914 | Lemma for lspprat 19918. In the first case of lsppratlem1 19912, since 𝑥 ∉ (𝑁‘∅), also 𝑌 ∈ (𝑁‘{𝑥}), and since 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑋, 𝑥}) and 𝑦 ∉ (𝑁‘{𝑥}), we have 𝑋 ∈ (𝑁‘{𝑥, 𝑦}) as desired. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) & ⊢ (𝜑 → 𝑥 ∈ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))) | ||
Theorem | lsppratlem4 19915 | Lemma for lspprat 19918. In the second case of lsppratlem1 19912, 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌}) and 𝑦 ∉ (𝑁‘{𝑥}) implies 𝑌 ∈ (𝑁‘{𝑥, 𝑦}) and thus 𝑋 ∈ (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦}) as well. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌})) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))) | ||
Theorem | lsppratlem5 19916 | Lemma for lspprat 19918. 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 19917 | Lemma for lspprat 19918. 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 19918* | 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 19919* | 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 19920* | 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 19921 | Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 19919. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = (LSubSp‘𝑊) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝐼 ∧ (𝑁‘𝑆) = 𝑋))) | ||
Theorem | lvecdim 19922 | The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 19909 and lbsacsbs 19921 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 17785. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽) → 𝑆 ≈ 𝑇) | ||
Theorem | lbsextlem1 19923* | Lemma for lbsext 19928. 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 19924* | Lemma for lbsext 19928. 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 19925* | Lemma for lbsext 19928. A chain in 𝑆 has an upper bound in 𝑆. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐶 ⊆ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) & ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} & ⊢ 𝑃 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝐴) & ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | lbsextlem4 19926* | Lemma for lbsext 19928. lbsextlem3 19925 satisfies the conditions for the application of Zorn's lemma zorn 9918 (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 19927* | 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 19928* | 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 19929 | 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 19930 | Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐽 ≠ ∅) | ||
Theorem | lvecprop2d 19931* | If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd 19932 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 19932* | 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)) | ||
Syntax | csra 19933 | Extend class notation with the subring algebra generator. |
class subringAlg | ||
Syntax | crglmod 19934 | Extend class notation with the left module induced by a ring over itself. |
class ringLMod | ||
Syntax | clidl 19935 | Ring left-ideal function. |
class LIdeal | ||
Syntax | crsp 19936 | Ring span function. |
class RSpan | ||
Definition | df-sra 19937* | 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 19938 | 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‘𝑤))) | ||
Definition | df-lidl 19939 | 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 19940 | Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ RSpan = (LSpan ∘ ringLMod) | ||
Theorem | sraval 19941 | Lemma for srabase 19943 through sravsca 19947. (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 19942 | Lemma for srabase 19943 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ (𝑁 < 5 ∨ 8 < 𝑁) ⇒ ⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴)) | ||
Theorem | srabase 19943 | 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.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (Base‘𝑊) = (Base‘𝐴)) | ||
Theorem | sraaddg 19944 | 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.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (+g‘𝑊) = (+g‘𝐴)) | ||
Theorem | sramulr 19945 | 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.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.r‘𝑊) = (.r‘𝐴)) | ||
Theorem | srasca 19946 | 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.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) | ||
Theorem | sravsca 19947 | 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.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.r‘𝑊) = ( ·𝑠 ‘𝐴)) | ||
Theorem | sraip 19948 | The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.r‘𝑊) = (·𝑖‘𝐴)) | ||
Theorem | sratset 19949 | Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (TopSet‘𝑊) = (TopSet‘𝐴)) | ||
Theorem | sratopn 19950 | 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 19951 | Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (dist‘𝑊) = (dist‘𝐴)) | ||
Theorem | sralmod 19952 | The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) | ||
Theorem | sralmod0 19953 | The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 0 = (0g‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 0 = (0g‘𝐴)) | ||
Theorem | issubrngd2 19954* | 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 19955 | ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
⊢ ringLMod Fn V | ||
Theorem | rlmval 19956 | Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊)) | ||
Theorem | lidlval 19957 | Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊)) | ||
Theorem | rspval 19958 | Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊)) | ||
Theorem | rlmval2 19959 | 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 19960 | Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (Base‘𝑅) = (Base‘(ringLMod‘𝑅)) | ||
Theorem | rlmplusg 19961 | Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (+g‘𝑅) = (+g‘(ringLMod‘𝑅)) | ||
Theorem | rlm0 19962 | 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 19963 | Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ (-g‘𝑅) = (-g‘(ringLMod‘𝑅)) | ||
Theorem | rlmmulr 19964 | Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (.r‘𝑅) = (.r‘(ringLMod‘𝑅)) | ||
Theorem | rlmsca 19965 | Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
⊢ (𝑅 ∈ 𝑋 → 𝑅 = (Scalar‘(ringLMod‘𝑅))) | ||
Theorem | rlmsca2 19966 | Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅)) | ||
Theorem | rlmvsca 19967 | Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (.r‘𝑅) = ( ·𝑠 ‘(ringLMod‘𝑅)) | ||
Theorem | rlmtopn 19968 | Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅)) | ||
Theorem | rlmds 19969 | Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (dist‘𝑅) = (dist‘(ringLMod‘𝑅)) | ||
Theorem | rlmlmod 19970 | The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
⊢ (𝑅 ∈ Ring → (ringLMod‘𝑅) ∈ LMod) | ||
Theorem | rlmlvec 19971 | The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ DivRing → (ringLMod‘𝑅) ∈ LVec) | ||
Theorem | rlmlsm 19972 | Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
⊢ (𝑅 ∈ 𝑉 → (LSSum‘𝑅) = (LSSum‘(ringLMod‘𝑅))) | ||
Theorem | rlmvneg 19973 | 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 19974 | Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (+𝑓‘(mulGrp‘𝑅)) = ( ·sf ‘(ringLMod‘𝑅)) | ||
Theorem | ixpsnbasval 19975* | 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 19976 | An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐼 = (LIdeal‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵) | ||
Theorem | islidl 19977* | Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐼 ∈ 𝑈 ↔ (𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐼 ((𝑥 · 𝑎) + 𝑏) ∈ 𝐼)) | ||
Theorem | lidl0cl 19978 | An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼) | ||
Theorem | lidlacl 19979 | An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (𝑋 + 𝑌) ∈ 𝐼) | ||
Theorem | lidlnegcl 19980 | An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝑁‘𝑋) ∈ 𝐼) | ||
Theorem | lidlsubg 19981 | An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅)) | ||
Theorem | lidlsubcl 19982 | 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 19983 | 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 19984 | 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 | lidl0 19985 | Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } ∈ 𝑈) | ||
Theorem | lidl1 19986 | Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈) | ||
Theorem | lidlacs 19987 | 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 19988 | 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 19989 | The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) | ||
Theorem | rsp1 19990 | 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 19991 | 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 19992 | 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 19993 | Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐹 = (mrCls‘𝑈) ⇒ ⊢ (𝑅 ∈ Ring → 𝐾 = 𝐹) | ||
Theorem | lidlnz 19994* | A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑥 ∈ 𝐼 𝑥 ≠ 0 ) | ||
Theorem | drngnidl 19995 | 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 19996* | 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‘𝐿))) | ||
Syntax | c2idl 19997 | Ring two-sided ideal function. |
class 2Ideal | ||
Definition | df-2idl 19998 | 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 19999 | Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐽 = (LIdeal‘𝑂) & ⊢ 𝑇 = (2Ideal‘𝑅) ⇒ ⊢ 𝑇 = (𝐼 ∩ 𝐽) | ||
Theorem | 2idlcpbl 20000 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝐸 = (𝑅 ~QG 𝑆) & ⊢ 𝐼 = (2Ideal‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |