![]() |
Metamath
Proof Explorer Theorem List (p. 208 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lss0cl 20701 | The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β 0 β π) | ||
Theorem | lsssn0 20702 | The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β { 0 } β π) | ||
Theorem | lss0ss 20703 | The zero subspace is included in every subspace. (sh0le 30960 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β { 0 } β π) | ||
Theorem | lssle0 20704 | No subspace is smaller than the zero subspace. (shle0 30962 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β { 0 } β π = { 0 })) | ||
Theorem | lssne0 20705* | A nonzero subspace has a nonzero vector. (shne0i 30968 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ (π β π β (π β { 0 } β βπ¦ β π π¦ β 0 )) | ||
Theorem | lssvneln0 20706 | A vector π which doesn't belong to a subspace π is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 19-Jul-2022.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β π β 0 ) | ||
Theorem | lssneln0 20707 | A vector π which doesn't belong to a subspace π is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 17-Jul-2022.) (Proof shortened by AV, 19-Jul-2022.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β π β (π β { 0 })) | ||
Theorem | lssssr 20708* | Conclude subspace ordering from nonzero vector membership. (ssrdv 3987 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π₯ β (π β { 0 })) β (π₯ β π β π₯ β π)) β β’ (π β π β π) | ||
Theorem | lssvacl 20709 | Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ + = (+gβπ) & β’ π = (LSubSpβπ) β β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π + π) β π) | ||
Theorem | lssvscl 20710 | Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (BaseβπΉ) & β’ π = (LSubSpβπ) β β’ (((π β LMod β§ π β π) β§ (π β π΅ β§ π β π)) β (π Β· π) β π) | ||
Theorem | lssvnegcl 20711 | Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
β’ π = (LSubSpβπ) & β’ π = (invgβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β π) | ||
Theorem | lsssubg 20712 | All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) | ||
Theorem | lsssssubg 20713 | All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (LSubSpβπ) β β’ (π β LMod β π β (SubGrpβπ)) | ||
Theorem | islss3 20714 | A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π = (π βΎs π) & β’ π = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β (π β π β (π β π β§ π β LMod))) | ||
Theorem | lsslmod 20715 | A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β LMod) | ||
Theorem | lsslss 20716 | The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β π β (π β π β§ π β π))) | ||
Theorem | islss4 20717* | A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β (π β π β (π β (SubGrpβπ) β§ βπ β π΅ βπ β π (π Β· π) β π))) | ||
Theorem | lss1d 20718* | One-dimensional subspace (or zero-dimensional if π is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β π) | ||
Theorem | lssintcl 20719 | The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π΄ β π β§ π΄ β β ) β β© π΄ β π) | ||
Theorem | lssincl 20720 | The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π β© π) β π) | ||
Theorem | lssmre 20721 | The subspaces of a module comprise a Moore system on the vectors of the module. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β π β (Mooreβπ΅)) | ||
Theorem | lssacs 20722 | Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β π β (ACSβπ΅)) | ||
Theorem | prdsvscacl 20723* | Pointwise scalar multiplication is closed in products of modules. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆLMod) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) & β’ ((π β§ π₯ β πΌ) β (Scalarβ(π βπ₯)) = π) β β’ (π β (πΉ Β· πΊ) β π΅) | ||
Theorem | prdslmodd 20724* | The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆLMod) & β’ ((π β§ π¦ β πΌ) β (Scalarβ(π βπ¦)) = π) β β’ (π β π β LMod) | ||
Theorem | pwslmod 20725 | A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LMod β§ πΌ β π) β π β LMod) | ||
Syntax | clspn 20726 | Extend class notation with span of a set of vectors. |
class LSpan | ||
Definition | df-lsp 20727* | Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) |
β’ LSpan = (π€ β V β¦ (π β π« (Baseβπ€) β¦ β© {π‘ β (LSubSpβπ€) β£ π β π‘})) | ||
Theorem | lspfval 20728* | The span function for a left vector space (or a left module). (df-span 30829 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β π β π = (π β π« π β¦ β© {π‘ β π β£ π β π‘})) | ||
Theorem | lspf 20729 | The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β π:π« πβΆπ) | ||
Theorem | lspval 20730* | The span of a set of vectors (in a left module). (spanval 30853 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = β© {π‘ β π β£ π β π‘}) | ||
Theorem | lspcl 20731 | The span of a set of vectors is a subspace. (spancl 30856 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) | ||
Theorem | lspsncl 20732 | The span of a singleton is a subspace (frequently used special case of lspcl 20731). (Contributed by NM, 17-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β π) | ||
Theorem | lspprcl 20733 | The span of a pair is a subspace (frequently used special case of lspcl 20731). (Contributed by NM, 11-Apr-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) | ||
Theorem | lsptpcl 20734 | The span of an unordered triple is a subspace (frequently used special case of lspcl 20731). (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π, π}) β π) | ||
Theorem | lspsnsubg 20735 | The span of a singleton is an additive subgroup (frequently used special case of lspcl 20731). (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) | ||
Theorem | 00lsp 20736 | fvco4i 6991 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ β = (LSpanββ ) | ||
Theorem | lspid 20737 | The span of a subspace is itself. (spanid 30867 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = π) | ||
Theorem | lspssv 20738 | A span is a set of vectors. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) | ||
Theorem | lspss 20739 | Span preserves subset ordering. (spanss 30868 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β (πβπ)) | ||
Theorem | lspssid 20740 | A set of vectors is a subset of its span. (spanss2 30865 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβπ)) | ||
Theorem | lspidm 20741 | The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ(πβπ)) = (πβπ)) | ||
Theorem | lspun 20742 | The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβ(π βͺ π)) = (πβ((πβπ) βͺ (πβπ)))) | ||
Theorem | lspssp 20743 | If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β π) | ||
Theorem | mrclsp 20744 | Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΎ = (LSpanβπ) & β’ πΉ = (mrClsβπ) β β’ (π β LMod β πΎ = πΉ) | ||
Theorem | lspsnss 20745 | The span of the singleton of a subspace member is included in the subspace. (spansnss 31091 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβ{π}) β π) | ||
Theorem | lspsnel3 20746 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 31092 analog.) (Contributed by NM, 4-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) β β’ (π β π β π) | ||
Theorem | lspprss 20747 | The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) | ||
Theorem | lspsnid 20748 | A vector belongs to the span of its singleton. (spansnid 31083 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβ{π})) | ||
Theorem | lspsnel6 20749 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (π β π β (π β π β§ (πβ{π}) β π))) | ||
Theorem | lspsnel5 20750 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β (πβ{π}) β π)) | ||
Theorem | lspsnel5a 20751 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π}) β π) | ||
Theorem | lspprid1 20752 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprid2 20753 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprvacl 20754 | The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π + π) β (πβ{π, π})) | ||
Theorem | lssats2 20755* | A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β π = βͺ π₯ β π (πβ{π₯})) | ||
Theorem | lspsneli 20756 | A scalar product with a vector belongs to the span of its singleton. (spansnmul 31084 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) β β’ (π β (π΄ Β· π) β (πβ{π})) | ||
Theorem | lspsn 20757* | Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) = {π£ β£ βπ β πΎ π£ = (π Β· π)}) | ||
Theorem | lspsnel 20758* | Member of span of the singleton of a vector. (elspansn 31086 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnvsi 20759 | Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β πΎ β§ π β π) β (πβ{(π Β· π)}) β (πβ{π})) | ||
Theorem | lspsnss2 20760* | Comparable spans of singletons must have proportional vectors. See lspsneq 20880 for equal span version. (Contributed by NM, 7-Jun-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnneg 20761 | Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) = (πβ{π})) | ||
Theorem | lspsnsub 20762 | Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{(π β π)}) = (πβ{(π β π)})) | ||
Theorem | lspsn0 20763 | Span of the singleton of the zero vector. (spansn0 31061 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πβ{ 0 }) = { 0 }) | ||
Theorem | lsp0 20764 | Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πββ ) = { 0 }) | ||
Theorem | lspuni0 20765 | Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β βͺ (πββ ) = 0 ) | ||
Theorem | lspun0 20766 | The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (πβ(π βͺ { 0 })) = (πβπ)) | ||
Theorem | lspsneq0 20767 | Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β ((πβ{π}) = { 0 } β π = 0 )) | ||
Theorem | lspsneq0b 20768 | Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (πβ{π}) = (πβ{π})) β β’ (π β (π = 0 β π = 0 )) | ||
Theorem | lmodindp1 20769 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π + π) β 0 ) | ||
Theorem | lsslsp 20770 | Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) TODO: Shouldn't we swap πβπΊ and πβπΊ since we are computing a property of πβπΊ? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015. |
β’ π = (π βΎs π) & β’ π = (LSpanβπ) & β’ π = (LSpanβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) = (πβπΊ)) | ||
Theorem | lss0v 20771 | The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.) |
β’ π = (π βΎs π) & β’ 0 = (0gβπ) & β’ π = (0gβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β LMod β§ π β πΏ) β π = 0 ) | ||
Theorem | lsspropd 20772* | If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β π = (Baseβ(ScalarβπΎ))) & β’ (π β π = (Baseβ(ScalarβπΏ))) β β’ (π β (LSubSpβπΎ) = (LSubSpβπΏ)) | ||
Theorem | lsppropd 20773* | If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β π = (Baseβ(ScalarβπΎ))) & β’ (π β π = (Baseβ(ScalarβπΏ))) & β’ (π β πΎ β π) & β’ (π β πΏ β π) β β’ (π β (LSpanβπΎ) = (LSpanβπΏ)) | ||
Syntax | clmhm 20774 | Extend class notation with the generator of left module hom-sets. |
class LMHom | ||
Syntax | clmim 20775 | The class of left module isomorphism sets. |
class LMIso | ||
Syntax | clmic 20776 | The class of the left module isomorphism relation. |
class βπ | ||
Definition | df-lmhm 20777* | A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ LMHom = (π β LMod, π‘ β LMod β¦ {π β (π GrpHom π‘) β£ [(Scalarβπ ) / π€]((Scalarβπ‘) = π€ β§ βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ )(πβ(π₯( Β·π βπ )π¦)) = (π₯( Β·π βπ‘)(πβπ¦)))}) | ||
Definition | df-lmim 20778* | An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ LMIso = (π β LMod, π‘ β LMod β¦ {π β (π LMHom π‘) β£ π:(Baseβπ )β1-1-ontoβ(Baseβπ‘)}) | ||
Definition | df-lmic 20779 | Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ βπ = (β‘ LMIso β (V β 1o)) | ||
Theorem | reldmlmhm 20780 | Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ Rel dom LMHom | ||
Theorem | lmimfn 20781 | Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ LMIso Fn (LMod Γ LMod) | ||
Theorem | islmhm 20782* | Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ (πΉ β (π LMHom π) β ((π β LMod β§ π β LMod) β§ (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) | ||
Theorem | islmhm3 20783* | Property of a module homomorphism, similar to ismhm 18707. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) | ||
Theorem | lmhmlem 20784 | Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) β β’ (πΉ β (π LMHom π) β ((π β LMod β§ π β LMod) β§ (πΉ β (π GrpHom π) β§ πΏ = πΎ))) | ||
Theorem | lmhmsca 20785 | A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) β β’ (πΉ β (π LMHom π) β πΏ = πΎ) | ||
Theorem | lmghm 20786 | A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) | ||
Theorem | lmhmlmod2 20787 | A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β π β LMod) | ||
Theorem | lmhmlmod1 20788 | A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β π β LMod) | ||
Theorem | lmhmf 20789 | A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π LMHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | lmhmlin 20790 | A homomorphism of left modules is πΎ-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((πΉ β (π LMHom π) β§ π β π΅ β§ π β πΈ) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) | ||
Theorem | lmodvsinv 20791 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ π = (invgβπΉ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π΅) β ((πβπ ) Β· π) = (πβ(π Β· π))) | ||
Theorem | lmodvsinv2 20792 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π΅) β (π Β· (πβπ)) = (πβ(π Β· π))) | ||
Theorem | islmhm2 20793* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20687. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ πΈ = (BaseβπΎ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))))) | ||
Theorem | islmhmd 20794* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) & β’ πΎ = (Scalarβπ) & β’ π½ = (Scalarβπ) & β’ π = (BaseβπΎ) & β’ (π β π β LMod) & β’ (π β π β LMod) & β’ (π β π½ = πΎ) & β’ (π β πΉ β (π GrpHom π)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) β β’ (π β πΉ β (π LMHom π)) | ||
Theorem | 0lmhm 20795 | The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β LMod β§ π = π) β (π΅ Γ { 0 }) β (π LMHom π)) | ||
Theorem | idlmhm 20796 | The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β LMod β ( I βΎ π΅) β (π LMHom π)) | ||
Theorem | invlmhm 20797 | The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ πΌ = (invgβπ) β β’ (π β LMod β πΌ β (π LMHom π)) | ||
Theorem | lmhmco 20798 | The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ β πΊ) β (π LMHom π)) | ||
Theorem | lmhmplusg 20799 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ + = (+gβπ) β β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ βf + πΊ) β (π LMHom π)) | ||
Theorem | lmhmvsca 20800 | The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π½ = (Scalarβπ) & β’ πΎ = (Baseβπ½) β β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π Γ {π΄}) βf Β· πΉ) β (π LMHom π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |