Metamath Proof Explorer


Table of Contents - 20.43.21.2. Linear combinations

According to Wikipedia ("Linear combination", 29-Mar-2019, https://en.wikipedia.org/wiki/Linear_combination) "In mathematics, a <b>linear combination</b> is an expression constructed from a set of terms by multiplying each term by a constant and adding the results (e.g., a linear combination of x and y would be any expression of the form ax + by, where a and b are constants). The concept of linear combinations is central to linear algebra and related fields of mathematics." In linear algebra, these "terms" are "vectors" (elements from vector spaces or left modules), and the constants are elements of the underlying field resp. ring. This corresponds to the definition in [Lang] p. 129: "Let M be a module over a ring A and let S be a subset of M. By a <b>linear combination</b> of elements of S (with <b>coefficients</b> in A) one means a sum &sum;<sub>x &isin;S</sub> a<sub>x</sub>x where {a<sub>x</sub>} is a set of elements of A, ...". In the definition in [Lang] p. 129, it is additionally claimed that "..., almost all of which [elements of A] are equal to 0.". This is not necessarily required in the following definition df-linc, but it is essential if additions and scalar multiplications of linear combinations are considered. Therefore, we define the set of all linear combinations with finite support in df-lco, so that we can show that such sets are submodules of the corresponding modules, see lincolss. <br> <b>Remark:</b>According to Wikipedia ("Linear span", 28-Apr-2019, https://en.wikipedia.org/wiki/Linear_span) "In linear algebra, the <b>linear span</b> (also called the linear hull or just span) of a set of vectors in a vector space [or module] is the intersection of all linear subspaces which each contain every vector in that set.", and "Alternately, the span of [a set] S may be defined as the set of all finite linear combinations of elements (vectors) of S". Whereas spans are defined according to the first approach in df-lsp, the set of all linear combinations as defined by df-lco follows the alternative approach. That both definitions are equivalent is shown by lspeqlco.

  1. clinc
  2. clinco
  3. df-linc
  4. df-lco
  5. lincop
  6. lincval
  7. dflinc2
  8. lcoop
  9. lcoval
  10. lincfsuppcl
  11. linccl
  12. lincval0
  13. lincvalsng
  14. lincvalsn
  15. lincvalpr
  16. lincval1
  17. lcosn0
  18. lincvalsc0
  19. lcoc0
  20. linc0scn0
  21. lincdifsn
  22. linc1
  23. lincellss
  24. lco0
  25. lcoel0
  26. lincsum
  27. lincscm
  28. lincsumcl
  29. lincscmcl
  30. lincsumscmcl
  31. lincolss
  32. ellcoellss
  33. lcoss
  34. lspsslco
  35. lcosslsp
  36. lspeqlco