Type | Label | Description |
Statement |
|
Theorem | scaffvalg 13401* |
The scalar multiplication operation as a function. (Contributed by
Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β = (
Β·sf βπ)
& β’ Β· = (
Β·π βπ) β β’ (π β π β β = (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦))) |
|
Theorem | scafvalg 13402 |
The scalar multiplication operation as a function. (Contributed by
Mario Carneiro, 5-Oct-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β = (
Β·sf βπ)
& β’ Β· = (
Β·π βπ) β β’ ((π β π β§ π β πΎ β§ π β π΅) β (π β π) = (π Β· π)) |
|
Theorem | scafeqg 13403 |
If the scalar multiplication operation is already a function, the
functionalization of it is equal to the original operation.
(Contributed by Mario Carneiro, 5-Oct-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β = (
Β·sf βπ)
& β’ Β· = (
Β·π βπ) β β’ ((π β π β§ Β· Fn (πΎ Γ π΅)) β β = Β·
) |
|
Theorem | scaffng 13404 |
The scalar multiplication operation is a function. (Contributed by
Mario Carneiro, 5-Oct-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β = (
Β·sf βπ) β β’ (π β π β β Fn (πΎ Γ π΅)) |
|
Theorem | lmodscaf 13405 |
The scalar multiplication operation is a function. (Contributed by
Mario Carneiro, 5-Oct-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β = (
Β·sf βπ) β β’ (π β LMod β β :(πΎ Γ π΅)βΆπ΅) |
|
Theorem | lmodvsdi 13406 |
Distributive law for scalar product (left-distributivity). (Contributed
by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ (π
β πΎ β§ π β π β§ π β π)) β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π))) |
|
Theorem | lmodvsdir 13407 |
Distributive law for scalar product (right-distributivity).
(Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro,
22-Sep-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΎ = (BaseβπΉ)
& ⒠⨣ =
(+gβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π
β πΎ β§ π β π)) β ((π ⨣ π
) Β· π) = ((π Β· π) + (π
Β· π))) |
|
Theorem | lmodvsass 13408 |
Associative law for scalar product. (Contributed by NM, 10-Jan-2014.)
(Revised by Mario Carneiro, 22-Sep-2015.)
|
β’ π = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΎ = (BaseβπΉ)
& β’ Γ =
(.rβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π
β πΎ β§ π β π)) β ((π Γ π
) Β· π) = (π Β· (π
Β· π))) |
|
Theorem | lmod0cl 13409 |
The ring zero in a left module belongs to the set of scalars.
(Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ 0 =
(0gβπΉ) β β’ (π β LMod β 0 β πΎ) |
|
Theorem | lmod1cl 13410 |
The ring unity in a left module belongs to the set of scalars.
(Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ 1 =
(1rβπΉ) β β’ (π β LMod β 1 β πΎ) |
|
Theorem | lmodvs1 13411 |
Scalar product with the ring unity. (Contributed by NM, 10-Jan-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ 1 =
(1rβπΉ) β β’ ((π β LMod β§ π β π) β ( 1 Β· π) = π) |
|
Theorem | lmod0vcl 13412 |
The zero vector is a vector. (Contributed by NM, 10-Jan-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ 0 =
(0gβπ) β β’ (π β LMod β 0 β π) |
|
Theorem | lmod0vlid 13413 |
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 13414 |
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 13415 |
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 13416 |
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 13417 |
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 13418 |
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 13419 |
Lemma 1 for lmodfopne 13421. (Contributed by AV, 2-Oct-2021.)
|
β’ Β· = (
Β·sf βπ)
& β’ + =
(+πβπ)
& β’ π = (Baseβπ)
& β’ π = (Scalarβπ)
& β’ πΎ = (Baseβπ) β β’ ((π β LMod β§ + = Β· ) β π = πΎ) |
|
Theorem | lmodfopnelem2 13420 |
Lemma 2 for lmodfopne 13421. (Contributed by AV, 2-Oct-2021.)
|
β’ Β· = (
Β·sf βπ)
& β’ + =
(+πβπ)
& β’ π = (Baseβπ)
& β’ π = (Scalarβπ)
& β’ πΎ = (Baseβπ)
& β’ 0 =
(0gβπ)
& β’ 1 =
(1rβπ) β β’ ((π β LMod β§ + = Β· ) β ( 0 β π β§ 1 β π)) |
|
Theorem | lmodfopne 13421 |
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 13422 |
A linear-combination sum is a function. (Contributed by Stefan O'Rear,
28-Feb-2015.)
|
β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ Β· = (
Β·π βπ)
& β’ π΅ = (Baseβπ)
& β’ (π β π β LMod) & β’ (π β πΊ:πΌβΆπΎ)
& β’ (π β π»:πΌβΆπ΅)
& β’ (π β πΌ β π) β β’ (π β (πΊ βπ Β· π»):πΌβΆπ΅) |
|
Theorem | lmodvnegcl 13423 |
Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised
by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (invgβπ) β β’ ((π β LMod β§ π β π) β (πβπ) β π) |
|
Theorem | lmodvnegid 13424 |
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 13425 |
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 13426 |
Multiplication of a vector by a negated scalar. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
β’ π΅ = (Baseβπ)
& β’ πΉ = (Scalarβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (invgβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (invgβπΉ)
& β’ (π β π β LMod) & β’ (π β π β π΅)
& β’ (π β π
β πΎ) β β’ (π β (πβ(π
Β· π)) = ((πβπ
) Β· π)) |
|
Theorem | lmodvsubcl 13427 |
Closure of vector subtraction. (Contributed by NM, 31-Mar-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
|
Theorem | lmodcom 13428 |
Left module vector sum is commutative. (Contributed by GΓ©rard
Lang, 25-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π + π) = (π + π)) |
|
Theorem | lmodabl 13429 |
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 13430 |
A left module is a commutative monoid under addition. (Contributed by
NM, 7-Jan-2015.)
|
β’ (π β LMod β π β CMnd) |
|
Theorem | lmodnegadd 13431 |
Distribute negation through addition of scalar products. (Contributed
by NM, 9-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (invgβπ)
& β’ π
= (Scalarβπ)
& β’ πΎ = (Baseβπ
)
& β’ πΌ = (invgβπ
)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π΅ β πΎ)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ((π΄ Β· π) + (π΅ Β· π))) = (((πΌβπ΄) Β· π) + ((πΌβπ΅) Β· π))) |
|
Theorem | lmod4 13432 |
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 13433 |
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 13434 |
Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) = (πΆ + π·) β (π΄ β πΆ) = (π· β π΅))) |
|
Theorem | lmodvpncan 13435 |
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 13436 |
Cancellation law for vector subtraction (Contributed by NM,
19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ) β β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β ((π΄ β π΅) + π΅) = π΄) |
|
Theorem | lmodvsubval2 13437 |
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 13438 |
Subtraction of a scalar product in terms of addition. (Contributed by
NM, 9-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ + =
(+gβπ)
& β’ β =
(-gβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ π = (invgβπΉ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (π β (π΄ Β· π)) = (π + ((πβπ΄) Β· π))) |
|
Theorem | lmodsubdi 13439 |
Scalar multiplication distributive law for subtraction. (Contributed by
NM, 2-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β =
(-gβπ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (π΄ Β· (π β π)) = ((π΄ Β· π) β (π΄ Β· π))) |
|
Theorem | lmodsubdir 13440 |
Scalar multiplication distributive law for subtraction. (Contributed by
NM, 2-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ Β· = (
Β·π βπ)
& β’ πΉ = (Scalarβπ)
& β’ πΎ = (BaseβπΉ)
& β’ β =
(-gβπ)
& β’ π = (-gβπΉ)
& β’ (π β π β LMod) & β’ (π β π΄ β πΎ)
& β’ (π β π΅ β πΎ)
& β’ (π β π β π) β β’ (π β ((π΄ππ΅) Β· π) = ((π΄ Β· π) β (π΅ Β· π))) |
|
Theorem | lmodsubeq0 13441 |
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 13442 |
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 13443* |
If two structures have the same components (properties), one is a left
module iff the other one is. This version of lmodpropd 13444 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 13444* |
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 13445* |
Lemma for rmodislmod 13446. This is the part of the proof of rmodislmod 13446
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 13446* |
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 13384 of a left module, see
also islmod 13386. (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 13447 |
Extend class notation with linear subspaces of a left module or left
vector space.
|
class LSubSp |
|
Definition | df-lssm 13448* |
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 | lsssetm 13449* |
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 13450* |
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 | islssmd 13451* |
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 13452 |
A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.)
(Revised by Mario Carneiro, 8-Jan-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ) β β’ ((π β π β§ π β π) β π β π) |
|
Theorem | lsselg 13453 |
A subspace member is a vector. (Contributed by NM, 11-Jan-2014.)
(Revised by Mario Carneiro, 8-Jan-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ) β β’ ((π β πΆ β§ π β π β§ π β π) β π β π) |
|
Theorem | lss1 13454 |
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 13455 |
The union of all subspaces is the vector space. (Contributed by NM,
13-Mar-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ (π β π β LMod)
β β’ (π β βͺ π = π) |
|
Theorem | lssclg 13456 |
Closure property of a subspace. (Contributed by NM, 8-Dec-2013.)
(Revised by Mario Carneiro, 8-Jan-2015.)
|
β’ πΉ = (Scalarβπ)
& β’ π΅ = (BaseβπΉ)
& β’ + =
(+gβπ)
& β’ Β· = (
Β·π βπ)
& β’ π = (LSubSpβπ) β β’ ((π β πΆ β§ π β π β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) + π) β π) |
|
Theorem | lssvsubcl 13457 |
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 13458 |
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 13459 |
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 13460 |
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 13461 |
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 13462 |
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 13463 |
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 13464 |
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 13465 |
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 | lssvacl 13466 |
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 13467 |
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 13468 |
Closure of negative vectors in a subspace. (Contributed by Stefan
O'Rear, 11-Dec-2014.)
|
β’ π = (LSubSpβπ)
& β’ π = (invgβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β π) |
|
Theorem | lsssubg 13469 |
All subspaces are subgroups. (Contributed by Stefan O'Rear,
11-Dec-2014.)
|
β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
|
Theorem | lsssssubg 13470 |
All subspaces are subgroups. (Contributed by Mario Carneiro,
19-Apr-2016.)
|
β’ π = (LSubSpβπ) β β’ (π β LMod β π β (SubGrpβπ)) |
|
Theorem | islss3 13471 |
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 13472 |
A submodule is a module. (Contributed by Stefan O'Rear,
12-Dec-2014.)
|
β’ π = (π βΎs π)
& β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β π β LMod) |
|
Theorem | lsslss 13473 |
The subspaces of a subspace are the smaller subspaces. (Contributed by
Stefan O'Rear, 12-Dec-2014.)
|
β’ π = (π βΎs π)
& β’ π = (LSubSpβπ)
& β’ π = (LSubSpβπ) β β’ ((π β LMod β§ π β π) β (π β π β (π β π β§ π β π))) |
|
Theorem | islss4 13474* |
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 13475* |
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 13476* |
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 13477 |
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 13478 |
Extend class notation with span of a set of vectors.
|
class LSpan |
|
Definition | df-lsp 13479* |
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 13480* |
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 13481 |
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 13482* |
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 13483 |
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 13484 |
The span of a singleton is a subspace (frequently used special case of
lspcl 13483). (Contributed by NM, 17-Jul-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β π) |
|
Theorem | lspprcl 13485 |
The span of a pair is a subspace (frequently used special case of
lspcl 13483). (Contributed by NM, 11-Apr-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) |
|
Theorem | lsptpcl 13486 |
The span of an unordered triple is a subspace (frequently used special
case of lspcl 13483). (Contributed by NM, 22-May-2015.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (πβ{π, π, π}) β π) |
|
Theorem | lspsnsubg 13487 |
The span of a singleton is an additive subgroup (frequently used special
case of lspcl 13483). (Contributed by Mario Carneiro,
21-Apr-2016.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) |
|
Theorem | lspid 13488 |
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 13489 |
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 13490 |
Span preserves subset ordering. (Contributed by NM, 11-Dec-2013.)
(Revised by Mario Carneiro, 19-Jun-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβπ) β (πβπ)) |
|
Theorem | lspssid 13491 |
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 13492 |
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 13493 |
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 13494 |
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 13495 |
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 13496 |
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 13497 |
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 13498 |
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 13499 |
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 13500 |
Relationship between a vector and the 1-dim (or 0-dim) subspace it
generates. (Contributed by NM, 8-Aug-2014.)
|
β’ π = (Baseβπ)
& β’ π = (LSubSpβπ)
& β’ π = (LSpanβπ)
& β’ (π β π β LMod) & β’ (π β π β π)
& β’ (π β π β π) β β’ (π β (π β π β (πβ{π}) β π)) |