Type | Label | Description |
Statement |
|
Theorem | lmod0vlid 13601 |
Left identity law for the zero vector. (Contributed by NM,
10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ 0 =
(0gβπ) β β’ ((π β LMod β§ π β π) β ( 0 + π) = π) |
|
Theorem | lmod0vrid 13602 |
Right identity law for the zero vector. (Contributed by NM,
10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ 0 =
(0gβπ) β β’ ((π β LMod β§ π β π) β (π + 0 ) = π) |
|
Theorem | lmod0vid 13603 |
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 13604 |
Zero times a vector is the zero vector. Equation 1a of [Kreyszig]
p. 51. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (0gβπΉ)
& β’ 0 =
(0gβπ) β β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) |
|
Theorem | lmodvs0 13605 |
Anything times the zero vector is the zero vector. Equation 1b of
[Kreyszig] p. 51. (Contributed by NM,
12-Jan-2014.) (Revised by Mario
Carneiro, 19-Jun-2014.)
|
β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΎ = (BaseβπΉ)
& β’ 0 =
(0gβπ) β β’ ((π β LMod β§ π β πΎ) β (π Β· 0 ) = 0 ) |
|
Theorem | lmodvsmmulgdi 13606 |
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 13607 |
Lemma 1 for lmodfopne 13609. (Contributed by AV, 2-Oct-2021.)
|
β’ Β· = (
Β·sf βπ)
& β’ + =
(+πβπ)
& β’ π = (Baseβπ)
& β’ π = (Scalarβπ)
& β’ πΎ = (Baseβπ) β β’ ((π β LMod β§ + = Β· ) β π = πΎ) |
|
Theorem | lmodfopnelem2 13608 |
Lemma 2 for lmodfopne 13609. (Contributed by AV, 2-Oct-2021.)
|
β’ Β· = (
Β·sf βπ)
& β’ + =
(+πβπ)
& β’ π = (Baseβπ)
& β’ π = (Scalarβπ)
& β’ πΎ = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ 1 =
(1rβπ) β β’ ((π β LMod β§ + = Β· ) β ( 0 β π β§ 1 β π)) |
|
Theorem | lmodfopne 13609 |
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 13610 |
A linear-combination sum is a function. (Contributed by Stefan O'Rear,
28-Feb-2015.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ Β· = (
Β·π βπ)
& β’ π΅ = (Baseβπ)
& β’ (π β π β LMod) & β’ (π β πΊ:πΌβΆπΎ)
& β’ (π β π»:πΌβΆπ΅)
& β’ (π β πΌ β π) β β’ (π β (πΊ βπ Β· π»):πΌβΆπ΅) |
|
Theorem | lmodvnegcl 13611 |
Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised
by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (invgβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) |
|
Theorem | lmodvnegid 13612 |
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 13613 |
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 13614 |
Multiplication of a vector by a negated scalar. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (invgβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (invgβπΉ)
& β’ (π β π β LMod) & β’ (π β π β π΅)
& β’ (π β π
β πΎ) β β’ (π β (πβ(π
Β· π)) = ((πβπ
) Β· π)) |
|
Theorem | lmodvsubcl 13615 |
Closure of vector subtraction. (Contributed by NM, 31-Mar-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
|
Theorem | lmodcom 13616 |
Left module vector sum is commutative. (Contributed by GΓ©rard
Lang, 25-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π + π) = (π + π)) |
|
Theorem | lmodabl 13617 |
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 13618 |
A left module is a commutative monoid under addition. (Contributed by
NM, 7-Jan-2015.)
|
β’ (π β LMod β π β CMnd) |
|
Theorem | lmodnegadd 13619 |
Distribute negation through addition of scalar products. (Contributed
by NM, 9-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (invgβπ)
& β’ π
= (Scalarβπ)
& β’ πΎ = (Baseβπ
)
& β’ πΌ = (invgβπ
)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π΅ β πΎ)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ((π΄ Β· π) + (π΅ Β· π))) = (((πΌβπ΄) Β· π) + ((πΌβπ΅) Β· π))) |
|
Theorem | lmod4 13620 |
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 13621 |
Relationship between vector subtraction and addition. (Contributed by
NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β π΅) = πΆ β (π΅ + πΆ) = π΄)) |
|
Theorem | lmodvaddsub4 13622 |
Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) = (πΆ + π·) β (π΄ β πΆ) = (π· β π΅))) |
|
Theorem | lmodvpncan 13623 |
Addition/subtraction cancellation law for vectors. (Contributed by NM,
16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ + π΅) β π΅) = π΄) |
|
Theorem | lmodvnpcan 13624 |
Cancellation law for vector subtraction (Contributed by NM,
19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ β π΅) + π΅) = π΄) |
|
Theorem | lmodvsubval2 13625 |
Value of vector subtraction in terms of addition. (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 13626 |
Subtraction of a scalar product in terms of addition. (Contributed by
NM, 9-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (invgβπΉ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (π β (π΄ Β· π)) = (π + ((πβπ΄) Β· π))) |
|
Theorem | lmodsubdi 13627 |
Scalar multiplication distributive law for subtraction. (Contributed by
NM, 2-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β =
(-gβπ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (π΄ Β· (π β π)) = ((π΄ Β· π) β (π΄ Β· π))) |
|
Theorem | lmodsubdir 13628 |
Scalar multiplication distributive law for subtraction. (Contributed by
NM, 2-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β =
(-gβπ)
& β’ π = (-gβπΉ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π΅ β πΎ)
& β’ (π β π β π) β β’ (π β ((π΄ππ΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) |
|
Theorem | lmodsubeq0 13629 |
If the difference between two vectors is zero, they are equal.
(Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ β π΅) = 0 β π΄ = π΅)) |
|
Theorem | lmodsubid 13630 |
Subtraction of a vector from itself. (Contributed by NM, 16-Apr-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π΄ β π) β (π΄ β π΄) = 0 ) |
|
Theorem | lmodprop2d 13631* |
If two structures have the same components (properties), one is a left
module iff the other one is. This version of lmodpropd 13632 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 13632* |
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 | rmodislmodlem 13633* |
Lemma for rmodislmod 13634. This is the part of the proof of rmodislmod 13634
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 13634* |
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 13572 of a left module, see
also islmod 13574. (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) |
|
7.5.2 Subspaces and spans in a left
module
|
|
Syntax | clss 13635 |
Extend class notation with linear subspaces of a left module or left
vector space.
|
class LSubSp |
|
Definition | df-lssm 13636* |
A linear subspace of a left module or left vector space is an inhabited
(in contrast to non-empty for non-intuitionistic logic) subset of the
base set of the left-module/vector space with a closure condition on
vector addition and scalar multiplication. (Contributed by NM,
8-Dec-2013.)
|
β’ LSubSp = (π€ β V β¦ {π β π« (Baseβπ€) β£ (βπ π β π β§ βπ₯ β (Baseβ(Scalarβπ€))βπ β π βπ β π ((π₯( Β·π
βπ€)π)(+gβπ€)π) β π )}) |
|
Theorem | lssex 13637 |
Existence of a linear subspace. (Contributed by Jim Kingdon,
27-Apr-2025.)
|
β’ (π β π β (LSubSpβπ) β V) |
|
Theorem | lssmex 13638 |
If a linear subspace is inhabited, the class it is built from is a set.
(Contributed by Jim Kingdon, 28-Apr-2025.)
|
β’ π = (LSubSpβπ) β β’ (π β π β π β V) |
|
Theorem | lsssetm 13639* |
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 | islssm 13640* |
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 | islssmg 13641* |
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.) Use islssm 13640 instead. (New usage is discouraged.)
|
β’ πΉ = (Scalarβπ)
& β’ π΅ = (BaseβπΉ)
& β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSubSpβπ) β β’ (π β π β (π β π β (π β π β§ βπ π β π β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π))) |
|
Theorem | islssmd 13642* |
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 | lssssg 13643 |
A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.)
(Revised by Mario Carneiro, 8-Jan-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ) β β’ ((π β π β§ π β π) β π β π) |
|
Theorem | lsselg 13644 |
A subspace member is a vector. (Contributed by NM, 11-Jan-2014.)
(Revised by Mario Carneiro, 8-Jan-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ) β β’ ((π β πΆ β§ π β π β§ π β π) β π β π) |
|
Theorem | lss1 13645 |
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 13646 |
The union of all subspaces is the vector space. (Contributed by NM,
13-Mar-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ (π β π β LMod)
β β’ (π β βͺ π = π) |
|
Theorem | lssclg 13647 |
Closure property of a subspace. (Contributed by NM, 8-Dec-2013.)
(Revised by Mario Carneiro, 8-Jan-2015.)
|
β’ πΉ = (Scalarβπ)
& β’ π΅ = (BaseβπΉ)
& β’ + =
(+gβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSubSpβπ) β β’ ((π β πΆ β§ π β π β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) + π) β π) |
|
Theorem | lssvacl 13648 |
Closure of vector addition in a subspace. (Contributed by NM,
11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ + =
(+gβπ)
& β’ π = (LSubSpβπ) β β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π + π) β π) |
|
Theorem | lssvsubcl 13649 |
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 13650 |
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, 14-May-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ π = (LSubSpβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β Β¬ π β π) β β’ (π β Β¬ (π + π) β π) |
|
Theorem | lssvancl2 13651 |
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 13652 |
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 13653 |
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 13654 |
The zero subspace is included in every subspace. (Contributed by NM,
27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β { 0 } β π) |
|
Theorem | lssle0 13655 |
No subspace is smaller than the zero subspace. (Contributed by NM,
20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ 0 =
(0gβπ)
& β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β { 0 } β π = { 0 })) |
|
Theorem | lssvneln0 13656 |
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 13657 |
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 | lssvscl 13658 |
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 13659 |
Closure of negative vectors in a subspace. (Contributed by Stefan
O'Rear, 11-Dec-2014.)
|
β’ π = (LSubSpβπ)
& β’ π = (invgβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β π) |
|
Theorem | lsssubg 13660 |
All subspaces are subgroups. (Contributed by Stefan O'Rear,
11-Dec-2014.)
|
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
|
Theorem | lsssssubg 13661 |
All subspaces are subgroups. (Contributed by Mario Carneiro,
19-Apr-2016.)
|
β’ π = (LSubSpβπ) β β’ (π β LMod β π β (SubGrpβπ)) |
|
Theorem | islss3 13662 |
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 13663 |
A submodule is a module. (Contributed by Stefan O'Rear,
12-Dec-2014.)
|
β’ π = (π βΎs π)
& β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β LMod) |
|
Theorem | lsslss 13664 |
The subspaces of a subspace are the smaller subspaces. (Contributed by
Stefan O'Rear, 12-Dec-2014.)
|
β’ π = (π βΎs π)
& β’ π = (LSubSpβπ)
& β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β π β (π β π β§ π β π))) |
|
Theorem | islss4 13665* |
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 13666* |
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 | lssintclm 13667* |
The intersection of an inhabited set of subspaces is a subspace.
(Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π΄ β π β§ βπ€ π€ β π΄) β β© π΄ β π) |
|
Theorem | lssincl 13668 |
The intersection of two subspaces is a subspace. (Contributed by NM,
7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π β© π) β π) |
|
Syntax | clspn 13669 |
Extend class notation with span of a set of vectors.
|
class LSpan |
|
Definition | df-lsp 13670* |
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 13671* |
The span function for a left vector space (or a left module).
(Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ (π β π β π = (π β π« π β¦ β©
{π‘ β π β£ π β π‘})) |
|
Theorem | lspf 13672 |
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 13673* |
The span of a set of vectors (in a left module). (Contributed by NM,
8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = β© {π‘ β π β£ π β π‘}) |
|
Theorem | lspcl 13674 |
The span of a set of vectors is a subspace. (Contributed by NM,
9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) |
|
Theorem | lspsncl 13675 |
The span of a singleton is a subspace (frequently used special case of
lspcl 13674). (Contributed by NM, 17-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β π) |
|
Theorem | lspprcl 13676 |
The span of a pair is a subspace (frequently used special case of
lspcl 13674). (Contributed by NM, 11-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) |
|
Theorem | lsptpcl 13677 |
The span of an unordered triple is a subspace (frequently used special
case of lspcl 13674). (Contributed by NM, 22-May-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ{π, π, π}) β π) |
|
Theorem | lspex 13678 |
Existence of the span of a set of vectors. (Contributed by Jim Kingdon,
25-Apr-2025.)
|
β’ (π β π β (LSpanβπ) β V) |
|
Theorem | lspsnsubg 13679 |
The span of a singleton is an additive subgroup (frequently used special
case of lspcl 13674). (Contributed by Mario Carneiro,
21-Apr-2016.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) |
|
Theorem | lspid 13680 |
The span of a subspace is itself. (Contributed by NM, 15-Dec-2013.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβπ) = π) |
|
Theorem | lspssv 13681 |
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 13682 |
Span preserves subset ordering. (Contributed by NM, 11-Dec-2013.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β (πβπ)) |
|
Theorem | lspssid 13683 |
A set of vectors is a subset of its span. (Contributed by NM,
6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβπ)) |
|
Theorem | lspidm 13684 |
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 13685 |
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 13686 |
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 | lspsnss 13687 |
The span of the singleton of a subspace member is included in the
subspace. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro,
4-Sep-2014.)
|
β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβ{π}) β π) |
|
Theorem | lspsnel3 13688 |
A member of the span of the singleton of a vector is a member of a
subspace containing the vector. (Contributed by NM, 4-Jul-2014.)
|
β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β π β (πβ{π})) β β’ (π β π β π) |
|
Theorem | lspprss 13689 |
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 13690 |
A vector belongs to the span of its singleton. (Contributed by NM,
9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβ{π})) |
|
Theorem | lspsnel6 13691 |
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 13692 |
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 13693 |
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 13694 |
A member of a pair of vectors belongs to their span. (Contributed by
NM, 14-May-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β π β (πβ{π, π})) |
|
Theorem | lspprid2 13695 |
A member of a pair of vectors belongs to their span. (Contributed by
NM, 14-May-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β π β (πβ{π, π})) |
|
Theorem | lspprvacl 13696 |
The sum of two vectors belongs to their span. (Contributed by NM,
20-May-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (π + π) β (πβ{π, π})) |
|
Theorem | lssats2 13697* |
A way to express atomisticity (a subspace is the union of its atoms).
(Contributed by NM, 3-Feb-2015.)
|
β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β π = βͺ
π₯ β π (πβ{π₯})) |
|
Theorem | lspsneli 13698 |
A scalar product with a vector belongs to the span of its singleton.
(Contributed by NM, 2-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π β π) β β’ (π β (π΄ Β· π) β (πβ{π})) |
|
Theorem | lspsn 13699* |
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 13700* |
Member of span of the singleton of a vector. (Contributed by NM,
22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β πΎ π = (π Β· π))) |