![]() |
Metamath
Proof Explorer Theorem List (p. 206 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmod0vlid 20501 | Left identity law for the zero vector. (hvaddlid 30271 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β LMod β§ π β π) β ( 0 + π) = π) | ||
Theorem | lmod0vrid 20502 | Right identity law for the zero vector. (ax-hvaddid 30252 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β LMod β§ π β π) β (π + 0 ) = π) | ||
Theorem | lmod0vid 20503 | Identity equivalent to the value of the zero vector. Provides a convenient way to compute the value. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β LMod β§ π β π) β ((π + π) = π β 0 = π)) | ||
Theorem | lmod0vs 20504 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30258 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) β β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) | ||
Theorem | lmodvs0 20505 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 30272 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπ) β β’ ((π β LMod β§ π β πΎ) β (π Β· 0 ) = 0 ) | ||
Theorem | lmodvsmmulgdi 20506 | Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ πΈ = (.gβπΉ) β β’ ((π β LMod β§ (πΆ β πΎ β§ π β β0 β§ π β π)) β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π)) | ||
Theorem | lmodfopnelem1 20507 | Lemma 1 for lmodfopne 20509. (Contributed by AV, 2-Oct-2021.) |
β’ Β· = ( Β·sf βπ) & β’ + = (+πβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ ((π β LMod β§ + = Β· ) β π = πΎ) | ||
Theorem | lmodfopnelem2 20508 | Lemma 2 for lmodfopne 20509. (Contributed by AV, 2-Oct-2021.) |
β’ Β· = ( Β·sf βπ) & β’ + = (+πβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) β β’ ((π β LMod β§ + = Β· ) β ( 0 β π β§ 1 β π)) | ||
Theorem | lmodfopne 20509 | The (functionalized) operations of a left module (over a nonzero ring) cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 2-Oct-2021.) |
β’ Β· = ( Β·sf βπ) & β’ + = (+πβπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) β β’ ((π β LMod β§ 1 β 0 ) β + β Β· ) | ||
Theorem | lcomf 20510 | A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ) & β’ (π β π β LMod) & β’ (π β πΊ:πΌβΆπΎ) & β’ (π β π»:πΌβΆπ΅) & β’ (π β πΌ β π) β β’ (π β (πΊ βf Β· π»):πΌβΆπ΅) | ||
Theorem | lcomfsupp 20511 | A linear-combination sum is finitely supported if the coefficients are. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by AV, 15-Jul-2019.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ) & β’ (π β π β LMod) & β’ (π β πΊ:πΌβΆπΎ) & β’ (π β π»:πΌβΆπ΅) & β’ (π β πΌ β π) & β’ 0 = (0gβπ) & β’ π = (0gβπΉ) & β’ (π β πΊ finSupp π) β β’ (π β (πΊ βf Β· π») finSupp 0 ) | ||
Theorem | lmodvnegcl 20512 | Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) | ||
Theorem | lmodvnegid 20513 | Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (invgβπ) β β’ ((π β LMod β§ π β π) β (π + (πβπ)) = 0 ) | ||
Theorem | lmodvneg1 20514 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπΉ) & β’ π = (invgβπΉ) β β’ ((π β LMod β§ π β π) β ((πβ 1 ) Β· π) = (πβπ)) | ||
Theorem | lmodvsneg 20515 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (invgβπΉ) & β’ (π β π β LMod) & β’ (π β π β π΅) & β’ (π β π β πΎ) β β’ (π β (πβ(π Β· π)) = ((πβπ ) Β· π)) | ||
Theorem | lmodvsubcl 20516 | Closure of vector subtraction. (hvsubcl 30265 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) | ||
Theorem | lmodcom 20517 | Left module vector sum is commutative. (Contributed by GΓ©rard Lang, 25-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π + π) = (π + π)) | ||
Theorem | lmodabl 20518 | A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
β’ (π β LMod β π β Abel) | ||
Theorem | lmodcmn 20519 | A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.) |
β’ (π β LMod β π β CMnd) | ||
Theorem | lmodnegadd 20520 | Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ((π΄ Β· π) + (π΅ Β· π))) = (((πΌβπ΄) Β· π) + ((πΌβπ΅) Β· π))) | ||
Theorem | lmod4 20521 | Commutative/associative law for left module vector sum. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β LMod β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
Theorem | lmodvsubadd 20522 | Relationship between vector subtraction and addition. (hvsubadd 30325 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | lmodvaddsub4 20523 | Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) = (πΆ + π·) β (π΄ β πΆ) = (π· β π΅))) | ||
Theorem | lmodvpncan 20524 | Addition/subtraction cancellation law for vectors. (hvpncan 30287 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ + π΅) β π΅) = π΄) | ||
Theorem | lmodvnpcan 20525 | Cancellation law for vector subtraction (npcan 11468 analog). (Contributed by NM, 19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ β π΅) + π΅) = π΄) | ||
Theorem | lmodvsubval2 20526 | Value of vector subtraction in terms of addition. (hvsubval 30264 analog.) (Contributed by NM, 31-Mar-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπΉ) & β’ 1 = (1rβπΉ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) = (π΄ + ((πβ 1 ) Β· π΅))) | ||
Theorem | lmodsubvs 20527 | Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (invgβπΉ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π΄ Β· π)) = (π + ((πβπ΄) Β· π))) | ||
Theorem | lmodsubdi 20528 | Scalar multiplication distributive law for subtraction. (hvsubdistr1 30297 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π΄ Β· (π β π)) = ((π΄ Β· π) β (π΄ Β· π))) | ||
Theorem | lmodsubdir 20529 | Scalar multiplication distributive law for subtraction. (hvsubdistr2 30298 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β ((π΄ππ΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) | ||
Theorem | lmodsubeq0 20530 | If the difference between two vectors is zero, they are equal. (hvsubeq0 30316 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ β π΅) = 0 β π΄ = π΅)) | ||
Theorem | lmodsubid 20531 | Subtraction of a vector from itself. (hvsubid 30274 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ β = (-gβπ) β β’ ((π β LMod β§ π΄ β π) β (π΄ β π΄) = 0 ) | ||
Theorem | lmodvsghm 20532* | 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 20533* | If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 20534 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 20534* | 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 20535* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 20128, 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 20536* | 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 20537* | A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe 21819. (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 20538* | Lemma for rmodislmod 20539. This is the part of the proof of rmodislmod 20539 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 20539* | 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 20472 of a left module, see also islmod 20474. (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 20540* | Obsolete version of rmodislmod 20539 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 20472 of a left module, see also islmod 20474. (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 20541 | Extend class notation with linear subspaces of a left module or left vector space. |
class LSubSp | ||
Definition | df-lss 20542* | 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 20543* | 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 20544* | 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 20545* | 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 20546 | A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β π β π β π) | ||
Theorem | lssel 20547 | A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) β β’ ((π β π β§ π β π) β π β π) | ||
Theorem | lss1 20548 | 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 20549 | The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) β β’ (π β βͺ π = π) | ||
Theorem | lssn0 20550 | A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (LSubSpβπ) β β’ (π β π β π β β ) | ||
Theorem | 00lss 20551 | The empty structure has no subspaces (for use with fvco4i 6992). (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ β = (LSubSpββ ) | ||
Theorem | lsscl 20552 | Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) β β’ ((π β π β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) + π) β π) | ||
Theorem | lssvsubcl 20553 | 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 20554 | 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 20748. Can it be used along with lspsnne1 20729, lspsnne2 20730 to shorten this proof? (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β Β¬ (π + π) β π) | ||
Theorem | lssvancl2 20555 | 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 20556 | 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 20557 | 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 20558 | The zero subspace is included in every subspace. (sh0le 30688 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β { 0 } β π) | ||
Theorem | lssle0 20559 | No subspace is smaller than the zero subspace. (shle0 30690 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β { 0 } β π = { 0 })) | ||
Theorem | lssne0 20560* | A nonzero subspace has a nonzero vector. (shne0i 30696 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ (π β π β (π β { 0 } β βπ¦ β π π¦ β 0 )) | ||
Theorem | lssvneln0 20561 | 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 20562 | 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 20563* | Conclude subspace ordering from nonzero vector membership. (ssrdv 3988 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π₯ β (π β { 0 })) β (π₯ β π β π₯ β π)) β β’ (π β π β π) | ||
Theorem | lssvacl 20564 | 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 20565 | 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 20566 | Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
β’ π = (LSubSpβπ) & β’ π = (invgβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β π) | ||
Theorem | lsssubg 20567 | All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) | ||
Theorem | lsssssubg 20568 | All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (LSubSpβπ) β β’ (π β LMod β π β (SubGrpβπ)) | ||
Theorem | islss3 20569 | 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 20570 | A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β LMod) | ||
Theorem | lsslss 20571 | The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β π β (π β π β§ π β π))) | ||
Theorem | islss4 20572* | 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 20573* | 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 20574 | 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 20575 | 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 20576 | 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 20577 | Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSubSpβπ) β β’ (π β LMod β π β (ACSβπ΅)) | ||
Theorem | prdsvscacl 20578* | 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 20579* | 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 20580 | A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LMod β§ πΌ β π) β π β LMod) | ||
Syntax | clspn 20581 | Extend class notation with span of a set of vectors. |
class LSpan | ||
Definition | df-lsp 20582* | 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 20583* | The span function for a left vector space (or a left module). (df-span 30557 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β π β π = (π β π« π β¦ β© {π‘ β π β£ π β π‘})) | ||
Theorem | lspf 20584 | 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 20585* | The span of a set of vectors (in a left module). (spanval 30581 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = β© {π‘ β π β£ π β π‘}) | ||
Theorem | lspcl 20586 | The span of a set of vectors is a subspace. (spancl 30584 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) | ||
Theorem | lspsncl 20587 | The span of a singleton is a subspace (frequently used special case of lspcl 20586). (Contributed by NM, 17-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β π) | ||
Theorem | lspprcl 20588 | The span of a pair is a subspace (frequently used special case of lspcl 20586). (Contributed by NM, 11-Apr-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) | ||
Theorem | lsptpcl 20589 | The span of an unordered triple is a subspace (frequently used special case of lspcl 20586). (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π, π}) β π) | ||
Theorem | lspsnsubg 20590 | The span of a singleton is an additive subgroup (frequently used special case of lspcl 20586). (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) | ||
Theorem | 00lsp 20591 | fvco4i 6992 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ β = (LSpanββ ) | ||
Theorem | lspid 20592 | The span of a subspace is itself. (spanid 30595 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = π) | ||
Theorem | lspssv 20593 | 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 20594 | Span preserves subset ordering. (spanss 30596 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β (πβπ)) | ||
Theorem | lspssid 20595 | A set of vectors is a subset of its span. (spanss2 30593 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβπ)) | ||
Theorem | lspidm 20596 | 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 20597 | 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 20598 | 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 20599 | Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΎ = (LSpanβπ) & β’ πΉ = (mrClsβπ) β β’ (π β LMod β πΎ = πΉ) | ||
Theorem | lspsnss 20600 | The span of the singleton of a subspace member is included in the subspace. (spansnss 30819 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβ{π}) β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |