Home | Metamath
Proof Explorer Theorem List (p. 423 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lcoval 42201* | The value of a linear combination. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar LinCo finSupp linC | ||
Theorem | lincfsuppcl 42202 | A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar finSupp linC | ||
Theorem | linccl 42203 | A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.) |
Scalar linC | ||
Theorem | lincval0 42204 | The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.) |
linC | ||
Theorem | lincvalsng 42205 | The linear combination over a singleton. (Contributed by AV, 25-May-2019.) |
Scalar linC | ||
Theorem | lincvalsn 42206 | The linear combination over a singleton. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 25-May-2019.) |
Scalar linC | ||
Theorem | lincvalpr 42207 | The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.) |
Scalar linC | ||
Theorem | lincval1 42208 | The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) |
Scalar linC | ||
Theorem | lcosn0 42209 | Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar finSupp linC | ||
Theorem | lincvalsc0 42210* | The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) |
Scalar linC | ||
Theorem | lcoc0 42211* | Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar finSupp linC | ||
Theorem | linc0scn0 42212* | If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019.) |
Scalar linC | ||
Theorem | lincdifsn 42213 | A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar finSupp linC linC | ||
Theorem | linc1 42214* | A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
Scalar linC | ||
Theorem | lincellss 42215 | A linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar finSupp Scalar linC | ||
Theorem | lco0 42216 | The set of empty linear combinations over a monoid is the singleton with the identity element of the monoid. (Contributed by AV, 12-Apr-2019.) |
LinCo | ||
Theorem | lcoel0 42217 | The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
LinCo | ||
Theorem | lincsum 42218 | The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
linC linC Scalar finSupp finSupp linC | ||
Theorem | lincscm 42219* | A linear combinations multiplied with a scalar is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 9-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
Scalar linC Scalar finSupp Scalar linC | ||
Theorem | lincsumcl 42220 | The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
LinCo LinCo LinCo | ||
Theorem | lincscmcl 42221 | The multiplication of a linear combination with a scalar is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 11-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
Scalar LinCo LinCo | ||
Theorem | lincsumscmcl 42222 | The sum of a linear combination and a multiplication of a linear combination with a scalar is a linear combination. (Contributed by AV, 11-Apr-2019.) |
Scalar LinCo LinCo LinCo | ||
Theorem | lincolss 42223 | According to the statement in [Lang] p. 129, the set of all linear combinations of a set of vectors V is a submodule (generated by V) of the module M. The elements of V are called generators of . (Contributed by AV, 12-Apr-2019.) |
LinCo | ||
Theorem | ellcoellss 42224* | Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
LinCo | ||
Theorem | lcoss 42225 | A set of vectors of a module is a subset of the set of all linear combinations of the set. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
LinCo | ||
Theorem | lspsslco 42226 | Lemma for lspeqlco 42228. (Contributed by AV, 17-Apr-2019.) |
LinCo | ||
Theorem | lcosslsp 42227 | Lemma for lspeqlco 42228. (Contributed by AV, 20-Apr-2019.) |
LinCo | ||
Theorem | lspeqlco 42228 | Equivalence of a span of a set of vectors of a left module defined as the intersection of all linear subspaces which each contain every vector in that set ( see df-lsp 18972) and as the set of all linear combinations of the vectors of the set with finite support. (Contributed by AV, 20-Apr-2019.) |
LinCo | ||
According to the definition in [Lang] p. 129: "A subset S of a module M is said
to be linearly independent (over [the ring] A) if whenever we have a
linear combination ∑x ∈S axx which is equal to
0, then ax=0 for all x∈S.". This definition does not care for
the finiteness of the set S (because the definition of a linear combination
in [Lang] p.129 does already assure that only a finite number of coefficients
can be 0 in the sum). Our definition df-lininds 42231 does also neither claim that
the subset must be finite, nor that almost all coefficients within the linear
combination are 0. If this is required, it must be explicitly stated as
precondition in the corresponding theorems. | ||
Syntax | clininds 42229 | Extend class notation with the relation between a module and its linearly independent subsets. |
linIndS | ||
Syntax | clindeps 42230 | Extend class notation with the relation between a module and its linearly dependent subsets. |
linDepS | ||
Definition | df-lininds 42231* | Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
linIndS Scalar finSupp Scalar linC Scalar | ||
Theorem | rellininds 42232 | The class defining the relation between a module and its linearly independent subsets is a relation. (Contributed by AV, 13-Apr-2019.) |
linIndS | ||
Definition | df-lindeps 42233* | Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.) |
linDepS linIndS | ||
Theorem | linindsv 42234 | The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.) |
linIndS | ||
Theorem | islininds 42235* | The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar linIndS finSupp linC | ||
Theorem | linindsi 42236* | The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar linIndS finSupp linC | ||
Theorem | linindslinci 42237* | The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar linIndS finSupp linC | ||
Theorem | islinindfis 42238* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
Scalar linIndS linC | ||
Theorem | islinindfiss 42239* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
Scalar linIndS linC | ||
Theorem | linindscl 42240 | A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.) |
linIndS | ||
Theorem | lindepsnlininds 42241 | A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.) |
linDepS linIndS | ||
Theorem | islindeps 42242* | The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar linDepS finSupp linC | ||
Theorem | lincext1 42243* | Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 29-Apr-2019.) |
Scalar | ||
Theorem | lincext2 42244* | Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp finSupp | ||
Theorem | lincext3 42245* | Property 3 of an extension of a linear combination. (Contributed by AV, 23-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp linC linC | ||
Theorem | lindslinindsimp1 42246* | Implication 1 for lindslininds 42253. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp linC | ||
Theorem | lindslinindimp2lem1 42247* | Lemma 1 for lindslinindsimp2 42252. (Contributed by AV, 25-Apr-2019.) |
Scalar | ||
Theorem | lindslinindimp2lem2 42248* | Lemma 2 for lindslinindsimp2 42252. (Contributed by AV, 25-Apr-2019.) |
Scalar | ||
Theorem | lindslinindimp2lem3 42249* | Lemma 3 for lindslinindsimp2 42252. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp finSupp | ||
Theorem | lindslinindimp2lem4 42250* | Lemma 4 for lindslinindsimp2 42252. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp linC g | ||
Theorem | lindslinindsimp2lem5 42251* | Lemma 5 for lindslinindsimp2 42252. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp linC finSupp linC | ||
Theorem | lindslinindsimp2 42252* | Implication 2 for lindslininds 42253. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
Scalar finSupp linC | ||
Theorem | lindslininds 42253 | Equivalence of definitions df-linds 20146 and df-lininds 42231 for (linear) independency for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
linIndS LIndS | ||
Theorem | linds0 42254 | The empty set is always a linearly independet subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
linIndS | ||
Theorem | el0ldep 42255 | A set containing the zero element of a module is always linearly dependent, if the underlying ring has at least two elements. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar linDepS | ||
Theorem | el0ldepsnzr 42256 | A set containing the zero element of a module over a nonzero ring is always linearly dependent. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.) |
Scalar NzRing linDepS | ||
Theorem | lindsrng01 42257 | Any subset of a module is always linearly independent if the underlying ring has at most one element. Since the underlying ring cannot be the empty set (see lmodsn0 18876), this means that the underlying ring has only one element, so it is a zero ring. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.) |
Scalar linIndS | ||
Theorem | lindszr 42258 | Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019.) |
Scalar NzRing linIndS | ||
Theorem | snlindsntorlem 42259* | Lemma for snlindsntor 42260. (Contributed by AV, 15-Apr-2019.) |
Scalar linC | ||
Theorem | snlindsntor 42260* | A singleton is linearly independent iff it does not contain a torsion element. According to Wikipedia ("Torsion (algebra)", 15-Apr-2019, https://en.wikipedia.org/wiki/Torsion_(algebra)): "An element m of a module M over a ring R is called a torsion element of the module if there exists a regular element r of the ring (an element that is neither a left nor a right zero divisor) that annihilates m, i.e., . In an integral domain (a commutative ring without zero divisors), every nonzero element is regular, so a torsion element of a module over an integral domain is one annihilated by a nonzero element of the integral domain." Analogously, the definition in [Lang] p. 147 states that "An element x of [a module] E [over a ring R] is called a torsion element if there exists , , such that . This definition includes the zero element of the module. Some authors, however, exclude the zero element from the definition of torsion elements. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.) |
Scalar linIndS | ||
Theorem | ldepsprlem 42261 | Lemma for ldepspr 42262. (Contributed by AV, 16-Apr-2019.) |
Scalar | ||
Theorem | ldepspr 42262 | If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar linDepS | ||
Theorem | lincresunit3lem3 42263 | Lemma 3 for lincresunit3 42270. (Contributed by AV, 18-May-2019.) |
Scalar Unit | ||
Theorem | lincresunitlem1 42264 | Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
Scalar Unit | ||
Theorem | lincresunitlem2 42265 | Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
Scalar Unit | ||
Theorem | lincresunit1 42266* | Property 1 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
Scalar Unit | ||
Theorem | lincresunit2 42267* | Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
Scalar Unit finSupp finSupp | ||
Theorem | lincresunit3lem1 42268* | Lemma 1 for lincresunit3 42270. (Contributed by AV, 17-May-2019.) |
Scalar Unit | ||
Theorem | lincresunit3lem2 42269* | Lemma 2 for lincresunit3 42270. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar Unit finSupp g linC | ||
Theorem | lincresunit3 42270* | Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar Unit finSupp linC linC | ||
Theorem | lincreslvec3 42271* | Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar Unit finSupp linC linC | ||
Theorem | islindeps2 42272* | Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar NzRing finSupp linC linDepS | ||
Theorem | islininds2 42273* | Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar NzRing linIndS finSupp linC | ||
Theorem | isldepslvec2 42274* | Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 42272 holds, so that both definitions are equivalent (see theorem 1.6 in [Roman] p. 46 and the note in [Roman] p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
Scalar finSupp linC linDepS | ||
Theorem | lindssnlvec 42275 | A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 28-Apr-2019.) |
linIndS | ||
Theorem | lmod1lem1 42276* | Lemma 1 for lmod1 42281. (Contributed by AV, 28-Apr-2019.) |
Scalar | ||
Theorem | lmod1lem2 42277* | Lemma 2 for lmod1 42281. (Contributed by AV, 28-Apr-2019.) |
Scalar | ||
Theorem | lmod1lem3 42278* | Lemma 3 for lmod1 42281. (Contributed by AV, 29-Apr-2019.) |
Scalar Scalar | ||
Theorem | lmod1lem4 42279* | Lemma 4 for lmod1 42281. (Contributed by AV, 29-Apr-2019.) |
Scalar Scalar | ||
Theorem | lmod1lem5 42280* | Lemma 5 for lmod1 42281. (Contributed by AV, 28-Apr-2019.) |
Scalar Scalar | ||
Theorem | lmod1 42281* | The (smallest) structure representing a zero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019.) |
Scalar | ||
Theorem | lmod1zr 42282 | The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.) |
Scalar | ||
Theorem | lmod1zrnlvec 42283 | There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.) |
Scalar | ||
Theorem | lmodn0 42284 | Left modules exist. (Contributed by AV, 29-Apr-2019.) |
Theorem | zlmodzxzequa 42285 | Example of an equation within the -module (see example in [Roman] p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod | ||
Theorem | zlmodzxznm 42286 | Example of a linearly dependent set whose elements are not linear combinations of the others, see note in [Roman] p. 112). (Contributed by AV, 23-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod | ||
Theorem | zlmodzxzldeplem 42287 | A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod | ||
Theorem | zlmodzxzequap 42288 | Example of an equation within the -module (see example in [Roman] p. 112 for a linearly dependent set), written as a sum. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod | ||
Theorem | zlmodzxzldeplem1 42289 | Lemma 1 for zlmodzxzldep 42293. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod | ||
Theorem | zlmodzxzldeplem2 42290 | Lemma 2 for zlmodzxzldep 42293. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.) |
ℤring freeLMod finSupp | ||
Theorem | zlmodzxzldeplem3 42291 | Lemma 3 for zlmodzxzldep 42293. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod linC | ||
Theorem | zlmodzxzldeplem4 42292* | Lemma 4 for zlmodzxzldep 42293. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod | ||
Theorem | zlmodzxzldep 42293 | { A , B } is a linearly dependent set within the -module (see example in [Roman] p. 112). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod linDepS | ||
Theorem | ldepsnlinclem1 42294 | Lemma 1 for ldepsnlinc 42297. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod ℤring linC | ||
Theorem | ldepsnlinclem2 42295 | Lemma 2 for ldepsnlinc 42297. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.) |
ℤring freeLMod ℤring linC | ||
Theorem | lvecpsslmod 42296 | The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 19106) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 42283. (Contributed by AV, 29-Apr-2019.) |
Theorem | ldepsnlinc 42297* | The reverse implication of islindeps2 42272 does not hold for arbitrary (left) modules, see note in [Roman] p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 42285 and zlmodzxznm 42286. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
linDepS Scalar finSupp Scalar linC | ||
Theorem | ldepslinc 42298* | For (left) vector spaces, isldepslvec2 42274 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 42297 indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
linDepS Scalar finSupp Scalar linC linDepS Scalar finSupp Scalar linC | ||
Theorem | offval0 42299* | Value of an operation applied to two functions. (Contributed by AV, 15-May-2020.) |
Theorem | suppdm 42300 | If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020.) |
supp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |