Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The sum U+W of two linear subspaces and the sum ∑i<nUi of a finite family

Definition

Let V be a vector space over a field F (Vector space over a field), let n∈N, and let U be a finite family of linear subspaces of V, that is a function assigning to each i<n a linear subspace Ui of V (Linear subspace of a vector space); here n={0,…,n−1} (The natural numbers N (von Neumann), On N the order is membership: m<n  ⟺  m∈n), so the family is indexed from 0. Define

∑i<nUi  :=  { ∑i<nui  :  u:n→V with ui∈Ui for every i<n },

the finite sums being those of The product g0g1⋯gn−1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity read additively in the abelian group (V,+,0V), as in Linear combination of a finite list, and the span span⁡(S) as the smallest linear subspace containing S. For two linear subspaces U,W of V we write

U+W  :=  { u+w  :  u∈U, w∈W },

which is the case n=2 of the display above, since ∑i<2ui=(0V+u0)+u1=u0+u1.

Three facts about finite sums of vectors

All three are proved by induction on n (The principle of mathematical induction) from the two defining clauses ∑i<0ui=0V and ∑i<σ(n)ui=(∑i<nui)+un (The product g0g1⋯gn−1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity), together with the abelian group laws of (V,+,0V). They are collected here because the definition itself needs the first two, and because the lemmas below need all three.

(F1) The all-zero list sums to 0V. If z:n→V has zi=0V for every i<n, then ∑i<nzi=0V. At n=0 this is the empty sum, and if it holds at n then ∑i<σ(n)zi=0V+0V=0V.

(F2) The mixed identity. For every λ∈F and all lists u,w:n→V,

λ∑i<nui  +  ∑i<nwi  =  ∑i<n(λui+wi).

At n=0 both sides are 0V, since λ0V=0V (In any vector space 0Fv=0V, λ0V=0V, (−λ)v=−(λv), (−1F)v=−v, and λv=0V forces λ=0F or v=0V). If the identity holds at n, then at σ(n) the left-hand side is λ(∑i<nui+un)+(∑i<nwi+wn), which by axiom (V2) equals (λ∑i<nui+λun)+(∑i<nwi+wn); commutativity and associativity of + regroup this as (λ∑i<nui+∑i<nwi)+(λun+wn), which by the inductive hypothesis is ∑i<n(λui+wi)+(λun+wn)=∑i<σ(n)(λui+wi).

(F3) Extracting one term. Let u:n→V and j<n, and let u(j):n→V agree with u at every i≠j and satisfy uj(j)=0V. Then

∑i<nui  =  uj+∑i<nui(j).

At n=0 there is no j<0 and the claim is vacuous. Assume it at n and let j<σ(n), so j≤n (On N the order is membership: m<n  ⟺  m∈n). If j=n, then u(n) agrees with u on n, so ∑i<σ(n)ui(n)=∑i<nui+0V=∑i<nui, and un+∑i<nui=∑i<nui+un=∑i<σ(n)ui by commutativity. If j<n, then u(j) agrees with u at n, so ∑i<σ(n)ui(j)=∑i<nui(j)+un, and the inductive hypothesis applied to the restriction of u to n gives ∑i<σ(n)ui=(uj+∑i<nui(j))+un=uj+∑i<σ(n)ui(j), by associativity.

A consequence of (F1) and (F3). If ui=0V for every i≠j, then u(j) is the all-zero list, so ∑i<nui=uj+0V=uj: a list vanishing off a single index sums to its value at that index.

The sum is a linear subspace

∑i<nUi is a linear subspace of V. It is nonempty: each Ui contains 0V, and the all-zero list sums to 0V by (F1), so 0V∈∑i<nUi. And it satisfies the one-step test (One-step subspace test: a nonempty W⊆V is a linear subspace if and only if λu+v∈W for all λ∈F and u,v∈W): if x=∑i<nui and y=∑i<nwi with ui,wi∈Ui, and λ∈F, then (F2) gives λx+y=∑i<n(λui+wi), and λui+wi∈Ui because Ui is a linear subspace, so λx+y∈∑i<nUi.

So the definition really does produce a linear subspace, and this is asserted here rather than assumed.

The boundary case

N contains 0, so n=0 is a genuine case. The only list u:0→V is the empty function, and its sum is the empty sum 0V, so

∑i<0Ui  =  {0V},

the sum of the empty family of linear subspaces being the zero subspace. This is the base case of the induction in ∑i<nUi=span⁡(⋃i<nUi), so the sum is the smallest linear subspace containing every Ui and of the boundary case of Internal direct sum V=⨁i<nUi: the sum is everything and each summand meets the sum of the others only in 0V.

Remarks

Depends on

Used by

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources