![]() |
Metamath
Proof Explorer Theorem List (p. 477 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | linc1 47601* | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) & β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) β β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ( linC βπ)π) = π) | ||
Theorem | lincellss 47602 | 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.) |
β’ ((π β LMod β§ π β (LSubSpβπ) β§ π β π) β ((πΉ β ((Baseβ(Scalarβπ)) βm π) β§ πΉ finSupp (0gβ(Scalarβπ))) β (πΉ( linC βπ)π) β π)) | ||
Theorem | lco0 47603 | 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.) |
β’ (π β Mnd β (π LinCo β ) = {(0gβπ)}) | ||
Theorem | lcoel0 47604 | The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
β’ ((π β LMod β§ π β π« (Baseβπ)) β (0gβπ) β (π LinCo π)) | ||
Theorem | lincsum 47605 | 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.) |
β’ + = (+gβπ) & β’ π = (π΄( linC βπ)π) & β’ π = (π΅( linC βπ)π) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ β = (+gβπ) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ (π΄ β (π βm π) β§ π΅ β (π βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π + π) = ((π΄ βf β π΅)( linC βπ)π)) | ||
Theorem | lincscm 47606* | 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.) |
β’ β = ( Β·π βπ) & β’ Β· = (.rβ(Scalarβπ)) & β’ π = (π΄( linC βπ)π) & β’ π = (Baseβ(Scalarβπ)) & β’ πΉ = (π₯ β π β¦ (π Β· (π΄βπ₯))) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ (π΄ β (π βm π) β§ π β π ) β§ π΄ finSupp (0gβ(Scalarβπ))) β (π β π) = (πΉ( linC βπ)π)) | ||
Theorem | lincsumcl 47607 | 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.) |
β’ + = (+gβπ) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ (πΆ β (π LinCo π) β§ π· β (π LinCo π))) β (πΆ + π·) β (π LinCo π)) | ||
Theorem | lincscmcl 47608 | 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.) |
β’ Β· = ( Β·π βπ) & β’ π = (Baseβ(Scalarβπ)) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π β§ π· β (π LinCo π)) β (πΆ Β· π·) β (π LinCo π)) | ||
Theorem | lincsumscmcl 47609 | 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.) |
β’ Β· = ( Β·π βπ) & β’ π = (Baseβ(Scalarβπ)) & β’ + = (+gβπ) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ (πΆ β π β§ π· β (π LinCo π) β§ π΅ β (π LinCo π))) β ((πΆ Β· π·) + π΅) β (π LinCo π)) | ||
Theorem | lincolss 47610 | According to the statement in [Lang] p. 129, the set (LSubSpβπ) 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 (LSubSpβπ). (Contributed by AV, 12-Apr-2019.) |
β’ ((π β LMod β§ π β π« (Baseβπ)) β (π LinCo π) β (LSubSpβπ)) | ||
Theorem | ellcoellss 47611* | 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.) |
β’ ((π β LMod β§ π β (LSubSpβπ) β§ π β π) β βπ₯ β (π LinCo π)π₯ β π) | ||
Theorem | lcoss 47612 | 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.) |
β’ ((π β LMod β§ π β π« (Baseβπ)) β π β (π LinCo π)) | ||
Theorem | lspsslco 47613 | Lemma for lspeqlco 47615. (Contributed by AV, 17-Apr-2019.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π β π« π΅) β ((LSpanβπ)βπ) β (π LinCo π)) | ||
Theorem | lcosslsp 47614 | Lemma for lspeqlco 47615. (Contributed by AV, 20-Apr-2019.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π β π« π΅) β (π LinCo π) β ((LSpanβπ)βπ)) | ||
Theorem | lspeqlco 47615 | 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 20855) and as the set of all linear combinations of the vectors of the set with finite support. (Contributed by AV, 20-Apr-2019.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π β π« π΅) β (π LinCo π) = ((LSpanβπ)βπ)) | ||
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 47618 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 47616 | Extend class notation with the relation between a module and its linearly independent subsets. |
class linIndS | ||
Syntax | clindeps 47617 | Extend class notation with the relation between a module and its linearly dependent subsets. |
class linDepS | ||
Definition | df-lininds 47618* | 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 = {β¨π , πβ© β£ (π β π« (Baseβπ) β§ βπ β ((Baseβ(Scalarβπ)) βm π )((π finSupp (0gβ(Scalarβπ)) β§ (π( linC βπ)π ) = (0gβπ)) β βπ₯ β π (πβπ₯) = (0gβ(Scalarβπ))))} | ||
Theorem | rellininds 47619 | The class defining the relation between a module and its linearly independent subsets is a relation. (Contributed by AV, 13-Apr-2019.) |
β’ Rel linIndS | ||
Definition | df-lindeps 47620* | Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.) |
β’ linDepS = {β¨π , πβ© β£ Β¬ π linIndS π} | ||
Theorem | linindsv 47621 | The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.) |
β’ (π linIndS π β (π β V β§ π β V)) | ||
Theorem | islininds 47622* | The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β π β§ π β π) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) | ||
Theorem | linindsi 47623* | The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) | ||
Theorem | linindslinci 47624* | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π linIndS π β§ (πΉ β (πΈ βm π) β§ πΉ finSupp 0 β§ (πΉ( linC βπ)π) = π)) β βπ₯ β π (πΉβπ₯) = 0 ) | ||
Theorem | islinindfis 47625* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Fin β§ π β π) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π( linC βπ)π) = π β βπ₯ β π (πβπ₯) = 0 )))) | ||
Theorem | islinindfiss 47626* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β π β§ π β Fin β§ π β π« π΅) β (π linIndS π β βπ β (πΈ βm π)((π( linC βπ)π) = π β βπ₯ β π (πβπ₯) = 0 ))) | ||
Theorem | linindscl 47627 | A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.) |
β’ (π linIndS π β π β π« (Baseβπ)) | ||
Theorem | lindepsnlininds 47628 | A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.) |
β’ ((π β π β§ π β π) β (π linDepS π β Β¬ π linIndS π)) | ||
Theorem | islindeps 47629* | The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β π β§ π β π« π΅) β (π linDepS π β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 ))) | ||
Theorem | lincext1 47630* | Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 29-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΉ = (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β πΉ β (πΈ βm π)) | ||
Theorem | lincext2 47631* | Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΉ = (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π}))) β§ πΊ finSupp 0 ) β πΉ finSupp 0 ) | ||
Theorem | lincext3 47632* | Property 3 of an extension of a linear combination. (Contributed by AV, 23-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΉ = (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π}))) β§ (πΊ finSupp 0 β§ (π( Β·π βπ)π) = (πΊ( linC βπ)(π β {π})))) β (πΉ( linC βπ)π) = π) | ||
Theorem | lindslinindsimp1 47633* | Implication 1 for lindslininds 47640. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ ((π β π β§ π β LMod) β ((π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) β (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦( Β·π βπ)π ) β ((LSpanβπ)β(π β {π }))))) | ||
Theorem | lindslinindimp2lem1 47634* | Lemma 1 for lindslinindsimp2 47639. (Contributed by AV, 25-Apr-2019.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = ((invgβπ )β(πβπ₯)) & β’ πΊ = (π βΎ (π β {π₯})) β β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π β§ π β (π΅ βm π))) β π β π΅) | ||
Theorem | lindslinindimp2lem2 47635* | Lemma 2 for lindslinindsimp2 47639. (Contributed by AV, 25-Apr-2019.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = ((invgβπ )β(πβπ₯)) & β’ πΊ = (π βΎ (π β {π₯})) β β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π β§ π β (π΅ βm π))) β πΊ β (π΅ βm (π β {π₯}))) | ||
Theorem | lindslinindimp2lem3 47636* | Lemma 3 for lindslinindsimp2 47639. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = ((invgβπ )β(πβπ₯)) & β’ πΊ = (π βΎ (π β {π₯})) β β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π) β§ (π β (π΅ βm π) β§ π finSupp 0 )) β πΊ finSupp 0 ) | ||
Theorem | lindslinindimp2lem4 47637* | Lemma 4 for lindslinindsimp2 47639. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = ((invgβπ )β(πβπ₯)) & β’ πΊ = (π βΎ (π β {π₯})) β β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π) β§ (π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π βπ)π¦))) = (π( Β·π βπ)π₯)) | ||
Theorem | lindslinindsimp2lem5 47638* | Lemma 5 for lindslinindsimp2 47639. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦( Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 ))) | ||
Theorem | lindslinindsimp2 47639* | Implication 2 for lindslininds 47640. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ ((π β π β§ π β LMod) β ((π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦( Β·π βπ)π ) β ((LSpanβπ)β(π β {π }))) β (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) | ||
Theorem | lindslininds 47640 | Equivalence of definitions df-linds 21740 and df-lininds 47618 for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
β’ ((π β π β§ π β LMod) β (π linIndS π β π β (LIndSβπ))) | ||
Theorem | linds0 47641 | The empty set is always a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
β’ (π β π β β linIndS π) | ||
Theorem | el0ldep 47642 | 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.) |
β’ (((π β LMod β§ 1 < (β―β(Baseβ(Scalarβπ)))) β§ π β π« (Baseβπ) β§ (0gβπ) β π) β π linDepS π) | ||
Theorem | el0ldepsnzr 47643 | 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.) |
β’ (((π β LMod β§ (Scalarβπ) β NzRing) β§ π β π« (Baseβπ) β§ (0gβπ) β π) β π linDepS π) | ||
Theorem | lindsrng01 47644 | 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 20756), 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.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) β β’ ((π β LMod β§ ((β―βπΈ) = 0 β¨ (β―βπΈ) = 1) β§ π β π« π΅) β π linIndS π) | ||
Theorem | lindszr 47645 | Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019.) |
β’ ((π β LMod β§ Β¬ (Scalarβπ) β NzRing β§ π β π« (Baseβπ)) β π linIndS π) | ||
Theorem | snlindsntorlem 47646* | Lemma for snlindsntor 47647. (Contributed by AV, 15-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π( linC βπ){π}) = π β (πβπ) = 0 ) β βπ β π ((π Β· π) = π β π = 0 ))) | ||
Theorem | snlindsntor 47647* | 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., (π Β· π) = 0. 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 π β π , π β 0, such that π Β· π₯ = 0. 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.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β LMod β§ π β π΅) β (βπ β (π β { 0 })(π Β· π) β π β {π} linIndS π)) | ||
Theorem | ldepsprlem 47648 | Lemma for ldepspr 47649. (Contributed by AV, 16-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ ) & β’ π = (invgβπ ) β β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π΄ β π)) β (π = (π΄ Β· π) β (( 1 Β· π)(+gβπ)((πβπ΄) Β· π)) = π)) | ||
Theorem | ldepspr 47649 | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π΄ β π β§ π = (π΄ Β· π)) β {π, π} linDepS π)) | ||
Theorem | lincresunit3lem3 47650 | Lemma 3 for lincresunit3 47657. (Contributed by AV, 18-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ π = (invgβπ ) & β’ Β· = ( Β·π βπ) β β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (((πβπ΄) Β· π) = ((πβπ΄) Β· π) β π = π)) | ||
Theorem | lincresunitlem1 47651 | Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β (πΌβ(πβ(πΉβπ))) β πΈ) | ||
Theorem | lincresunitlem2 47652 | Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β§ π β π) β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ)) β πΈ) | ||
Theorem | lincresunit1 47653* | Property 1 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β πΊ β (πΈ βm (π β {π}))) | ||
Theorem | lincresunit2 47654* | Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β πΊ finSupp 0 ) | ||
Theorem | lincresunit3lem1 47655* | Lemma 1 for lincresunit3 47657. (Contributed by AV, 17-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ π§ β (π β {π}))) β ((πβ(πΉβπ))( Β·π βπ)((πΊβπ§)( Β·π βπ)π§)) = ((πΉβπ§)( Β·π βπ)π§)) | ||
Theorem | lincresunit3lem2 47656* | Lemma 2 for lincresunit3 47657. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β ((πβ(πΉβπ))( Β·π βπ)(π Ξ£g (π§ β (π β {π}) β¦ ((πΊβπ§)( Β·π βπ)π§)))) = ((πΉ βΎ (π β {π}))( linC βπ)(π β {π}))) | ||
Theorem | lincresunit3 47657* | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (πΊ( linC βπ)(π β {π})) = π) | ||
Theorem | lincreslvec3 47658* | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (πΊ( linC βπ)(π β {π})) = π) | ||
Theorem | islindeps2 47659* | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β LMod β§ π β π« π΅ β§ π β NzRing) β (βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β π linDepS π)) | ||
Theorem | islininds2 47660* | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β LMod β§ π β π« π΅ β§ π β NzRing) β (π linIndS π β βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ))) | ||
Theorem | isldepslvec2 47661* | Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 47659 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.) |
β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ π = (Scalarβπ) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β LVec β§ π β π« π΅) β (βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β π linDepS π)) | ||
Theorem | lindssnlvec 47662 | 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.) |
β’ ((π β LVec β§ π β (Baseβπ) β§ π β (0gβπ)) β {π} linIndS π) | ||
Theorem | lmod1lem1 47663* | Lemma 1 for lmod1 47668. (Contributed by AV, 28-Apr-2019.) |
β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), (π₯ β (Baseβπ ), π¦ β {πΌ} β¦ π¦)β©}) β β’ ((πΌ β π β§ π β Ring β§ π β (Baseβπ )) β (π( Β·π βπ)πΌ) β {πΌ}) | ||
Theorem | lmod1lem2 47664* | Lemma 2 for lmod1 47668. (Contributed by AV, 28-Apr-2019.) |
β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), (π₯ β (Baseβπ ), π¦ β {πΌ} β¦ π¦)β©}) β β’ ((πΌ β π β§ π β Ring β§ π β (Baseβπ )) β (π( Β·π βπ)(πΌ(+gβπ)πΌ)) = ((π( Β·π βπ)πΌ)(+gβπ)(π( Β·π βπ)πΌ))) | ||
Theorem | lmod1lem3 47665* | Lemma 3 for lmod1 47668. (Contributed by AV, 29-Apr-2019.) |
β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), (π₯ β (Baseβπ ), π¦ β {πΌ} β¦ π¦)β©}) β β’ (((πΌ β π β§ π β Ring) β§ (π β (Baseβπ ) β§ π β (Baseβπ ))) β ((π(+gβ(Scalarβπ))π)( Β·π βπ)πΌ) = ((π( Β·π βπ)πΌ)(+gβπ)(π( Β·π βπ)πΌ))) | ||
Theorem | lmod1lem4 47666* | Lemma 4 for lmod1 47668. (Contributed by AV, 29-Apr-2019.) |
β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), (π₯ β (Baseβπ ), π¦ β {πΌ} β¦ π¦)β©}) β β’ (((πΌ β π β§ π β Ring) β§ (π β (Baseβπ ) β§ π β (Baseβπ ))) β ((π(.rβ(Scalarβπ))π)( Β·π βπ)πΌ) = (π( Β·π βπ)(π( Β·π βπ)πΌ))) | ||
Theorem | lmod1lem5 47667* | Lemma 5 for lmod1 47668. (Contributed by AV, 28-Apr-2019.) |
β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), (π₯ β (Baseβπ ), π¦ β {πΌ} β¦ π¦)β©}) β β’ ((πΌ β π β§ π β Ring) β ((1rβ(Scalarβπ))( Β·π βπ)πΌ) = πΌ) | ||
Theorem | lmod1 47668* | The (smallest) structure representing a zero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019.) |
β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), (π₯ β (Baseβπ ), π¦ β {πΌ} β¦ π¦)β©}) β β’ ((πΌ β π β§ π β Ring) β π β LMod) | ||
Theorem | lmod1zr 47669 | The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} & β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), {β¨β¨π, πΌβ©, πΌβ©}β©}) β β’ ((πΌ β π β§ π β π) β π β LMod) | ||
Theorem | lmod1zrnlvec 47670 | There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} & β’ π = ({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), {β¨β¨π, πΌβ©, πΌβ©}β©}) β β’ ((πΌ β π β§ π β π) β π β LVec) | ||
Theorem | lmodn0 47671 | Left modules exist. (Contributed by AV, 29-Apr-2019.) |
β’ LMod β β | ||
Theorem | zlmodzxzequa 47672 | 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 {0, 1}) & β’ 0 = {β¨0, 0β©, β¨1, 0β©} & β’ β = ( Β·π βπ) & β’ β = (-gβπ) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} β β’ ((2 β π΄) β (3 β π΅)) = 0 | ||
Theorem | zlmodzxznm 47673 | 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 {0, 1}) & β’ 0 = {β¨0, 0β©, β¨1, 0β©} & β’ β = ( Β·π βπ) & β’ β = (-gβπ) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} β β’ βπ β β€ ((π β π΄) β π΅ β§ (π β π΅) β π΄) | ||
Theorem | zlmodzxzldeplem 47674 | A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} β β’ π΄ β π΅ | ||
Theorem | zlmodzxzequap 47675 | 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 {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} & β’ 0 = {β¨0, 0β©, β¨1, 0β©} & β’ + = (+gβπ) & β’ β = ( Β·π βπ) β β’ ((2 β π΄) + (-3 β π΅)) = 0 | ||
Theorem | zlmodzxzldeplem1 47676 | Lemma 1 for zlmodzxzldep 47680. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} & β’ πΉ = {β¨π΄, 2β©, β¨π΅, -3β©} β β’ πΉ β (β€ βm {π΄, π΅}) | ||
Theorem | zlmodzxzldeplem2 47677 | Lemma 2 for zlmodzxzldep 47680. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} & β’ πΉ = {β¨π΄, 2β©, β¨π΅, -3β©} β β’ πΉ finSupp 0 | ||
Theorem | zlmodzxzldeplem3 47678 | Lemma 3 for zlmodzxzldep 47680. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} & β’ πΉ = {β¨π΄, 2β©, β¨π΅, -3β©} β β’ (πΉ( linC βπ){π΄, π΅}) = (0gβπ) | ||
Theorem | zlmodzxzldeplem4 47679* | Lemma 4 for zlmodzxzldep 47680. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} & β’ πΉ = {β¨π΄, 2β©, β¨π΅, -3β©} β β’ βπ¦ β {π΄, π΅} (πΉβπ¦) β 0 | ||
Theorem | zlmodzxzldep 47680 | { 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 {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} β β’ {π΄, π΅} linDepS π | ||
Theorem | ldepsnlinclem1 47681 | Lemma 1 for ldepsnlinc 47684. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} β β’ (πΉ β ((Baseββ€ring) βm {π΅}) β (πΉ( linC βπ){π΅}) β π΄) | ||
Theorem | ldepsnlinclem2 47682 | Lemma 2 for ldepsnlinc 47684. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ π΄ = {β¨0, 3β©, β¨1, 6β©} & β’ π΅ = {β¨0, 2β©, β¨1, 4β©} β β’ (πΉ β ((Baseββ€ring) βm {π΄}) β (πΉ( linC βπ){π΄}) β π΅) | ||
Theorem | lvecpsslmod 47683 | 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 20990) 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 47670. (Contributed by AV, 29-Apr-2019.) |
β’ LVec β LMod | ||
Theorem | ldepsnlinc 47684* | The reverse implication of islindeps2 47659 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 47672 and zlmodzxznm 47673. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
β’ βπ β LMod βπ β π« (Baseβπ)(π linDepS π β§ βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp (0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£)) | ||
Theorem | ldepslinc 47685* | For (left) vector spaces, isldepslvec2 47661 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 47684 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.) |
β’ (βπ β LVec βπ β π« (Baseβπ)(π linDepS π β βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp (0gβ(Scalarβπ)) β§ (π( linC βπ)(π β {π£})) = π£)) β§ Β¬ βπ β LMod βπ β π« (Baseβπ)(π linDepS π β βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp (0gβ(Scalarβπ)) β§ (π( linC βπ)(π β {π£})) = π£))) | ||
Theorem | suppdm 47686 | 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.) |
β’ (((Fun πΉ β§ πΉ β π β§ π β π) β§ π β ran πΉ) β (πΉ supp π) = dom πΉ) | ||
Theorem | eluz2cnn0n1 47687 | An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.) |
β’ (π΅ β (β€β₯β2) β π΅ β (β β {0, 1})) | ||
Theorem | divge1b 47688 | The ratio of a real number to a positive real number is greater than or equal to 1 iff the divisor (the positive real number) is less than or equal to the dividend (the real number). (Contributed by AV, 26-May-2020.) |
β’ ((π΄ β β+ β§ π΅ β β) β (π΄ β€ π΅ β 1 β€ (π΅ / π΄))) | ||
Theorem | divgt1b 47689 | The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020.) |
β’ ((π΄ β β+ β§ π΅ β β) β (π΄ < π΅ β 1 < (π΅ / π΄))) | ||
Theorem | ltsubaddb 47690 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ β πΆ) < (π΅ β π·) β (π΄ + π·) < (π΅ + πΆ))) | ||
Theorem | ltsubsubb 47691 | Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ β πΆ) < (π΅ β π·) β (π΄ β π΅) < (πΆ β π·))) | ||
Theorem | ltsubadd2b 47692 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π· β πΆ) < (π΅ β π΄) β (π΄ + π·) < (π΅ + πΆ))) | ||
Theorem | divsub1dir 47693 | Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β ((π΄ / π΅) β 1) = ((π΄ β π΅) / π΅)) | ||
Theorem | expnegico01 47694 | An integer greater than 1 to the power of a negative integer is in the closed-below, open-above interval between 0 and 1. (Contributed by AV, 24-May-2020.) |
β’ ((π΅ β (β€β₯β2) β§ π β β€ β§ π < 0) β (π΅βπ) β (0[,)1)) | ||
Theorem | elfzolborelfzop1 47695 | An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020.) |
β’ (πΎ β (π..^π) β (πΎ = π β¨ πΎ β ((π + 1)..^π))) | ||
Theorem | pw2m1lepw2m1 47696 | 2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020.) |
β’ (πΌ β β β (2β(πΌ β 1)) β€ ((2βπΌ) β 1)) | ||
Theorem | zgtp1leeq 47697 | If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.) |
β’ ((πΌ β β€ β§ π΄ β β€) β (((π΄ β 1) < πΌ β§ πΌ β€ π΄) β πΌ = π΄)) | ||
Theorem | flsubz 47698 | An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.) |
β’ ((π΄ β β β§ π β β€) β (ββ(π΄ β π)) = ((ββπ΄) β π)) | ||
Theorem | fldivmod 47699 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
β’ ((π΄ β β β§ π΅ β β+) β (ββ(π΄ / π΅)) = ((π΄ β (π΄ mod π΅)) / π΅)) | ||
Theorem | mod0mul 47700* | If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020.) |
β’ ((π΄ β β€ β§ π β β) β ((π΄ mod π) = 0 β βπ₯ β β€ π΄ = (π₯ Β· π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |