![]() |
Metamath
Proof Explorer Theorem List (p. 210 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lspsolvlem 20901* | Lemma for lspsolv 20902. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = {π§ β π β£ βπ β π΅ (π§ + (π Β· π)) β (πβπ΄)} & β’ (π β π β LMod) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β π β (πβ(π΄ βͺ {π}))) β β’ (π β βπ β π΅ (π + (π Β· π)) β (πβπ΄)) | ||
Theorem | lspsolv 20902 | 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 20903* | In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 20723 by lspsolv 20902. (Contributed by David Moews, 1-May-2017.) |
β’ π΄ = (LSubSpβπ) & β’ π = (mrClsβπ΄) & β’ π = (Baseβπ) β β’ (π β LVec β (π΄ β (ACSβπ) β§ βπ β π« πβπ¦ β π βπ§ β ((πβ(π βͺ {π¦})) β (πβπ ))π¦ β (πβ(π βͺ {π§})))) | ||
Theorem | lspsnat 20904 | 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 31098 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 22-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (((π β LVec β§ π β π β§ π β π) β§ π β (πβ{π})) β (π = (πβ{π}) β¨ π = { 0 })) | ||
Theorem | lspsncv0 20905* | 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 20906 | Lemma for lspprat 20912. 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 20902 (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 20907 | Lemma for lspprat 20912. 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 20908 | Lemma for lspprat 20912. In the first case of lsppratlem1 20906, since π₯ β (πββ ), also π β (πβ{π₯}), and since π¦ β (πβ{π, π}) β (πβ{π, π₯}) and π¦ β (πβ{π₯}), we have π β (πβ{π₯, π¦}) as desired. (Contributed by NM, 29-Aug-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π, π})) & β’ 0 = (0gβπ) & β’ (π β π₯ β (π β { 0 })) & β’ (π β π¦ β (π β (πβ{π₯}))) & β’ (π β π₯ β (πβ{π})) β β’ (π β (π β (πβ{π₯, π¦}) β§ π β (πβ{π₯, π¦}))) | ||
Theorem | lsppratlem4 20909 | Lemma for lspprat 20912. In the second case of lsppratlem1 20906, π¦ β (πβ{π, π}) β (πβ{π₯, π}) and π¦ β (πβ{π₯}) implies π β (πβ{π₯, π¦}) and thus π β (πβ{π₯, π}) β (πβ{π₯, π¦}) as well. (Contributed by NM, 29-Aug-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π, π})) & β’ 0 = (0gβπ) & β’ (π β π₯ β (π β { 0 })) & β’ (π β π¦ β (π β (πβ{π₯}))) & β’ (π β π β (πβ{π₯, π})) β β’ (π β (π β (πβ{π₯, π¦}) β§ π β (πβ{π₯, π¦}))) | ||
Theorem | lsppratlem5 20910 | Lemma for lspprat 20912. 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 20911 | Lemma for lspprat 20912. 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 20912* | 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 20913* | 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 20914* | 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 20915 | Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 20913. (Contributed by David Moews, 1-May-2017.) |
β’ π΄ = (LSubSpβπ) & β’ π = (mrClsβπ΄) & β’ π = (Baseβπ) & β’ πΌ = (mrIndβπ΄) & β’ π½ = (LBasisβπ) β β’ (π β LVec β (π β π½ β (π β πΌ β§ (πβπ) = π))) | ||
Theorem | lvecdim 20916 | The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 20903 and lbsacsbs 20915 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 18517. (Contributed by David Moews, 1-May-2017.) |
β’ π½ = (LBasisβπ) β β’ ((π β LVec β§ π β π½ β§ π β π½) β π β π) | ||
Theorem | lbsextlem1 20917* | Lemma for lbsext 20922. 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 20918* | Lemma for lbsext 20922. 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 20919* | Lemma for lbsext 20922. A chain in π has an upper bound in π. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β πΆ β π) & β’ (π β βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯}))) & β’ π = {π§ β π« π β£ (πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})))} & β’ π = (LSubSpβπ) & β’ (π β π΄ β π) & β’ (π β π΄ β β ) & β’ (π β [β] Or π΄) & β’ π = βͺ π’ β π΄ (πβ(π’ β {π₯})) β β’ (π β βͺ π΄ β π) | ||
Theorem | lbsextlem4 20920* | Lemma for lbsext 20922. lbsextlem3 20919 satisfies the conditions for the application of Zorn's lemma zorn 10505 (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 20921* | 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 20922* | 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 20923 | 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 20924 | Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ π½ = (LBasisβπ) β β’ (π β LVec β π½ β β ) | ||
Theorem | lvecprop2d 20925* | If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd 20926 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 20926* | 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 20927 | Extend class notation with the subring algebra generator. |
class subringAlg | ||
Syntax | crglmod 20928 | Extend class notation with the left module induced by a ring over itself. |
class ringLMod | ||
Syntax | clidl 20929 | Ring left-ideal function. |
class LIdeal | ||
Syntax | crsp 20930 | Ring span function. |
class RSpan | ||
Definition | df-sra 20931* | 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 20932 | 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 20933 | 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 dflidl2 20993. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ LIdeal = (LSubSp β ringLMod) | ||
Definition | df-rsp 20934 | Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ RSpan = (LSpan β ringLMod) | ||
Theorem | sraval 20935 | Lemma for srabase 20938 through sravsca 20946. (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 20936 | Lemma for srabase 20938 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 | sralemOLD 20937 | Obsolete version of sralem 20936 as of 29-Oct-2024. Lemma for srabase 20938 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) & β’ πΈ = Slot π & β’ π β β & β’ (π < 5 β¨ 8 < π) β β’ (π β (πΈβπ) = (πΈβπ΄)) | ||
Theorem | srabase 20938 | 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 | srabaseOLD 20939 | Obsolete proof of srabase 20938 as of 29-Oct-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) β β’ (π β (Baseβπ) = (Baseβπ΄)) | ||
Theorem | sraaddg 20940 | 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 | sraaddgOLD 20941 | Obsolete proof of sraaddg 20940 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 20942 | 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 20943 | Obsolete proof of sramulr 20942 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 20944 | 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 20945 | Obsolete proof of srasca 20944 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 20946 | 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 20947 | Obsolete proof of sravsca 20946 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 20948 | The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (Baseβπ)) β β’ (π β (.rβπ) = (Β·πβπ΄)) | ||
Theorem | sratset 20949 | 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 20950 | Obsolete proof of sratset 20949 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 20951 | 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 20952 | 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 20953 | Obsolete proof of srads 20952 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 20954 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π΅) β π΄ β Ring) | ||
Theorem | sralmod 20955 | The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ π΄ = ((subringAlg βπ)βπ) β β’ (π β (SubRingβπ) β π΄ β LMod) | ||
Theorem | sralmod0 20956 | 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 20957* | 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 20958 | ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
β’ ringLMod Fn V | ||
Theorem | rlmval 20959 | Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ (ringLModβπ) = ((subringAlg βπ)β(Baseβπ)) | ||
Theorem | lidlval 20960 | Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ (LIdealβπ) = (LSubSpβ(ringLModβπ)) | ||
Theorem | rspval 20961 | Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ (RSpanβπ) = (LSpanβ(ringLModβπ)) | ||
Theorem | rlmval2 20962 | 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 20963 | Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ (Baseβπ ) = (Baseβ(ringLModβπ )) | ||
Theorem | rlmplusg 20964 | Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ (+gβπ ) = (+gβ(ringLModβπ )) | ||
Theorem | rlm0 20965 | 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 20966 | Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ (-gβπ ) = (-gβ(ringLModβπ )) | ||
Theorem | rlmmulr 20967 | Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (.rβπ ) = (.rβ(ringLModβπ )) | ||
Theorem | rlmsca 20968 | Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
β’ (π β π β π = (Scalarβ(ringLModβπ ))) | ||
Theorem | rlmsca2 20969 | Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ ( I βπ ) = (Scalarβ(ringLModβπ )) | ||
Theorem | rlmvsca 20970 | Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ (.rβπ ) = ( Β·π β(ringLModβπ )) | ||
Theorem | rlmtopn 20971 | Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (TopOpenβπ ) = (TopOpenβ(ringLModβπ )) | ||
Theorem | rlmds 20972 | Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (distβπ ) = (distβ(ringLModβπ )) | ||
Theorem | rlmlmod 20973 | The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
β’ (π β Ring β (ringLModβπ ) β LMod) | ||
Theorem | rlmlvec 20974 | The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β DivRing β (ringLModβπ ) β LVec) | ||
Theorem | rlmlsm 20975 | Subgroup sum of the ring module. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
β’ (π β π β (LSSumβπ ) = (LSSumβ(ringLModβπ ))) | ||
Theorem | rlmvneg 20976 | 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 20977 | Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (+πβ(mulGrpβπ )) = ( Β·sf β(ringLModβπ )) | ||
Theorem | ixpsnbasval 20978* | 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 20979 | An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ πΌ = (LIdealβπ) β β’ (π β πΌ β π β π΅) | ||
Theorem | lidlssbas 20980 | 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 20981 | 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 20982* | Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ (πΌ β π β (πΌ β π΅ β§ πΌ β β β§ βπ₯ β π΅ βπ β πΌ βπ β πΌ ((π₯ Β· π) + π) β πΌ)) | ||
Theorem | rnglidlmcl 20983 | 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 20990. (Contributed by AV, 18-Feb-2025.) |
β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (LIdealβπ ) β β’ (((π β Rng β§ πΌ β π β§ 0 β πΌ) β§ (π β π΅ β§ π β πΌ)) β (π Β· π) β πΌ) | ||
Theorem | rngridlmcl 20984 | 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 | lidl0cl 20985 | An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΌ β π) β 0 β πΌ) | ||
Theorem | lidlacl 20986 | An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ + = (+gβπ ) β β’ (((π β Ring β§ πΌ β π) β§ (π β πΌ β§ π β πΌ)) β (π + π) β πΌ) | ||
Theorem | lidlnegcl 20987 | An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ πΌ β π β§ π β πΌ) β (πβπ) β πΌ) | ||
Theorem | lidlsubg 20988 | An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β πΌ β (SubGrpβπ )) | ||
Theorem | lidlsubcl 20989 | 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 20990 | 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 20991 | 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 20992* | Lemma for dflidl2 20993: a sufficient condition for a set to be a left ideal. (Contributed by AV, 13-Feb-2025.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((πΌ β (SubGrpβπ ) β§ βπ₯ β π΅ βπ¦ β πΌ (π₯ Β· π¦) β πΌ) β πΌ β π) | ||
Theorem | dflidl2 20993* | 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 20994 | Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } β π) | ||
Theorem | lidl1 20995 | Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β π) | ||
Theorem | lidlacs 20996 | 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 20997 | 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 20998 | The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ πΊ β π΅) β πΊ β (πΎβπΊ)) | ||
Theorem | rsp1 20999 | 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 21000 | The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ πΎ = (RSpanβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πΎβ{ 0 }) = { 0 }) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |