Home | Metamath
Proof Explorer Theorem List (p. 204 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmodsubvs 20301 | Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (invgβπΉ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π΄ Β· π)) = (π + ((πβπ΄) Β· π))) | ||
Theorem | lmodsubdi 20302 | Scalar multiplication distributive law for subtraction. (hvsubdistr1 29777 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π΄ Β· (π β π)) = ((π΄ Β· π) β (π΄ Β· π))) | ||
Theorem | lmodsubdir 20303 | Scalar multiplication distributive law for subtraction. (hvsubdistr2 29778 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β ((π΄ππ΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) | ||
Theorem | lmodsubeq0 20304 | If the difference between two vectors is zero, they are equal. (hvsubeq0 29796 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ β π΅) = 0 β π΄ = π΅)) | ||
Theorem | lmodsubid 20305 | Subtraction of a vector from itself. (hvsubid 29754 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π΄ β π) β (π΄ β π΄) = 0 ) | ||
Theorem | lmodvsghm 20306* | Scalar multiplication of the vector space by a fixed scalar is an endomorphism of the additive group of vectors. (Contributed by Mario Carneiro, 5-May-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ) β (π₯ β π β¦ (π Β· π₯)) β (π GrpHom π)) | ||
Theorem | lmodprop2d 20307* | If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 20308 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βπΊ)π¦)) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) β β’ (π β (πΎ β LMod β πΏ β LMod)) | ||
Theorem | lmodpropd 20308* | If two structures have the same components (properties), one is a left module iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 27-Jun-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ (π β πΉ = (ScalarβπΎ)) & β’ (π β πΉ = (ScalarβπΏ)) & β’ π = (BaseβπΉ) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) β β’ (π β (πΎ β LMod β πΏ β LMod)) | ||
Theorem | gsumvsmul 20309* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 19954, since every ring is a left module over itself. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) (Revised by AV, 10-Jul-2019.) |
β’ π΅ = (Baseβπ ) & β’ π = (Scalarβπ ) & β’ πΎ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ + = (+gβπ ) & β’ Β· = ( Β·π βπ ) & β’ (π β π β LMod) & β’ (π β π΄ β π) & β’ (π β π β πΎ) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) | ||
Theorem | mptscmfsupp0 20310* | A mapping to a scalar product is finitely supported if the mapping to the scalar is finitely supported. (Contributed by AV, 5-Oct-2019.) |
β’ (π β π· β π) & β’ (π β π β LMod) & β’ (π β π = (Scalarβπ)) & β’ πΎ = (Baseβπ) & β’ ((π β§ π β π·) β π β π΅) & β’ ((π β§ π β π·) β π β πΎ) & β’ 0 = (0gβπ) & β’ π = (0gβπ ) & β’ β = ( Β·π βπ) & β’ (π β (π β π· β¦ π) finSupp π) β β’ (π β (π β π· β¦ (π β π)) finSupp 0 ) | ||
Theorem | mptscmfsuppd 20311* | A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe 21589. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.) (Proof shortened by AV, 18-Oct-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ ((π β§ π β π) β π β π΅) & β’ (π β π΄:πβΆπ) & β’ (π β π΄ finSupp (0gβπ)) β β’ (π β (π β π β¦ ((π΄βπ) Β· π)) finSupp (0gβπ)) | ||
Theorem | rmodislmodlem 20312* | Lemma for rmodislmod 20313. This is the part of the proof of rmodislmod 20313 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.) |
β’ π = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = ( Β·π βπ ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ (π β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) & β’ β = (π β πΎ, π£ β π β¦ (π£ Β· π )) & β’ πΏ = (π sSet β¨( Β·π βndx), β β©) β β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Γ π) β π) = (π β (π β π))) | ||
Theorem | rmodislmod 20313* | The right module π induces a left module πΏ by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod 20247 of a left module, see also islmod 20249. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.) |
β’ π = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = ( Β·π βπ ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ (π β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) & β’ β = (π β πΎ, π£ β π β¦ (π£ Β· π )) & β’ πΏ = (π sSet β¨( Β·π βndx), β β©) β β’ (πΉ β CRing β πΏ β LMod) | ||
Theorem | rmodislmodOLD 20314* | Obsolete version of rmodislmod 20313 as of 18-Oct-2024. The right module π induces a left module πΏ by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod 20247 of a left module, see also islmod 20249. (Contributed by AV, 3-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = ( Β·π βπ ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ (π β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) & β’ β = (π β πΎ, π£ β π β¦ (π£ Β· π )) & β’ πΏ = (π sSet β¨( Β·π βndx), β β©) β β’ (πΉ β CRing β πΏ β LMod) | ||
Syntax | clss 20315 | Extend class notation with linear subspaces of a left module or left vector space. |
class LSubSp | ||
Definition | df-lss 20316* | Define the set of linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) |
β’ LSubSp = (π€ β V β¦ {π β (π« (Baseβπ€) β {β }) β£ βπ₯ β (Baseβ(Scalarβπ€))βπ β π βπ β π ((π₯( Β·π βπ€)π)(+gβπ€)π) β π }) | ||
Theorem | lssset 20317* | The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 15-Jul-2014.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) β β’ (π β π β π = {π β (π« π β {β }) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) | ||
Theorem | islss 20318* | The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) β β’ (π β π β (π β π β§ π β β β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) | ||
Theorem | islssd 20319* | Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ (π β πΉ = (Scalarβπ)) & β’ (π β π΅ = (BaseβπΉ)) & β’ (π β π = (Baseβπ)) & β’ (π β + = (+gβπ)) & β’ (π β Β· = ( Β·π βπ)) & β’ (π β π = (LSubSpβπ)) & β’ (π β π β π) & β’ (π β π β β ) & β’ ((π β§ (π₯ β π΅ β§ π β π β§ π β π)) β ((π₯ Β· π) + π) β π) β β’ (π β π β π) | ||
Theorem | lssss 20320 | A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β π β π β π) | ||
Theorem | lssel 20321 | A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) β β’ ((π β π β§ π β π) β π β π) | ||
Theorem | lss1 20322 | The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β π β π) | ||
Theorem | lssuni 20323 | The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) β β’ (π β βͺ π = π) | ||
Theorem | lssn0 20324 | A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (LSubSpβπ) β β’ (π β π β π β β ) | ||
Theorem | 00lss 20325 | The empty structure has no subspaces (for use with fvco4i 6938). (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ β = (LSubSpββ ) | ||
Theorem | lsscl 20326 | Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) β β’ ((π β π β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) + π) β π) | ||
Theorem | lssvsubcl 20327 | Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ β = (-gβπ) & β’ π = (LSubSpβπ) β β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π β π) β π) | ||
Theorem | lssvancl1 20328 | Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 20520. Can it be used along with lspsnne1 20501, lspsnne2 20502 to shorten this proof? (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β Β¬ (π + π) β π) | ||
Theorem | lssvancl2 20329 | Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 20-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β Β¬ (π + π) β π) | ||
Theorem | lss0cl 20330 | 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 20331 | 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 20332 | The zero subspace is included in every subspace. (sh0le 30168 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β { 0 } β π) | ||
Theorem | lssle0 20333 | No subspace is smaller than the zero subspace. (shle0 30170 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β { 0 } β π = { 0 })) | ||
Theorem | lssne0 20334* | A nonzero subspace has a nonzero vector. (shne0i 30176 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ (π β π β (π β { 0 } β βπ¦ β π π¦ β 0 )) | ||
Theorem | lssvneln0 20335 | 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 20336 | 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 20337* | Conclude subspace ordering from nonzero vector membership. (ssrdv 3949 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π₯ β (π β { 0 })) β (π₯ β π β π₯ β π)) β β’ (π β π β π) | ||
Theorem | lssvacl 20338 | 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 20339 | 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 20340 | Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
β’ π = (LSubSpβπ) & β’ π = (invgβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β π) | ||
Theorem | lsssubg 20341 | All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) | ||
Theorem | lsssssubg 20342 | All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (LSubSpβπ) β β’ (π β LMod β π β (SubGrpβπ)) | ||
Theorem | islss3 20343 | 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 20344 | A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β LMod) | ||
Theorem | lsslss 20345 | The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β π β (π β π β§ π β π))) | ||
Theorem | islss4 20346* | 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 20347* | 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 20348 | 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 20349 | 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 20350 | 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 20351 | Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β π β (ACSβπ΅)) | ||
Theorem | prdsvscacl 20352* | 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 20353* | 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 20354 | A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LMod β§ πΌ β π) β π β LMod) | ||
Syntax | clspn 20355 | Extend class notation with span of a set of vectors. |
class LSpan | ||
Definition | df-lsp 20356* | 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 20357* | The span function for a left vector space (or a left module). (df-span 30037 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β π β π = (π β π« π β¦ β© {π‘ β π β£ π β π‘})) | ||
Theorem | lspf 20358 | The span operator on a left module maps subsets to subsets. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β π:π« πβΆπ) | ||
Theorem | lspval 20359* | The span of a set of vectors (in a left module). (spanval 30061 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = β© {π‘ β π β£ π β π‘}) | ||
Theorem | lspcl 20360 | The span of a set of vectors is a subspace. (spancl 30064 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) | ||
Theorem | lspsncl 20361 | The span of a singleton is a subspace (frequently used special case of lspcl 20360). (Contributed by NM, 17-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β π) | ||
Theorem | lspprcl 20362 | The span of a pair is a subspace (frequently used special case of lspcl 20360). (Contributed by NM, 11-Apr-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) | ||
Theorem | lsptpcl 20363 | The span of an unordered triple is a subspace (frequently used special case of lspcl 20360). (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π, π}) β π) | ||
Theorem | lspsnsubg 20364 | The span of a singleton is an additive subgroup (frequently used special case of lspcl 20360). (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) | ||
Theorem | 00lsp 20365 | fvco4i 6938 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ β = (LSpanββ ) | ||
Theorem | lspid 20366 | The span of a subspace is itself. (spanid 30075 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = π) | ||
Theorem | lspssv 20367 | 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 20368 | Span preserves subset ordering. (spanss 30076 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β (πβπ)) | ||
Theorem | lspssid 20369 | A set of vectors is a subset of its span. (spanss2 30073 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβπ)) | ||
Theorem | lspidm 20370 | 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 20371 | 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 20372 | 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 20373 | Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΎ = (LSpanβπ) & β’ πΉ = (mrClsβπ) β β’ (π β LMod β πΎ = πΉ) | ||
Theorem | lspsnss 20374 | The span of the singleton of a subspace member is included in the subspace. (spansnss 30299 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβ{π}) β π) | ||
Theorem | lspsnel3 20375 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 30300 analog.) (Contributed by NM, 4-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) β β’ (π β π β π) | ||
Theorem | lspprss 20376 | 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 20377 | A vector belongs to the span of its singleton. (spansnid 30291 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβ{π})) | ||
Theorem | lspsnel6 20378 | 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 20379 | 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 20380 | 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 20381 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprid2 20382 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprvacl 20383 | The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π + π) β (πβ{π, π})) | ||
Theorem | lssats2 20384* | A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β π = βͺ π₯ β π (πβ{π₯})) | ||
Theorem | lspsneli 20385 | A scalar product with a vector belongs to the span of its singleton. (spansnmul 30292 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) β β’ (π β (π΄ Β· π) β (πβ{π})) | ||
Theorem | lspsn 20386* | 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 20387* | Member of span of the singleton of a vector. (elspansn 30294 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnvsi 20388 | 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 20389* | Comparable spans of singletons must have proportional vectors. See lspsneq 20506 for equal span version. (Contributed by NM, 7-Jun-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnneg 20390 | 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 20391 | Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{(π β π)}) = (πβ{(π β π)})) | ||
Theorem | lspsn0 20392 | Span of the singleton of the zero vector. (spansn0 30269 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πβ{ 0 }) = { 0 }) | ||
Theorem | lsp0 20393 | Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πββ ) = { 0 }) | ||
Theorem | lspuni0 20394 | Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β βͺ (πββ ) = 0 ) | ||
Theorem | lspun0 20395 | The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (πβ(π βͺ { 0 })) = (πβπ)) | ||
Theorem | lspsneq0 20396 | 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 20397 | 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 20398 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π + π) β 0 ) | ||
Theorem | lsslsp 20399 | 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 20400 | 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 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |