Alphabeta Math
Session-authored (Fable 5 assisted)
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.

10 results · all verified · 9 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Vector Spaces, Linear Subspaces, Span and Direct Sums

1 · Prerequisites

2 · Summary

Objective. This page opens the linear algebra track. It defines a vector space over an arbitrary field and develops the structure theory that needs no counting: linear subspaces, the span, sums of subspaces and internal direct sums. Every result below holds over any field and for any vector space whatever. No proof on this page assumes a basis or a dimension, and none assumes that a vector space, an index set or a spanning set is finite; the only finiteness anywhere is the length of an individual sum of vectors and of a family of summands.

The field and the additive group are the published ones. A vector space here is over a field in the sense of Field, and no field axiom is restated. Its addition is an abelian group in the sense of Group and abelian group, so associativity, commutativity, the uniqueness of the zero vector (A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity), the uniqueness of negatives (In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided) and cancellation (Cancellation in a group: gx=gygx = gy or xg=ygxg = yg forces x=yx = y; equivalently left and right translation by gg are bijections of GG, so gx=hgx = h and xg=hxg = h each have exactly one solution) are inherited rather than re-derived. Vector space over a field therefore adds exactly four axioms, relating the scalars to the addition, and one warning: scalar multiplication is a map F×VVF \times V \to V and is not a binary operation on a set, so Binary operation on a set; associativity, commutativity, and a subset closed under the operation applies to the vector addition and never to it. The fourth axiom 1Fv=v1_F v = v is an axiom, not a consequence, as the definition shows by exhibiting a structure satisfying the other three and failing it. In any vector space 0Fv=0V0_F v = 0_V, λ0V=0V\lambda 0_V = 0_V, (λ)v=(λv)(-\lambda)v = -(\lambda v), (1F)v=v(-1_F)v = -v, and λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F or v=0Vv = 0_V then extracts what the axioms do not say outright: 0Fv=0V0_F v = 0_V, λ0V=0V\lambda 0_V = 0_V, (λ)v=(λv)(-\lambda)v = -(\lambda v), (1F)v=v(-1_F)v = -v, and that λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F or v=0Vv = 0_V. The identity (1F)v=v(-1_F)v = -v is used constantly below, since it says that closure under scalar multiplication already gives closure under negatives.

The two families of examples that carry the page. The vector space FXF^{X} of all functions XFX \to F with pointwise operations, and FnF^{n} as the case X=n={0,1,,n1}X = n = \{0, 1, \dots, n-1\} makes the set FXF^{X} of all functions XFX \to F a vector space with the pointwise operations, for an arbitrary index set XX. Taking X=nX = n, a natural number, gives FnF^{n}; and because a natural number is a von Neumann natural, n={0,,n1}n = \{0, \dots, n-1\}, so the coordinates of an element of FnF^{n} are x0,,xn1x_0, \dots, x_{n-1} and every index on this page starts at 00. The two boundary cases are stated there rather than left implicit: F0F^{0} has exactly one element, the empty function, so it is the zero space, and F1F^{1} is carried to FF by the bijection sending a vector to its single coordinate. The vector space Mm×n(F):=Fm×nM_{m \times n}(F) := F^{\,m \times n} of mm by nn matrices over a field, with entrywise operations is the case X=m×nX = m \times n: it gives Mm×n(F)=Fm×nM_{m \times n}(F) = F^{\,m \times n} its vector-space structure and its entry notation aija_{ij}, with both indices from 00, and nothing else: there is no matrix product, no identity matrix and no determinant on this page, and a later page must add the product to this object rather than define a second one. The vector space FXF^{X} of all functions XFX \to F with pointwise operations, and FnF^{n} as the case X=n={0,1,,n1}X = n = \{0, 1, \dots, n-1\} also records a dictionary that would otherwise be a silent double definition: the same set FXF^{X} carries the ring structure of The ring RXR^{X} of all functions from a set XX into a ring, with pointwise operations, with the same addition and with the pointwise product of two functions in place of the scalar multiplication used here. The two second operations do not even share a domain, and the relation between them is that λf\lambda f equals the ring product of ff with the constant function at λ\lambda.

Changing the field without changing the set. A field is a vector space over itself, and over any subfield KFK \subseteq F every FF-vector space is a KK-vector space by restricting the scalars proves that a field is a vector space over itself, and that an FF-vector space becomes a KK-vector space for any subfield KFK \subseteq F (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations) by restricting the scalar multiplication. This is the one place where the ring page is a genuine prerequisite. Its consequence for reading everything below is that the field is part of the data: "the vector space VV" is incomplete language, and every statement on this page names its field.

Linear subspaces, and why they are called that. The word subspace is already in use in this library for the topological notion, so the names here all say linear: Linear subspace of a vector space, One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W, The intersection of a nonempty family of linear subspaces of VV is a linear subspace of VV, The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace, The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family. The definition asks for three closure conditions and shows that the restricted operations make such a subset a vector space in its own right, with the zero and the negatives of the ambient space. The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace states the dictionary in both directions: the linear subspaces of VV are exactly the subgroups of (V,+,0V)(V,+,0_V) (Subgroup) that are closed under scalar multiplication, so everything the library proves about subgroups is available here at once. One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W compresses the three conditions into the single test λu+vW\lambda u + v \in W on a nonempty subset, the linear counterpart of One-step subgroup test: a nonempty HGH \subseteq G is a subgroup iff gh1Hgh^{-1} \in H for all g,hHg, h \in H; the identity and the inverses of HH are then those of GG, and The intersection of a nonempty family of linear subspaces of VV is a linear subspace of VV shows that intersections of nonempty families are again linear subspaces.

The span, defined from outside and identified from inside. The intersection lemma is what licenses Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS to define span(S)\operatorname{span}(S) as the intersection of all linear subspaces containing SS, exactly as The subgroup S\langle S \rangle generated by a subset, the cyclic subgroup g\langle g \rangle, and cyclic groups is defined; a linear combination is a finite sum i<nλivi\sum_{i<n} \lambda_i v_i, the finite sum being the published The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity read additively in the abelian group (V,+,0V)(V,+,0_V). Finite sums and finite products, by recursion cannot serve here, being stated for sequences into the complete ordered field. span(S)\operatorname{span}(S) is exactly the set of linear combinations of finite lists of elements of SS, and span()={0V}\operatorname{span}(\varnothing) = \{0_V\} then gives the description from inside, that span(S)\operatorname{span}(S) is precisely the set of linear combinations of finite lists of elements of SS, and with it span()={0V}\operatorname{span}(\varnothing) = \{0_V\} as a consequence of the empty sum being 0V0_V, not as a stipulation. The span is monotone and idempotent, span(S)=S\operatorname{span}(S) = S exactly when SS is a linear subspace, and span(S{0V})=span(S)\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S) records that the span is extensive, monotone and idempotent, and that span(S)=S\operatorname{span}(S) = S characterises the linear subspaces among all subsets; span{v}={λv:λF}\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}, which is {0V}\{0_V\} when v=0Vv = 0_V, and when v0Vv \ne 0_V contains 0V0_V only as the multiple 0Fv0_F v computes span{v}={λv:λF}\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\} and shows that for v0Vv \ne 0_V distinct scalars give distinct multiples.

Sums and direct sums. The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family defines i<nUi\sum_{i<n} U_i as the set of sums i<nui\sum_{i<n} u_i with uiUiu_i \in U_i, proves that it is a linear subspace rather than assuming it, and collects the three facts about finite sums of vectors that the rest of the page uses. Its empty case is {0V}\{0_V\}. i<nUi=span(i<nUi)\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr), so the sum is the smallest linear subspace containing every UiU_i identifies the sum with span(i<nUi)\operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr), so it is the smallest linear subspace containing every summand. Internal direct sum V=i<nUiV = \bigoplus_{i<n} U_i: the sum is everything and each summand meets the sum of the others only in 0V0_V then states the condition that matters: for each jj, UjU_j meets the sum of the other summands only in 0V0_V, and not merely that the summands meet each other pairwise only in 0V0_V. The definition proves that its condition implies the pairwise one and states that the converse fails from three summands on, the witness being on the companion page; for two summands the two conditions coincide and the definition reads U+W=VU + W = V with UW={0V}U \cap W = \{0_V\}. The payoff is V=i<nUiV = \bigoplus_{i<n} U_i if and only if every vVv \in V is i<nui\sum_{i<n} u_i with uiUiu_i \in U_i in exactly one way; equivalently, if and only if the sum is VV and i<nui=0V\sum_{i<n} u_i = 0_V with uiUiu_i \in U_i forces every ui=0Vu_i = 0_V: a direct sum is exactly the situation in which every vector decomposes in exactly one way, and equally exactly the situation in which the sum is all of VV and only the all-zero list sums to 0V0_V; the second half of that condition is not on its own equivalent to the first, and the lemma states both.

What this page does not develop. Linear independence, bases, dimension, linear maps, the matrix product, quotient spaces and external direct sums are all absent, and no proof above uses any of them. The empty family, the empty sum and the index 00 are treated as genuine cases throughout rather than as edge cases, which is why F0F^{0}, span()\operatorname{span}(\varnothing), i<0Ui\sum_{i<0} U_i and i<0Ui\bigoplus_{i<0} U_i all appear explicitly. Seventeen items make up this page, seven definitions and ten lemmas, six of them marked as landmarks in the flowchart above.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Vector space over a field

Definition

Let FF be a field (Field), with additive identity 0F0_F, multiplicative identity 1F1_F, and the field axioms as stated there. A vector space over FF, also called an FF-vector space, consists of

subject to the following axioms, in which u,vVu, v \in V and λ,μF\lambda, \mu \in F are arbitrary.

The elements of FF are called scalars. When several vector spaces are in play we write 0V0_V for the zero of VV, and we write v-v for the additive inverse of vv and uv:=u+(v)u - v := u + (-v).

The notation 0V0_V and v-v is legitimate. Axiom (V1) asserts only that some two-sided identity and some additive inverses exist. That there is at most one two-sided identity for ++ is A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity, and that an invertible element of a monoid has exactly one inverse is In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided; both are proved before Group and abelian group and are inherited here with the group structure. So 0V0_V and v-v denote well-defined elements, and nothing below re-derives them.

What (V1) buys, and why it is not restated. Associativity, commutativity, the identity law v+0V=v=0V+vv + 0_V = v = 0_V + v, the inverse law v+(v)=0Vv + (-v) = 0_V, cancellation (Cancellation in a group: gx=gygx = gy or xg=ygxg = yg forces x=yx = y; equivalently left and right translation by gg are bijections of GG, so gx=hgx = h and xg=hxg = h each have exactly one solution) and the inverse identities (In a group e1=ee^{-1} = e, (g1)1=g(g^{-1})^{-1} = g and (gh)1=h1g1(gh)^{-1} = h^{-1}g^{-1}, the order of the last product being essential) are facts about abelian groups. They are quoted from the group page wherever they are used and are never proved again for vectors.

Remarks

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

In any vector space 0Fv=0V0_F v = 0_V, λ0V=0V\lambda 0_V = 0_V, (λ)v=(λv)(-\lambda)v = -(\lambda v), (1F)v=v(-1_F)v = -v, and λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F or v=0Vv = 0_V

Statement

Let VV be a vector space over a field FF (Vector space over a field). For all λF\lambda \in F and vVv \in V:

  1. 0Fv=0V0_F v = 0_V;
  2. λ0V=0V\lambda 0_V = 0_V;
  3. (λ)v=(λv)(-\lambda)v = -(\lambda v), and also λ(v)=(λv)\lambda(-v) = -(\lambda v);
  4. (1F)v=v(-1_F)v = -v;
  5. if λv=0V\lambda v = 0_V then λ=0F\lambda = 0_F or v=0Vv = 0_V.

Here 0F0_F and 1F1_F are the additive and multiplicative identities of FF, 0V0_V is the zero vector, λ-\lambda is the additive inverse of λ\lambda in FF, and v-v is the additive inverse of vv in the abelian group (V,+,0V)(V,+,0_V).

Facts & Assumptions

Given: A field FF, a vector space VV over FF with axioms (V1)–(V5) (Vector space over a field), a scalar λF\lambda \in F and a vector vVv \in V.

[L1]

The four scalar axioms: λ(u+w)=λu+λw\lambda(u+w) = \lambda u + \lambda w (V2); (λ+μ)w=λw+μw(\lambda+\mu)w = \lambda w + \mu w (V3); (λμ)w=λ(μw)(\lambda\mu)w = \lambda(\mu w) (V4); 1Fw=w1_F w = w (V5) (Vector space over a field).

[L2]

(V,+,0V)(V,+,0_V) is an abelian group (V1): addition is associative and commutative, 0V0_V is a two-sided identity, and each wVw \in V has an additive inverse w-w with w+(w)=0V=(w)+ww + (-w) = 0_V = (-w) + w (Vector space over a field, Group and abelian group).

[L3]
[L4]

Field arithmetic (Field): 0F+0F=0F0_F + 0_F = 0_F; μ+(μ)=0F\mu + (-\mu) = 0_F for every μF\mu \in F; 1F1_F is the multiplicative identity; multiplication is associative; and every μ0F\mu \ne 0_F has a multiplicative inverse μ1\mu^{-1} with μ1μ=1F\mu^{-1}\mu = 1_F.

[L5]

The identities 0F0_F, 1F1_F and the inverses μ-\mu, μ1\mu^{-1} of a field are unique, so those notations denote well-defined elements (Identities and inverses in a field are unique).

Proof

technique · direct
1.1

By (V3) applied to 0F0_F and 0F0_F, and 0F+0F=0F0_F + 0_F = 0_F in FF: 0Fv+0Fv=(0F+0F)v=0Fv0_F v + 0_F v = (0_F + 0_F)v = 0_F v.

L1L4
1.2

Since 0V0_V is a two-sided identity for ++: 0Fv=0V+0Fv0_F v = 0_V + 0_F v.

L2
1.3

By (V2) applied to 0V0_V and 0V0_V, and 0V+0V=0V0_V + 0_V = 0_V in VV: λ0V+λ0V=λ(0V+0V)=λ0V\lambda 0_V + \lambda 0_V = \lambda(0_V + 0_V) = \lambda 0_V.

L1L2
1.4

Since 0V0_V is a two-sided identity for ++: λ0V=0V+λ0V\lambda 0_V = 0_V + \lambda 0_V.

L2
1.5

The vector λv\lambda v has an additive inverse (λv)-(\lambda v) with λv+((λv))=0V\lambda v + (-(\lambda v)) = 0_V.

L2
2.1

Combining steps 1.1 and 1.2 gives 0Fv+0Fv=0V+0Fv0_F v + 0_F v = 0_V + 0_F v; cancelling 0Fv0_F v on the right yields 0Fv=0V0_F v = 0_V, which is claim 1.

step 1.1step 1.2L3
2.2

Combining steps 1.3 and 1.4 gives λ0V+λ0V=0V+λ0V\lambda 0_V + \lambda 0_V = 0_V + \lambda 0_V; cancelling λ0V\lambda 0_V on the right yields λ0V=0V\lambda 0_V = 0_V, which is claim 2.

step 1.3step 1.4L3
3.1

By (V3) applied to λ\lambda and λ-\lambda, then λ+(λ)=0F\lambda + (-\lambda) = 0_F, then claim 1: λv+(λ)v=(λ+(λ))v=0Fv=0V\lambda v + (-\lambda)v = (\lambda + (-\lambda))v = 0_F v = 0_V.

step 2.1L1L4
3.2

By (V2) applied to vv and v-v, then v+(v)=0Vv + (-v) = 0_V, then claim 2: λv+λ(v)=λ(v+(v))=λ0V=0V\lambda v + \lambda(-v) = \lambda(v + (-v)) = \lambda 0_V = 0_V.

step 2.2L1L2
3.3

Suppose λv=0V\lambda v = 0_V and λ0F\lambda \ne 0_F. Then λ1F\lambda^{-1} \in F exists with λ1λ=1F\lambda^{-1}\lambda = 1_F, so v=1Fv=(λ1λ)v=λ1(λv)=λ10V=0Vv = 1_F v = (\lambda^{-1}\lambda)v = \lambda^{-1}(\lambda v) = \lambda^{-1} 0_V = 0_V, using (V5), (V4) and claim 2 in turn.

step 2.2L1L4L5
4.1

Steps 3.1 and 1.5 exhibit both (λ)v(-\lambda)v and (λv)-(\lambda v) as vectors xx with λv+x=0V\lambda v + x = 0_V; cancelling λv\lambda v on the left gives (λ)v=(λv)(-\lambda)v = -(\lambda v).

step 3.1step 1.5L3
5.1

Likewise steps 3.2 and 1.5 give λv+λ(v)=0V=λv+((λv))\lambda v + \lambda(-v) = 0_V = \lambda v + (-(\lambda v)), and cancelling λv\lambda v on the left gives λ(v)=(λv)\lambda(-v) = -(\lambda v); with step 4.1 this is claim 3.

step 3.2step 1.5L3
5.2

Taking λ=1F\lambda = 1_F in step 4.1 and using (V5): (1F)v=(1Fv)=v(-1_F)v = -(1_F v) = -v, which is claim 4.

step 4.1L1
6.1

Claim 1 is step 2.1, claim 2 is step 2.2, claim 3 is steps 4.1 and 5.1, and claim 4 is step 5.2; for claim 5, if λv=0V\lambda v = 0_V then either λ=0F\lambda = 0_F, or λ0F\lambda \ne 0_F and step 3.3 gives v=0Vv = 0_V.

step 2.1step 2.2step 3.3step 4.1step 5.1step 5.2

Remarks

DefinitionDefinition: AI-adaptedProof: AI-adaptedjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The vector space FXF^{X} of all functions XFX \to F with pointwise operations, and FnF^{n} as the case X=n={0,1,,n1}X = n = \{0, 1, \dots, n-1\}

Definition

Let FF be a field (Field) and let XX be any set. Write

FX  :=  {f  :  f is a function XF},F^{X} \;:=\; \{\, f \;:\; f \text{ is a function } X \to F \,\},

and for fFXf \in F^{X} write f(x)f(x) for its value at xXx \in X. Two elements of FXF^{X} are equal exactly when they agree at every point of XX. Define

(f+g)(x)  :=  f(x)+g(x),(λf)(x)  :=  λf(x),0FX(x)  :=  0F,(f + g)(x) \;:=\; f(x) + g(x), \qquad (\lambda f)(x) \;:=\; \lambda\, f(x), \qquad 0_{F^{X}}(x) \;:=\; 0_F,

for f,gFXf, g \in F^{X}, λF\lambda \in F and xXx \in X, the operations on the right being those of FF. These are the pointwise operations.

These rules really are the required data. For f,gFXf, g \in F^{X} the assignment xf(x)+g(x)x \mapsto f(x) + g(x) is a function XFX \to F, so ++ is a binary operation FX×FXFXF^{X} \times F^{X} \to F^{X} (Binary operation on a set; associativity, commutativity, and a subset closed under the operation); for λF\lambda \in F and fFXf \in F^{X} the assignment xλf(x)x \mapsto \lambda f(x) is a function XFX \to F, so scalar multiplication is a map F×FXFXF \times F^{X} \to F^{X}; and 0FX0_{F^{X}}, the constant function at 0F0_F, is an element of FXF^{X}.

FXF^{X} is a vector space over FF (Vector space over a field). Each axiom is an equation between elements of FXF^{X}, hence holds exactly when it holds at every xXx \in X after evaluation, and there it is the corresponding field axiom applied to the values f(x),g(x),λ,μf(x), g(x), \lambda, \mu:

  • associativity and commutativity of ++, and f+0FX=ff + 0_{F^{X}} = f, come from the same laws for ++ in FF; the additive inverse of ff is xf(x)x \mapsto -f(x), which lies in FXF^{X} and satisfies f+(f)=0FXf + (-f) = 0_{F^{X}} pointwise. This is axiom (V1);
  • (λ(f+g))(x)=λ(f(x)+g(x))=λf(x)+λg(x)\bigl(\lambda(f+g)\bigr)(x) = \lambda(f(x)+g(x)) = \lambda f(x) + \lambda g(x) is (V2), by distributivity in FF;
  • ((λ+μ)f)(x)=(λ+μ)f(x)=λf(x)+μf(x)\bigl((\lambda+\mu)f\bigr)(x) = (\lambda+\mu)f(x) = \lambda f(x) + \mu f(x) is (V3), by distributivity in FF;
  • ((λμ)f)(x)=(λμ)f(x)=λ(μf(x))\bigl((\lambda\mu)f\bigr)(x) = (\lambda\mu)f(x) = \lambda(\mu f(x)) is (V4), by associativity of multiplication in FF;
  • (1Ff)(x)=1Ff(x)=f(x)(1_F f)(x) = 1_F f(x) = f(x) is (V5), by the multiplicative identity law in FF.

The case X=nX = n

A natural number is a von Neumann natural (The natural numbers N\mathbb{N} (von Neumann)), that is a set, and n={mN:m<n}={0,1,,n1}n = \{\, m \in \mathbb{N} : m < n \,\} = \{0, 1, \dots, n-1\} (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n). Taking X=nX = n therefore gives

Fn  =  {x  :  x is a function nF},F^{n} \;=\; \{\, x \;:\; x \text{ is a function } n \to F \,\},

whose elements are written x=(x0,x1,,xn1)x = (x_0, x_1, \dots, x_{n-1}) with xi:=x(i)x_i := x(i) for i<ni < n. The coordinates are indexed from 00, because 0n0 \in n whenever n0n \ne 0 and nnn \notin n always. The operations read

(x+y)i=xi+yi,(λx)i=λxi(i<n),(x + y)_i = x_i + y_i, \qquad (\lambda x)_i = \lambda x_i \qquad (i < n),

and the zero of FnF^{n} is the tuple all of whose coordinates are 0F0_F.

The two boundary cases. N\mathbb{N} contains 00, so n=0n = 0 is a genuine case. Since 0=0 = \varnothing, the set F0=FF^{0} = F^{\varnothing} has exactly one element, the empty function; that element is 0F00_{F^{0}}, so F0F^{0} is the zero space {0F0}\{0_{F^{0}}\}, not the empty set. For n=1n = 1 we have 1={0}1 = \{0\}, and the map F1FF^{1} \to F sending xx to its single coordinate x0x_0 is a bijection satisfying (x+y)0=x0+y0(x+y)_0 = x_0 + y_0 and (λx)0=λx0(\lambda x)_0 = \lambda x_0; we use it to read F1F^{1} as FF where convenient. (No general notion of isomorphism of vector spaces is available on this page, and none is claimed here: what is asserted is exactly the displayed bijection and the two displayed equations.)

Remarks

  • The same set FXF^{X} also carries a ring structure, and the two must not be conflated. For a ring RR and a set XX, The ring RXR^{X} of all functions from a set XX into a ring, with pointwise operations equips the set RXR^{X} of all functions XRX \to R with pointwise addition and pointwise multiplication. Taking R=FR = F, the underlying set is literally the same set FXF^{X} as here, and the addition is literally the same operation, (f+g)(x)=f(x)+g(x)(f+g)(x) = f(x) + g(x) in both. What differs is the second operation:

    second operationtype
    ring of functions(fg)(x)=f(x)g(x)(fg)(x) = f(x)\,g(x)FX×FXFXF^{X} \times F^{X} \to F^{X}
    vector space (here)(λf)(x)=λf(x)(\lambda f)(x) = \lambda\, f(x)F×FXFXF \times F^{X} \to F^{X}

    Neither is a special case of the other, since they do not even have the same domain: one multiplies two functions, the other multiplies a function by a scalar. They agree in the following sense, and this is the whole of the relation between them: for λF\lambda \in F let cλFXc_\lambda \in F^{X} be the constant function at λ\lambda; then λf\lambda f and the ring product cλfc_\lambda f have the same value λf(x)\lambda f(x) at every xx, so they are equal. Both structures are present on FXF^{X} at once, and nothing on this page uses the ring product.

  • Why FnF^{n} is defined this way rather than as "nn-tuples". An nn-tuple is already a function on an index set, and taking that index set to be the natural number nn itself makes the coordinates, the finite sums of The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity and the induction arguments below all run over the same object. The price is that every index starts at 00, and that F0F^{0} is a one-element space; both are recorded above so that no statement on this page or its companion is quietly restricted to n1n \ge 1.

  • XX is arbitrary. Nothing above assumes XX finite, countable, or nonempty. The case X=NX = \mathbb{N} gives the space of all families of scalars indexed by N\mathbb{N}, and the case X=m×nX = m \times n gives the matrices of The vector space Mm×n(F):=Fm×nM_{m \times n}(F) := F^{\,m \times n} of mm by nn matrices over a field, with entrywise operations.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The vector space Mm×n(F):=Fm×nM_{m \times n}(F) := F^{\,m \times n} of mm by nn matrices over a field, with entrywise operations

Definition

Let FF be a field (Field) and let m,nNm, n \in \mathbb{N}. Recall that a natural number is a von Neumann natural (The natural numbers N\mathbb{N} (von Neumann)), so m={0,,m1}m = \{0, \dots, m-1\} and n={0,,n1}n = \{0, \dots, n-1\} (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n), and let m×nm \times n be their cartesian product. An mm by nn matrix over FF is an element of the function space Fm×nF^{\,m \times n} (The vector space FXF^{X} of all functions XFX \to F with pointwise operations, and FnF^{n} as the case X=n={0,1,,n1}X = n = \{0, 1, \dots, n-1\}), that is a function a:m×nFa : m \times n \to F; we write

aij  :=  a(i,j)(i<m,  j<n)a_{ij} \;:=\; a(i,j) \qquad (i < m,\; j < n)

for its entries, ii being the row index and jj the column index. Write

Mm×n(F)  :=  Fm×n,M_{m \times n}(F) \;:=\; F^{\,m \times n},

and Mn(F):=Mn×n(F)M_n(F) := M_{n \times n}(F) for the square case.

Since Mm×n(F)M_{m \times n}(F) is the function space Fm×nF^{\,m \times n}, it is a vector space over FF with the pointwise operations of The vector space FXF^{X} of all functions XFX \to F with pointwise operations, and FnF^{n} as the case X=n={0,1,,n1}X = n = \{0, 1, \dots, n-1\}, which read entrywise:

(a+b)ij=aij+bij,(λa)ij=λaij(i<m,  j<n),(a + b)_{ij} = a_{ij} + b_{ij}, \qquad (\lambda a)_{ij} = \lambda\, a_{ij} \qquad (i < m,\; j < n),

and the zero of Mm×n(F)M_{m \times n}(F) is the matrix all of whose entries are 0F0_F. No verification is needed beyond that already carried out in The vector space FXF^{X} of all functions XFX \to F with pointwise operations, and FnF^{n} as the case X=n={0,1,,n1}X = n = \{0, 1, \dots, n-1\} for an arbitrary index set: this is the case X=m×nX = m \times n.

Both indices start at 00. The rows are indexed by im={0,,m1}i \in m = \{0,\dots,m-1\} and the columns by jn={0,,n1}j \in n = \{0,\dots,n-1\}, so the entries of a 22 by 33 matrix are a00,a01,a02,a10,a11,a12a_{00}, a_{01}, a_{02}, a_{10}, a_{11}, a_{12}.

The degenerate shapes. N\mathbb{N} contains 00, so m=0m = 0 and n=0n = 0 are genuine cases. If m=0m = 0 or n=0n = 0 then m×n=m \times n = \varnothing, so Mm×n(F)M_{m \times n}(F) has exactly one element, the empty function, and is the zero space; there is no matrix of shape 00 by nn other than that one.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-28 (claude-fable-5)Open item page →

A field is a vector space over itself, and over any subfield KFK \subseteq F every FF-vector space is a KK-vector space by restricting the scalars

Statement

Let FF be a field (Field).

  1. FF is a vector space over itself (Vector space over a field): take the set to be FF, the vector addition to be the field addition, the zero vector to be 0F0_F, and the scalar multiplication F×FFF \times F \to F to be the field multiplication.
  2. Let KFK \subseteq F be a subfield (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations) and let VV be a vector space over FF. Then VV, with the same addition and the same zero vector and with the scalar multiplication restricted to K×VK \times V, is a vector space over KK. This is called restricting the scalars from FF to KK.
  3. In particular FF is a vector space over every subfield KFK \subseteq F, with the field multiplication restricted to K×FK \times F as scalar multiplication.

Facts & Assumptions

Given: A field FF, a subfield KFK \subseteq F, and a vector space VV over FF.

[L1]

The vector space axioms (V1)–(V5) (Vector space over a field): (V,+,0V)(V,+,0_V) is an abelian group; λ(u+v)=λu+λv\lambda(u+v) = \lambda u + \lambda v; (λ+μ)v=λv+μv(\lambda+\mu)v = \lambda v + \mu v; (λμ)v=λ(μv)(\lambda\mu)v = \lambda(\mu v); 1Fv=v1_F v = v.

[L2]

The field axioms of Field, read as they are read throughout this library: (F,+,0F)(F,+,0_F) is an abelian group; multiplication on FF is associative and commutative with two-sided identity 1F1_F; multiplication distributes over addition, so that x(y+z)=xy+xzx(y+z) = xy+xz and (y+z)x=yx+zx(y+z)x = yx+zx; and every x0Fx \ne 0_F has a multiplicative inverse.

[L3]

A subfield KK of FF is a subring of FF closed under inverses of its nonzero elements; equivalently, a subset containing 1F1_F with abKa - b \in K and abKab \in K for all a,bKa, b \in K and x1Kx^{-1} \in K for every nonzero xKx \in K. With the restricted operations KK is itself a field, its addition and multiplication being the restrictions of those of FF, and 0K=0F0_K = 0_F, 1K=1F1_K = 1_F, with the negatives and the inverses of KK those of FF (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations).

Proof

technique · direct
1.1

Put VF:=FV_F := F as a set, let the vector addition be the field addition with zero vector 0F0_F, and let the scalar multiplication be the field multiplication, which is a map F×FFF \times F \to F as required.

L2
1.2

Axiom (V1) holds for VFV_F: axiom (A) of a field says exactly that (F,+,0F)(F,+,0_F) is an abelian group.

L2
1.3

Axiom (V2) holds for VFV_F: λ(u+v)=λu+λv\lambda(u+v) = \lambda u + \lambda v is distributivity of multiplication over addition.

L2
1.4

Axiom (V3) holds for VFV_F: (λ+μ)v=λv+μv(\lambda+\mu)v = \lambda v + \mu v is distributivity on the other side.

L2
1.5

Axiom (V4) holds for VFV_F: (λμ)v=λ(μv)(\lambda\mu)v = \lambda(\mu v) is associativity of the field multiplication.

L2
1.6

Axiom (V5) holds for VFV_F: 1Fv=v1_F v = v is the multiplicative identity law.

L2
1.7

For claim 2: since KFK \subseteq F, restricting the scalar multiplication of VV to the subset K×VK \times V of F×VF \times V yields a map K×VVK \times V \to V, which is the required datum.

L3
1.8

The set VV, its addition and its zero vector are unchanged by the restriction, so (V,+,0V)(V,+,0_V) is still an abelian group; this is axiom (V1) for the KK-structure.

L1
1.9

For λ,μK\lambda, \mu \in K the sum λ+μ\lambda + \mu and the product λμ\lambda\mu formed in KK are the sum and the product formed in FF, and the multiplicative identity of KK is 1F1_F.

L3
2.1

Steps 1.1 to 1.6 verify (V1)–(V5), so FF with the operations of step 1.1 is a vector space over itself: claim 1.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6L1
2.2

Let λ,μK\lambda, \mu \in K and u,vVu, v \in V. Then λ(u+v)=λu+λv\lambda(u+v) = \lambda u + \lambda v and (λμ)v=λ(μv)(\lambda\mu)v = \lambda(\mu v) are the instances of (V2) and (V4) for these elements of FF, the product λμ\lambda\mu being the same whether formed in KK or in FF; (λ+μ)v=λv+μv(\lambda+\mu)v = \lambda v + \mu v is the instance of (V3), the sum λ+μ\lambda+\mu being likewise the same; and the identity of KK is 1F1_F, so 1Kv=1Fv=v1_K v = 1_F v = v is the instance of (V5).

step 1.7step 1.9L1L3
3.1

With step 1.8, the restricted structure satisfies (V1)–(V5) over KK, so VV is a vector space over KK: claim 2.

step 1.8step 2.2L1
4.1

Claim 3 follows by applying claim 2 to the FF-vector space of claim 1: FF is a vector space over KK, its scalar multiplication being the field multiplication restricted to K×FK \times F.

step 2.1step 3.1

Remarks

  • On the field facts in [L2]. Axiom (M) of Field asserts that multiplication is associative and commutative on all of FF with x1F=xx \cdot 1_F = x for every xFx \in F, the element 0F0_F included, and right distributivity then follows from axiom (D) by commuting, as Multiplication by zero: 0a=00 \cdot a = 0 already records. These unrestricted forms are spent in exactly three of the steps above, where axioms (V3), (V4) and (V5) are read off for arbitrary scalars including 0F0_F: step 1.4 needs distributivity on the right; step 1.5 needs associativity of the multiplication at 0F0_F as well; and step 1.6 needs 1Fx=x1_F x = x rather than the literal x1F=xx \cdot 1_F = x, which commutativity supplies, and needs it at x=0Fx = 0_F too. They are used nowhere else: step 1.2 is axiom (A) verbatim, step 1.3 is axiom (D) verbatim, and steps 1.7 to 4.1 use only the vector-space axioms of VV and the subfield facts of [L3].

  • Restricting the scalars changes the structure, not the set. The vectors, the addition and the zero are untouched; only the collection of scalars allowed to act shrinks. Everything that can be said about VV as a KK-vector space is therefore a statement about the same object with fewer operations available, and every FF-linear subspace of VV is in particular a KK-linear subspace (Linear subspace of a vector space). The converse fails, and that is the point of the construction.

  • The field is part of the data. Because of this lemma, a bare phrase like "the vector space VV" is incomplete: R\mathbb{R} is a vector space over R\mathbb{R} and also over the embedded copy of Q\mathbb{Q} inside it, and these are different structures on one set. Every statement on this page names its field.

  • Nothing here is about dimension. How much smaller KK is than FF, and what that does to VV, is a question about bases and dimension, which are developed on a later page. This lemma asserts only that the restricted structure satisfies the five axioms.

DefinitionDefinition: Literature-sourcedProof: AI-adaptedjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Linear subspace of a vector space

Definition

Let VV be a vector space over a field FF (Vector space over a field). A subset WVW \subseteq V is a linear subspace of VV when

  • (W1) 0VW0_V \in W;
  • (W2) WW is closed under the vector addition: u,vWu, v \in W implies u+vWu + v \in W;
  • (W3) WW is closed under scalar multiplication: λF\lambda \in F and vWv \in W imply λvW\lambda v \in W.

Every vector space VV has the two trivial linear subspaces {0V}\{0_V\} and VV itself; a linear subspace WW with WVW \ne V is called proper.

The restricted operations are the required data, and WW is a vector space. By (W2) the vector addition of VV restricts to a binary operation W×WWW \times W \to W, and by (W3) the scalar multiplication restricts to a map F×WWF \times W \to W. With these and the element 0V0_V, the set WW is a vector space over FF:

So (W,+,0V)(W,+,0_V) is an abelian group, which is axiom (V1), and WW is a vector space over FF whose zero vector and whose additive inverses are those of VV. In the language of Subgroup, the three displayed conditions (S1) 0VW0_V \in W, (S2) closure under addition and (S3) closure under additive inverses all hold, so WW is a subgroup of the abelian group (V,+,0V)(V,+,0_V) (Group and abelian group); that reading, and its converse, are recorded as The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace and are cited from there rather than re-argued below.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace

Statement

Let VV be a vector space over a field FF (Vector space over a field).

  1. (V,+,0V)(V, +, 0_V) is an abelian group (Group and abelian group), called the additive group of VV.
  2. Every linear subspace WW of VV (Linear subspace of a vector space) is a subgroup of (V,+,0V)(V,+,0_V) (Subgroup). Consequently WW with the restricted addition is itself a group, whose identity is 0V0_V and whose inverses are those of VV.
  3. Conversely, if WVW \subseteq V is a subgroup of (V,+,0V)(V,+,0_V) and λvW\lambda v \in W for all λF\lambda \in F and vWv \in W, then WW is a linear subspace of VV.

So the linear subspaces of VV are exactly the subgroups of its additive group that are closed under scalar multiplication.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, and a subset WVW \subseteq V.

[L1]

Axiom (V1): (V,+,0V)(V,+,0_V) is an abelian group (Vector space over a field, Group and abelian group).

[L2]

A subgroup of a group GG with identity ee is a subset HH satisfying (S1) eHe \in H, (S2) x,yHx, y \in H implies xyHxy \in H, and (S3) xHx \in H implies x1Hx^{-1} \in H; such an HH, with the restricted operation, is itself a group whose identity and whose inverses are those of GG (Subgroup).

[L3]

A linear subspace of VV is a subset satisfying (W1) 0VW0_V \in W, (W2) closure under ++, and (W3) closure under scalar multiplication (Linear subspace of a vector space).

Proof

technique · direct
1.1

Claim 1 is axiom (V1) of a vector space, which asserts in as many words that (V,+,0V)(V,+,0_V) is an abelian group.

L1
1.2

Let WW be a linear subspace of VV. Condition (W1) says 0VW0_V \in W, which is condition (S1) for the group (V,+,0V)(V,+,0_V), whose identity is 0V0_V.

L1L2L3
1.3

Condition (W2) says u+vWu + v \in W for all u,vWu, v \in W, which is condition (S2) for (V,+,0V)(V,+,0_V), whose operation is ++.

L2L3
1.4

Let vWv \in W. By (W3) with λ=1F\lambda = -1_F we get (1F)vW(-1_F)v \in W, and (1F)v=v(-1_F)v = -v, so vW-v \in W; since the inverse of vv in the group (V,+,0V)(V,+,0_V) is v-v, this is condition (S3).

L1L2L3L4
1.5

Conversely, let WW be a subgroup of (V,+,0V)(V,+,0_V) with λvW\lambda v \in W for all λF\lambda \in F and vWv \in W. Condition (S1) gives 0VW0_V \in W, which is (W1); condition (S2) gives closure under ++, which is (W2); and the hypothesis is (W3).

L2L3
2.1

By steps 1.2, 1.3 and 1.4 the subset WW satisfies (S1), (S2) and (S3), so it is a subgroup of (V,+,0V)(V,+,0_V); by the properties of a subgroup it is then a group under the restricted addition, with identity 0V0_V and with the inverses of VV. This is claim 2.

step 1.2step 1.3step 1.4L2
2.2

By step 1.5 the subset WW of that step satisfies (W1), (W2) and (W3), so it is a linear subspace of VV. This is claim 3.

step 1.5L3
3.1

Claim 1 is step 1.1, claim 2 is step 2.1 and claim 3 is step 2.2; together they say that the linear subspaces of VV are exactly the subgroups of (V,+,0V)(V,+,0_V) closed under scalar multiplication.

step 1.1step 2.1step 2.2

Remarks

  • What the two directions cost. Going from a linear subspace to a subgroup uses one fact about vector spaces and no group theory: closure under additive inverses is not assumed but derived, from closure under scalar multiplication at the scalar 1F-1_F. Going back is pure bookkeeping, since (W1) and (W2) are literally (S1) and (S2).

  • Why this is worth an item. Every statement the library proves about subgroups applies to linear subspaces at once. In particular the intersection of a nonempty family of subgroups is a subgroup (The intersection of a nonempty family of subgroups of GG is a subgroup of GG), which is the group-theoretic shadow of The intersection of a nonempty family of linear subspaces of VV is a linear subspace of VV below.

  • The hypothesis in claim 3 is not decoration. Conditions (S1)–(S3) do not mention the scalars at all, so a subgroup of (V,+,0V)(V,+,0_V) is required only to contain 0V0_V and to be closed under addition and under negation; closure under multiplication by an arbitrary λF\lambda \in F is a further condition, and claim 3 assumes it rather than deriving it. Claim 2 says that in the other direction nothing extra is needed, because (W3) is already one of the three defining conditions of a linear subspace.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W

Statement

Let VV be a vector space over a field FF (Vector space over a field) and let WVW \subseteq V be nonempty. Then WW is a linear subspace of VV (Linear subspace of a vector space) if and only if

λu+vWfor all λF and all u,vW.\lambda u + v \in W \qquad \text{for all } \lambda \in F \text{ and all } u, v \in W .

Nonemptiness cannot be dropped: the empty set satisfies the displayed condition vacuously and is not a linear subspace, since it does not contain 0V0_V.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, and a nonempty subset WVW \subseteq V.

[L1]

A linear subspace of VV is a subset satisfying (W1) 0VW0_V \in W, (W2) closure under ++, and (W3) closure under scalar multiplication (Linear subspace of a vector space).

[L2]

The vector space axioms, in particular (V5) 1Fv=v1_F v = v, and that (V,+,0V)(V,+,0_V) is an abelian group with 0V0_V a two-sided identity (Vector space over a field).

[L4]

FF has elements 0F0_F and 1F1_F, and every μF\mu \in F has an additive inverse μ-\mu; in particular 1FF1_F \in F and 1FF-1_F \in F (Field).

Proof

technique · direct
1.1

Necessity. Suppose WW is a linear subspace, and let λF\lambda \in F and u,vWu, v \in W. Then λuW\lambda u \in W by (W3), and hence λu+vW\lambda u + v \in W by (W2).

L1
1.2

Sufficiency, the zero vector. Suppose λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W. Since WW is nonempty, choose wWw \in W; applying the condition with λ=1F\lambda = -1_F and u=v=wu = v = w gives (1F)w+wW(-1_F)w + w \in W, and (1F)w+w=w+w=0V(-1_F)w + w = -w + w = 0_V, so 0VW0_V \in W, which is (W1).

givenL3L4choose
1.3

Sufficiency, closure under addition. Let u,vWu, v \in W. Applying the condition with λ=1F\lambda = 1_F gives 1Fu+vW1_F u + v \in W, and 1Fu=u1_F u = u by (V5), so u+vWu + v \in W, which is (W2).

givenL2L4
2.1

Sufficiency, closure under scalars. Let λF\lambda \in F and uWu \in W. By step 1.2 we have 0VW0_V \in W, so the condition applies to λ\lambda, uu and 0V0_V and gives λu+0VW\lambda u + 0_V \in W; since 0V0_V is a two-sided identity, λu+0V=λu\lambda u + 0_V = \lambda u, so λuW\lambda u \in W, which is (W3).

step 1.2givenL2
3.1

Steps 1.2, 1.3 and 2.1 verify (W1), (W2) and (W3), so a nonempty WW satisfying the displayed condition is a linear subspace; with step 1.1 this proves the equivalence.

step 1.1step 1.2step 1.3step 2.1L1

Remarks

  • The order of the two verifications matters. Closure under scalar multiplication is deduced after 0V0_V is known to lie in WW, because it is obtained by applying the test to the pair uu, 0V0_V. Running the argument in the other order would use 0VW0_V \in W before it had been established.

  • One test, three conditions. The single condition is exactly as strong as the three of Linear subspace of a vector space, and it is the form used in practice: to check that a set is a linear subspace one shows it is nonempty and closes under a single mixed expression. It is the linear analogue of the one-step subgroup test gh1Hgh^{-1} \in H (One-step subgroup test: a nonempty HGH \subseteq G is a subgroup iff gh1Hgh^{-1} \in H for all g,hHg, h \in H; the identity and the inverses of HH are then those of GG), and, exactly as there, the nonemptiness hypothesis is what rules out the empty set.

  • Neither closure condition implies the other, so a test combining them is not extravagant. A subset of a vector space can be closed under addition and not under scalar multiplication, and another can be closed under scalar multiplication and not under addition; the companion examples page records a witness of each kind.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The intersection of a nonempty family of linear subspaces of VV is a linear subspace of VV

Statement

Let VV be a vector space over a field FF (Vector space over a field) and let W\mathcal{W} be a nonempty set of linear subspaces of VV (Linear subspace of a vector space). Then

U  =  WWW  =  {xV  :  xW for every WW}U \;=\; \bigcap_{W \in \mathcal{W}} W \;=\; \{\, x \in V \;:\; x \in W \text{ for every } W \in \mathcal{W} \,\}

is a linear subspace of VV. In particular the intersection of two linear subspaces is a linear subspace.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, a nonempty set W\mathcal{W} of linear subspaces of VV, and UU the intersection of the members of W\mathcal{W}.

[L1]

Each WWW \in \mathcal{W} contains 0V0_V, is closed under ++, and is closed under scalar multiplication (Linear subspace of a vector space).

[L2]

One-step test: a nonempty SVS \subseteq V with λu+vS\lambda u + v \in S for all λF\lambda \in F and u,vSu, v \in S is a linear subspace of VV (One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W).

Proof

technique · direct
1.1

UVU \subseteq V, since W\mathcal{W} is nonempty and every member of it is a subset of VV.

givenL1
1.2

0VU0_V \in U, since 0VW0_V \in W for every WWW \in \mathcal{W}; in particular UU is nonempty.

L1
1.3

Let λF\lambda \in F and u,vUu, v \in U, and let WWW \in \mathcal{W} be arbitrary. Then u,vWu, v \in W, so λuW\lambda u \in W by closure under scalar multiplication and λu+vW\lambda u + v \in W by closure under addition.

givenL1
2.1

Since WW was an arbitrary member of W\mathcal{W}, the vector λu+v\lambda u + v lies in every member of W\mathcal{W}, that is λu+vU\lambda u + v \in U.

step 1.3
3.1

UU is a nonempty subset of VV satisfying the one-step test, hence a linear subspace of VV; taking W\mathcal{W} to have two members gives the last sentence of the statement.

step 1.1step 1.2step 2.1L2

Remarks

DefinitionDefinition: AI-adaptedProof: AI-adaptedjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS

Definition

Let VV be a vector space over a field FF (Vector space over a field).

Finite sums of vectors

By axiom (V1) the triple (V,+,0V)(V, +, 0_V) is an abelian group (Group and abelian group), hence in particular a commutative monoid (Semigroup and monoid). So the finite products of The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity are available in it, and we write them additively: for nNn \in \mathbb{N} and a finite list u:nVu : n \to V, that is a function on the von Neumann natural n={0,,n1}n = \{0, \dots, n-1\} (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n),

i<nui  :=  i<nuicomputed in (V,+,0V),\sum_{i<n} u_i \;:=\; \prod_{i<n} u_i \quad \text{computed in } (V,+,0_V),

so that i<0ui=0V\sum_{i<0} u_i = 0_V and i<σ(n)ui=(i<nui)+un\sum_{i<\sigma(n)} u_i = \bigl(\sum_{i<n} u_i\bigr) + u_n, and the value depends only on u0,,un1u_0, \dots, u_{n-1}.

Linear combinations

A linear combination in VV is a vector of the form

i<nλivi\sum_{i<n} \lambda_i v_i

where nNn \in \mathbb{N}, λ:nF\lambda : n \to F is a finite list of scalars and v:nVv : n \to V is a finite list of vectors; the sum is the finite sum just described, of the list iλivii \mapsto \lambda_i v_i. For SVS \subseteq V, a vector wVw \in V is a linear combination of elements of SS when there are nNn \in \mathbb{N}, λ:nF\lambda : n \to F and v:nSv : n \to S with w=i<nλiviw = \sum_{i<n} \lambda_i v_i.

The empty case is a real case. N\mathbb{N} contains 00 (The natural numbers N\mathbb{N} (von Neumann)), and at n=0n = 0 the sum is the empty sum, which is 0V0_V. So 0V0_V is a linear combination of elements of every subset of VV, including S=S = \varnothing. The lists are indexed from 00, so a linear combination of length nn is λ0v0++λn1vn1\lambda_0 v_0 + \dots + \lambda_{n-1}v_{n-1}; no statement here is restricted to n1n \ge 1.

The span

Let SVS \subseteq V. The set of linear subspaces of VV containing SS is nonempty, since VV itself is one, so its intersection is a linear subspace of VV by The intersection of a nonempty family of linear subspaces of VV is a linear subspace of VV. That intersection is the span of SS,

span(S)  :=  {W  :  W is a linear subspace of V and SW}.\operatorname{span}(S) \;:=\; \bigcap \{\, W \;:\; W \text{ is a linear subspace of } V \text{ and } S \subseteq W \,\} .

It contains SS, being an intersection of sets each of which contains SS, and it is contained in every linear subspace of VV that contains SS. So it is the smallest linear subspace of VV containing SS, and those two properties determine it uniquely: if WW and WW' both contain SS and are each contained in every linear subspace containing SS, then each is contained in the other. This is what licenses the definite article.

A subset SVS \subseteq V spans VV, or is a spanning set of VV, when span(S)=V\operatorname{span}(S) = V.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

span(S)\operatorname{span}(S) is exactly the set of linear combinations of finite lists of elements of SS, and span()={0V}\operatorname{span}(\varnothing) = \{0_V\}

Statement

Let VV be a vector space over a field FF (Vector space over a field) and let SVS \subseteq V. Write

L(S)  :=  {i<nλivi  :  nN, λ:nF, v:nS}L(S) \;:=\; \Bigl\{\, \sum_{i<n} \lambda_i v_i \;:\; n \in \mathbb{N},\ \lambda : n \to F,\ v : n \to S \,\Bigr\}

for the set of linear combinations of elements of SS (Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS). Then

span(S)  =  L(S).\operatorname{span}(S) \;=\; L(S).

In particular span()={0V}\operatorname{span}(\varnothing) = \{0_V\}, and for every SVS \subseteq V the span of SS contains 0V0_V as the empty linear combination.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, and a subset SVS \subseteq V.

[L1]

span(S)\operatorname{span}(S) is a linear subspace of VV, it contains SS, and it is contained in every linear subspace of VV that contains SS (Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS).

[L2]

Finite sums in (V,+,0V)(V,+,0_V), written additively: i<0ui=0V\sum_{i<0} u_i = 0_V; i<σ(n)ui=(i<nui)+un\sum_{i<\sigma(n)} u_i = \bigl(\sum_{i<n} u_i\bigr) + u_n; and the value of i<nui\sum_{i<n} u_i depends only on u0,,un1u_0, \dots, u_{n-1}, so a list u:nVu : n \to V determines it (The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity, Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS).

[L3]

Induction on N\mathbb{N}: a property holding at 00 and passing from nn to σ(n)\sigma(n) holds at every natural number (The principle of mathematical induction).

[L4]

The vector space axioms (Vector space over a field): (V,+,0V)(V,+,0_V) is an abelian group, so ++ is associative and commutative and 0V0_V is a two-sided identity; (V2) λ(u+w)=λu+λw\lambda(u+w) = \lambda u + \lambda w; (V4) (λμ)w=λ(μw)(\lambda\mu)w = \lambda(\mu w); (V5) 1Fw=w1_F w = w.

[L6]

A linear subspace satisfies (W1) 0VW0_V \in W, (W2) closure under ++, (W3) closure under scalar multiplication; and a nonempty TVT \subseteq V with λu+vT\lambda u + v \in T for all λF\lambda \in F, u,vTu, v \in T is a linear subspace (Linear subspace of a vector space, One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W).

[L7]

σ(n)=n{n}\sigma(n) = n \cup \{n\} and nnn \notin n; n={mN:m<n}n = \{\, m \in \mathbb{N} : m < n \,\}; and 0n0 \in n whenever n0n \ne 0 (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

Proof

technique · direct
1.1

L(S)VL(S) \subseteq V by construction, and 0VL(S)0_V \in L(S): take n=0n = 0, whose only lists are the empty ones, and whose sum is the empty sum 0V0_V. In particular L(S)L(S) is nonempty.

L2
1.2

SL(S)S \subseteq L(S): for wSw \in S take n=1n = 1 with λ0=1F\lambda_0 = 1_F and v0=wv_0 = w, so that i<1λivi=0V+1Fw=1Fw=w\sum_{i<1} \lambda_i v_i = 0_V + 1_F w = 1_F w = w, using the recursion at σ(0)=1\sigma(0) = 1, the identity law and (V5).

L2L4
1.3

Extending a list. Let AA be a set, nNn \in \mathbb{N}, u:nAu : n \to A and xAx \in A. Since σ(n)=n{n}\sigma(n) = n \cup \{n\} and nnn \notin n, there is exactly one u:σ(n)Au' : \sigma(n) \to A with u(i)=u(i)u'(i) = u(i) for i<ni < n and u(n)=xu'(n) = x; and when A=VA = V, the recursion gives i<σ(n)ui=(i<nui)+x\sum_{i<\sigma(n)} u'_i = \bigl(\sum_{i<n} u_i\bigr) + x.

L2L7
1.4

Scalars pass through a finite sum: for every μF\mu \in F, every nNn \in \mathbb{N} and every list u:nVu : n \to V, μi<nui=i<nμui\mu \sum_{i<n} u_i = \sum_{i<n} \mu u_i. By induction on nn: at n=0n = 0 both sides are 0V0_V, since μ0V=0V\mu 0_V = 0_V; and if the identity holds at nn, then for a list on σ(n)\sigma(n) we get μi<σ(n)ui=μ(i<nui+un)=μi<nui+μun=i<nμui+μun=i<σ(n)μui\mu \sum_{i<\sigma(n)} u_i = \mu\bigl(\sum_{i<n} u_i + u_n\bigr) = \mu \sum_{i<n} u_i + \mu u_n = \sum_{i<n} \mu u_i + \mu u_n = \sum_{i<\sigma(n)} \mu u_i, by (V2), the inductive hypothesis and the recursion.

L2L3L4L5
1.5

A linear subspace WW with SWS \subseteq W contains every linear combination of elements of SS. By induction on nn: at n=0n = 0 the sum is 0VW0_V \in W by (W1); and if every such combination of length nn lies in WW, then for lists λ:σ(n)F\lambda : \sigma(n) \to F and v:σ(n)Sv : \sigma(n) \to S we have i<σ(n)λivi=(i<nλivi)+λnvn\sum_{i<\sigma(n)} \lambda_i v_i = \bigl(\sum_{i<n} \lambda_i v_i\bigr) + \lambda_n v_n, whose first summand lies in WW by the inductive hypothesis and whose second lies in WW by (W3) applied to vnSWv_n \in S \subseteq W, so the whole lies in WW by (W2).

L2L3L6
1.6

The only function v:nv : n \to \varnothing has n=0n = 0: if n0n \ne 0 then 0n0 \in n, and v(0)v(0) would be an element of \varnothing. So the only linear combination of elements of \varnothing is the empty sum, and L()={0V}L(\varnothing) = \{0_V\}.

L2L7
2.1

L(S)L(S) is closed under scalar multiplication: if w=i<nλiviw = \sum_{i<n} \lambda_i v_i with λ:nF\lambda : n \to F and v:nSv : n \to S, and μF\mu \in F, then μw=i<nμ(λivi)=i<n(μλi)vi\mu w = \sum_{i<n} \mu(\lambda_i v_i) = \sum_{i<n} (\mu\lambda_i) v_i by (V4), and iμλii \mapsto \mu\lambda_i is a list nFn \to F, so μwL(S)\mu w \in L(S).

step 1.4L4
2.2

L(S)L(S) is closed under addition. Fix xL(S)x \in L(S); we show by induction on nn that x+i<nμiviL(S)x + \sum_{i<n} \mu_i v_i \in L(S) for all lists μ:nF\mu : n \to F and v:nSv : n \to S. At n=0n = 0 the sum is 0V0_V and x+0V=xL(S)x + 0_V = x \in L(S). Assume it at nn and let μ:σ(n)F\mu : \sigma(n) \to F, v:σ(n)Sv : \sigma(n) \to S; then x+i<σ(n)μivi=(x+i<nμivi)+μnvnx + \sum_{i<\sigma(n)} \mu_i v_i = \bigl(x + \sum_{i<n} \mu_i v_i\bigr) + \mu_n v_n by the recursion and associativity, and y:=x+i<nμiviy := x + \sum_{i<n} \mu_i v_i lies in L(S)L(S) by the inductive hypothesis, say y=i<mνiwiy = \sum_{i<m} \nu_i w_i with ν:mF\nu : m \to F and w:mSw : m \to S; extending ν\nu by μn\mu_n and ww by vnv_n as in step 1.3 gives lists on σ(m)\sigma(m) whose combination is y+μnvny + \mu_n v_n, so x+i<σ(n)μiviL(S)x + \sum_{i<\sigma(n)} \mu_i v_i \in L(S).

step 1.3L2L3L4
2.3

L(S)span(S)L(S) \subseteq \operatorname{span}(S): the span is a linear subspace of VV containing SS, so by step 1.5 it contains every linear combination of elements of SS.

step 1.5L1
3.1

L(S)L(S) is a linear subspace of VV: it is nonempty, and for λF\lambda \in F and u,vL(S)u, v \in L(S) we have λuL(S)\lambda u \in L(S) and then λu+vL(S)\lambda u + v \in L(S), so the one-step test applies.

step 1.1step 2.1step 2.2L6
4.1

span(S)L(S)\operatorname{span}(S) \subseteq L(S): by steps 1.2 and 3.1 the set L(S)L(S) is a linear subspace of VV containing SS, and the span is contained in every such subspace.

step 1.2step 3.1L1
5.1

Combining the two inclusions, span(S)=L(S)\operatorname{span}(S) = L(S).

step 2.3step 4.1
6.1

Taking S=S = \varnothing and using step 1.6 gives span()=L()={0V}\operatorname{span}(\varnothing) = L(\varnothing) = \{0_V\}; and for arbitrary SS, the empty combination shows 0VL(S)=span(S)0_V \in L(S) = \operatorname{span}(S).

step 1.1step 1.6step 5.1

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The span is monotone and idempotent, span(S)=S\operatorname{span}(S) = S exactly when SS is a linear subspace, and span(S{0V})=span(S)\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S)

Statement

Let VV be a vector space over a field FF (Vector space over a field) and let S,TVS, T \subseteq V. Then:

  1. Extensive. Sspan(S)S \subseteq \operatorname{span}(S).
  2. Monotone. If STS \subseteq T then span(S)span(T)\operatorname{span}(S) \subseteq \operatorname{span}(T).
  3. Idempotent. span(span(S))=span(S)\operatorname{span}(\operatorname{span}(S)) = \operatorname{span}(S).
  4. span(S)=S\operatorname{span}(S) = S if and only if SS is a linear subspace of VV (Linear subspace of a vector space).
  5. span(S{0V})=span(S)\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S).

Facts & Assumptions

Given: A field FF, a vector space VV over FF, and subsets S,TVS, T \subseteq V.

[L1]

span(S)\operatorname{span}(S) is a linear subspace of VV, it contains SS, and it is contained in every linear subspace of VV that contains SS; the same holds with TT or any other subset in place of SS (Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS).

[L2]

Every linear subspace of VV contains 0V0_V, by condition (W1) (Linear subspace of a vector space).

Proof

technique · direct
1.1

Claim 1 is part of the defining description of the span: it contains SS.

L1
1.2

Claim 2. Suppose STS \subseteq T. Then span(T)\operatorname{span}(T) is a linear subspace of VV containing TT, hence containing SS; since span(S)\operatorname{span}(S) is contained in every linear subspace containing SS, we get span(S)span(T)\operatorname{span}(S) \subseteq \operatorname{span}(T).

L1
1.3

If SS is a linear subspace of VV, then SS is itself a linear subspace containing SS, so span(S)S\operatorname{span}(S) \subseteq S; together with Sspan(S)S \subseteq \operatorname{span}(S) this gives span(S)=S\operatorname{span}(S) = S.

L1
1.4

Conversely, if span(S)=S\operatorname{span}(S) = S then SS is a linear subspace of VV, because span(S)\operatorname{span}(S) is one.

L1
1.5

0Vspan(S)0_V \in \operatorname{span}(S), since span(S)\operatorname{span}(S) is a linear subspace of VV.

L1L2
2.1

Steps 1.3 and 1.4 together are claim 4.

step 1.3step 1.4
2.2

Claim 5. From SS{0V}S \subseteq S \cup \{0_V\} and step 1.2 we get span(S)span(S{0V})\operatorname{span}(S) \subseteq \operatorname{span}(S \cup \{0_V\}). Conversely Sspan(S)S \subseteq \operatorname{span}(S) by step 1.1 and 0Vspan(S)0_V \in \operatorname{span}(S) by step 1.5, so S{0V}span(S)S \cup \{0_V\} \subseteq \operatorname{span}(S), and since span(S)\operatorname{span}(S) is a linear subspace containing S{0V}S \cup \{0_V\}, minimality gives span(S{0V})span(S)\operatorname{span}(S \cup \{0_V\}) \subseteq \operatorname{span}(S).

step 1.1step 1.2step 1.5L1
3.1

Claim 3. The set span(S)\operatorname{span}(S) is a linear subspace of VV, so applying claim 4 to it gives span(span(S))=span(S)\operatorname{span}(\operatorname{span}(S)) = \operatorname{span}(S).

step 2.1L1
4.1

Claims 1, 2, 3, 4 and 5 are steps 1.1, 1.2, 3.1, 2.1 and 2.2 respectively.

step 1.1step 1.2step 2.1step 2.2step 3.1

Remarks

  • These three properties are exactly what makes the span a closure operator on the subsets of VV: extensive, monotone and idempotent. The closed sets of that operator are the linear subspaces, which is the content of claim 4. The subgroup generated by a subset (The subgroup S\langle S \rangle generated by a subset, the cyclic subgroup g\langle g \rangle, and cyclic groups) is the closure operator of the same shape on the subsets of a group.

  • Claim 5 says 0V0_V is invisible to the span. Adding or deleting the zero vector changes nothing, since every linear subspace contains it. It does not follow, and is not claimed here, that deleting any other single vector changes nothing: that question is about linear independence and belongs to a later page.

  • Claim 2 is used constantly in the form "a bigger set spans more". It is what lets a spanning set be enlarged freely, and, with claim 3, what lets the span be computed in stages: spanning a set, then spanning the result, gains nothing.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

span{v}={λv:λF}\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}, which is {0V}\{0_V\} when v=0Vv = 0_V, and when v0Vv \ne 0_V contains 0V0_V only as the multiple 0Fv0_F v

Statement

Let VV be a vector space over a field FF (Vector space over a field) and let vVv \in V. Write Fv:={λv:λF}Fv := \{\, \lambda v : \lambda \in F \,\}. Then:

  1. span{v}=Fv\operatorname{span}\{v\} = Fv;
  2. if v=0Vv = 0_V then span{v}={0V}\operatorname{span}\{v\} = \{0_V\};
  3. if v0Vv \ne 0_V then, for λ,μF\lambda, \mu \in F, λv=μv\lambda v = \mu v holds only when λ=μ\lambda = \mu; in particular λv=0V\lambda v = 0_V holds only for λ=0F\lambda = 0_F, so 0V0_V occurs in span{v}\operatorname{span}\{v\} only as the multiple 0Fv0_F v, and span{v}{0V}\operatorname{span}\{v\} \ne \{0_V\}.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, and a vector vVv \in V.

[L1]

span{v}\operatorname{span}\{v\} is a linear subspace of VV containing vv, and it is contained in every linear subspace of VV containing vv (Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS).

[L2]

A linear subspace is closed under scalar multiplication, by condition (W3) (Linear subspace of a vector space).

[L3]

One-step test: a nonempty TVT \subseteq V with λu+wT\lambda u + w \in T for all λF\lambda \in F and u,wTu, w \in T is a linear subspace of VV (One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W).

[L4]

The vector space axioms (Vector space over a field): (V3) (λ+μ)w=λw+μw(\lambda+\mu)w = \lambda w + \mu w; (V4) (λμ)w=λ(μw)(\lambda\mu)w = \lambda(\mu w); (V5) 1Fw=w1_F w = w.

[L5]

0Fw=0V0_F w = 0_V and λ0V=0V\lambda 0_V = 0_V for all λF\lambda \in F and wVw \in V; (λ)w=(λw)(-\lambda)w = -(\lambda w), which is claim 3 there; and if λw=0V\lambda w = 0_V then λ=0F\lambda = 0_F or w=0Vw = 0_V (In any vector space 0Fv=0V0_F v = 0_V, λ0V=0V\lambda 0_V = 0_V, (λ)v=(λv)(-\lambda)v = -(\lambda v), (1F)v=v(-1_F)v = -v, and λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F or v=0Vv = 0_V).

[L6]

FF is a field, so (F,+,0F)(F,+,0_F) is an abelian group with 0F,1FF0_F, 1_F \in F and an additive inverse μ-\mu for each μ\mu; adding μ\mu to both sides of λ+(μ)=0F\lambda + (-\mu) = 0_F therefore gives λ=μ\lambda = \mu (Field).

Proof

technique · direct
1.1

FvFv is nonempty, since 0Fv=0V0_F v = 0_V lies in it.

L5
1.2

FvFv is closed under the one-step expression: for λ,μ,νF\lambda, \mu, \nu \in F, λ(μv)+νv=(λμ)v+νv=(λμ+ν)vFv\lambda(\mu v) + \nu v = (\lambda\mu)v + \nu v = (\lambda\mu + \nu)v \in Fv, by (V4) and (V3).

L4
1.3

vFvv \in Fv, since v=1Fvv = 1_F v by (V5).

L4
1.4

If WW is a linear subspace of VV with vWv \in W, then λvW\lambda v \in W for every λF\lambda \in F, so FvWFv \subseteq W.

L2
1.5

If λv=μv\lambda v = \mu v then 0V=λv+((μv))=λv+(μ)v=(λ+(μ))v0_V = \lambda v + (-(\mu v)) = \lambda v + (-\mu)v = (\lambda + (-\mu))v, using claim 3 of the elementary consequences and (V3); so λ+(μ)=0F\lambda + (-\mu) = 0_F or v=0Vv = 0_V.

L4L5
2.1

FvFv is a linear subspace of VV containing vv, by the one-step test.

step 1.1step 1.2step 1.3L3
2.2

If v0Vv \ne 0_V and λv=μv\lambda v = \mu v, then step 1.5 forces λ+(μ)=0F\lambda + (-\mu) = 0_F, that is λ=μ\lambda = \mu; taking μ=0F\mu = 0_F and using 0Fv=0V0_F v = 0_V gives that λv=0V\lambda v = 0_V only for λ=0F\lambda = 0_F.

step 1.5L5L6
3.1

span{v}=Fv\operatorname{span}\{v\} = Fv: the span is contained in FvFv because FvFv is a linear subspace containing vv, and FvFv is contained in the span because the span is a linear subspace containing vv. This is claim 1.

step 2.1step 1.4L1
4.1

If v=0Vv = 0_V then every scalar multiple is λ0V=0V\lambda 0_V = 0_V, so Fv={0V}Fv = \{0_V\}; combined with claim 1 this is claim 2.

step 3.1L5
4.2

Suppose v0Vv \ne 0_V. Then λv=μv\lambda v = \mu v forces λ=μ\lambda = \mu, and λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F; moreover v=1Fvv = 1_F v lies in FvFv, which is span{v}\operatorname{span}\{v\} by claim 1, and v0Vv \ne 0_V, so span{v}{0V}\operatorname{span}\{v\} \ne \{0_V\}. This is claim 3.

step 2.2step 3.1L4
5.1

Claims 1, 2 and 3 are steps 3.1, 4.1 and 4.2.

step 3.1step 4.1step 4.2

Remarks

DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family

Definition

Let VV be a vector space over a field FF (Vector space over a field), let nNn \in \mathbb{N}, and let UU be a finite family of linear subspaces of VV, that is a function assigning to each i<ni < n a linear subspace UiU_i of VV (Linear subspace of a vector space); here n={0,,n1}n = \{0, \dots, n-1\} (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n), so the family is indexed from 00. Define

i<nUi  :=  {i<nui  :  u:nV with uiUi for every i<n},\sum_{i<n} U_i \;:=\; \Bigl\{\, \sum_{i<n} u_i \;:\; u : n \to V \text{ with } u_i \in U_i \text{ for every } i < n \,\Bigr\},

the finite sums being those of The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity read additively in the abelian group (V,+,0V)(V,+,0_V), as in Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS. For two linear subspaces U,WU, W of VV we write

U+W  :=  {u+w  :  uU, wW},U + W \;:=\; \{\, u + w \;:\; u \in U,\ w \in W \,\},

which is the case n=2n = 2 of the display above, since i<2ui=(0V+u0)+u1=u0+u1\sum_{i<2} u_i = (0_V + u_0) + u_1 = u_0 + u_1.

Three facts about finite sums of vectors

All three are proved by induction on nn (The principle of mathematical induction) from the two defining clauses i<0ui=0V\sum_{i<0} u_i = 0_V and i<σ(n)ui=(i<nui)+un\sum_{i<\sigma(n)} u_i = \bigl(\sum_{i<n} u_i\bigr) + u_n (The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity), together with the abelian group laws of (V,+,0V)(V,+,0_V). 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 0V0_V. If z:nVz : n \to V has zi=0Vz_i = 0_V for every i<ni < n, then i<nzi=0V\sum_{i<n} z_i = 0_V. At n=0n = 0 this is the empty sum, and if it holds at nn then i<σ(n)zi=0V+0V=0V\sum_{i<\sigma(n)} z_i = 0_V + 0_V = 0_V.

(F2) The mixed identity. For every λF\lambda \in F and all lists u,w:nVu, w : n \to V,

λi<nui  +  i<nwi  =  i<n(λui+wi).\lambda \sum_{i<n} u_i \;+\; \sum_{i<n} w_i \;=\; \sum_{i<n} (\lambda u_i + w_i).

At n=0n = 0 both sides are 0V0_V, since λ0V=0V\lambda 0_V = 0_V (In any vector space 0Fv=0V0_F v = 0_V, λ0V=0V\lambda 0_V = 0_V, (λ)v=(λv)(-\lambda)v = -(\lambda v), (1F)v=v(-1_F)v = -v, and λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F or v=0Vv = 0_V). If the identity holds at nn, then at σ(n)\sigma(n) the left-hand side is λ(i<nui+un)+(i<nwi+wn)\lambda\bigl(\sum_{i<n} u_i + u_n\bigr) + \bigl(\sum_{i<n} w_i + w_n\bigr), which by axiom (V2) equals (λi<nui+λun)+(i<nwi+wn)\bigl(\lambda\sum_{i<n} u_i + \lambda u_n\bigr) + \bigl(\sum_{i<n} w_i + w_n\bigr); commutativity and associativity of ++ regroup this as (λi<nui+i<nwi)+(λun+wn)\bigl(\lambda\sum_{i<n} u_i + \sum_{i<n} w_i\bigr) + (\lambda u_n + w_n), which by the inductive hypothesis is i<n(λui+wi)+(λun+wn)=i<σ(n)(λui+wi)\sum_{i<n}(\lambda u_i + w_i) + (\lambda u_n + w_n) = \sum_{i<\sigma(n)}(\lambda u_i + w_i).

(F3) Extracting one term. Let u:nVu : n \to V and j<nj < n, and let u(j):nVu^{(j)} : n \to V agree with uu at every iji \ne j and satisfy uj(j)=0Vu^{(j)}_j = 0_V. Then

i<nui  =  uj+i<nui(j).\sum_{i<n} u_i \;=\; u_j + \sum_{i<n} u^{(j)}_i .

At n=0n = 0 there is no j<0j < 0 and the claim is vacuous. Assume it at nn and let j<σ(n)j < \sigma(n), so jnj \le n (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n). If j=nj = n, then u(n)u^{(n)} agrees with uu on nn, so i<σ(n)ui(n)=i<nui+0V=i<nui\sum_{i<\sigma(n)} u^{(n)}_i = \sum_{i<n} u_i + 0_V = \sum_{i<n} u_i, and un+i<nui=i<nui+un=i<σ(n)uiu_n + \sum_{i<n} u_i = \sum_{i<n} u_i + u_n = \sum_{i<\sigma(n)} u_i by commutativity. If j<nj < n, then u(j)u^{(j)} agrees with uu at nn, so i<σ(n)ui(j)=i<nui(j)+un\sum_{i<\sigma(n)} u^{(j)}_i = \sum_{i<n} u^{(j)}_i + u_n, and the inductive hypothesis applied to the restriction of uu to nn gives i<σ(n)ui=(uj+i<nui(j))+un=uj+i<σ(n)ui(j)\sum_{i<\sigma(n)} u_i = \bigl(u_j + \sum_{i<n} u^{(j)}_i\bigr) + u_n = u_j + \sum_{i<\sigma(n)} u^{(j)}_i, by associativity.

A consequence of (F1) and (F3). If ui=0Vu_i = 0_V for every iji \ne j, then u(j)u^{(j)} is the all-zero list, so i<nui=uj+0V=uj\sum_{i<n} u_i = u_j + 0_V = u_j: a list vanishing off a single index sums to its value at that index.

The sum is a linear subspace

i<nUi\sum_{i<n} U_i is a linear subspace of VV. It is nonempty: each UiU_i contains 0V0_V, and the all-zero list sums to 0V0_V by (F1), so 0Vi<nUi0_V \in \sum_{i<n} U_i. And it satisfies the one-step test (One-step subspace test: a nonempty WVW \subseteq V is a linear subspace if and only if λu+vW\lambda u + v \in W for all λF\lambda \in F and u,vWu, v \in W): if x=i<nuix = \sum_{i<n} u_i and y=i<nwiy = \sum_{i<n} w_i with ui,wiUiu_i, w_i \in U_i, and λF\lambda \in F, then (F2) gives λx+y=i<n(λui+wi)\lambda x + y = \sum_{i<n} (\lambda u_i + w_i), and λui+wiUi\lambda u_i + w_i \in U_i because UiU_i is a linear subspace, so λx+yi<nUi\lambda x + y \in \sum_{i<n} U_i.

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

The boundary case

N\mathbb{N} contains 00, so n=0n = 0 is a genuine case. The only list u:0Vu : 0 \to V is the empty function, and its sum is the empty sum 0V0_V, so

i<0Ui  =  {0V},\sum_{i<0} U_i \;=\; \{0_V\},

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)\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr), so the sum is the smallest linear subspace containing every UiU_i and of the boundary case of Internal direct sum V=i<nUiV = \bigoplus_{i<n} U_i: the sum is everything and each summand meets the sum of the others only in 0V0_V.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

i<nUi=span(i<nUi)\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr), so the sum is the smallest linear subspace containing every UiU_i

Statement

Let VV be a vector space over a field FF (Vector space over a field), let nNn \in \mathbb{N}, and let UU be a finite family of linear subspaces UiU_i of VV indexed by i<ni < n (The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family). Write

i<nUi  =  {xV  :  xUi for some i<n}.\bigcup_{i<n} U_i \;=\; \{\, x \in V \;:\; x \in U_i \text{ for some } i < n \,\}.

Then

i<nUi  =  span(i<nUi),\sum_{i<n} U_i \;=\; \operatorname{span}\Bigl(\bigcup_{i<n} U_i\Bigr),

so i<nUi\sum_{i<n} U_i is the smallest linear subspace of VV containing UiU_i for every i<ni < n: it contains each UiU_i, and it is contained in every linear subspace of VV that contains each UiU_i.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, a natural number nn, and a family of linear subspaces UiU_i of VV indexed by i<ni < n.

[L1]

i<nUi\sum_{i<n} U_i is a linear subspace of VV whose elements are exactly the vectors i<nui\sum_{i<n} u_i with uiUiu_i \in U_i for every i<ni < n; and a list vanishing off a single index j<nj < n sums to its value at jj (The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family).

[L2]

For TVT \subseteq V, the span span(T)\operatorname{span}(T) is a linear subspace of VV containing TT and contained in every linear subspace of VV containing TT (Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS).

[L3]

A linear subspace contains 0V0_V by (W1) and is closed under ++ by (W2) (Linear subspace of a vector space).

[L4]

Finite sums in (V,+,0V)(V,+,0_V): i<0ui=0V\sum_{i<0} u_i = 0_V and i<σ(m)ui=(i<mui)+um\sum_{i<\sigma(m)} u_i = \bigl(\sum_{i<m} u_i\bigr) + u_m (The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity, Linear combination of a finite list, and the span span(S)\operatorname{span}(S) as the smallest linear subspace containing SS).

[L5]

Induction on N\mathbb{N}, whose elements are the von Neumann naturals with m={k:k<m}m = \{\, k : k < m \,\} (The principle of mathematical induction, The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

Proof

technique · direct
1.1

Each UjU_j with j<nj < n is contained in i<nUi\sum_{i<n} U_i: given xUjx \in U_j, let u:nVu : n \to V be the list with uj=xu_j = x and ui=0Vu_i = 0_V for iji \ne j; then uiUiu_i \in U_i for every i<ni < n, since each UiU_i contains 0V0_V, and this list sums to xx.

L1L3
1.2

A linear subspace WW of VV is closed under finite sums: for every mNm \in \mathbb{N} and every list u:mWu : m \to W, the vector i<mui\sum_{i<m} u_i lies in WW. By induction on mm: at m=0m = 0 the sum is 0VW0_V \in W by (W1), and if it holds at mm then i<σ(m)ui=(i<mui)+um\sum_{i<\sigma(m)} u_i = \bigl(\sum_{i<m} u_i\bigr) + u_m lies in WW by the inductive hypothesis and (W2).

L3L4L5
2.1

i<nUii<nUi\bigcup_{i<n} U_i \subseteq \sum_{i<n} U_i by step 1.1, and i<nUi\sum_{i<n} U_i is a linear subspace of VV, so the span of the union is contained in it: span(i<nUi)i<nUi\operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr) \subseteq \sum_{i<n} U_i.

step 1.1L1L2
2.2

Conversely, span(i<nUi)\operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr) is a linear subspace of VV containing the union, hence containing each UiU_i; so any list u:nVu : n \to V with uiUiu_i \in U_i for every i<ni < n takes its values in it, and step 1.2 gives i<nuispan(i<nUi)\sum_{i<n} u_i \in \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr). As these vectors are exactly the elements of i<nUi\sum_{i<n} U_i, that yields i<nUispan(i<nUi)\sum_{i<n} U_i \subseteq \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr).

step 1.2L1L2
3.1

The two inclusions give i<nUi=span(i<nUi)\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr).

step 2.1step 2.2
4.1

A linear subspace of VV contains i<nUi\bigcup_{i<n} U_i exactly when it contains UiU_i for every i<ni < n, so the span of the union is the smallest linear subspace containing every UiU_i; by step 3.1 the sum is that subspace.

step 3.1L2

Remarks

DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Internal direct sum V=i<nUiV = \bigoplus_{i<n} U_i: the sum is everything and each summand meets the sum of the others only in 0V0_V

Definition

Let VV be a vector space over a field FF (Vector space over a field), let nNn \in \mathbb{N}, and let UU be a finite family of linear subspaces UiU_i of VV indexed by i<ni < n (Linear subspace of a vector space, The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family); as everywhere on this page the index runs over the von Neumann natural n={0,,n1}n = \{0, \dots, n-1\} (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

The sum of the other summands. The set {0V}\{0_V\} is a linear subspace of VV: it contains 0V0_V, it is closed under addition since 0V+0V=0V0_V + 0_V = 0_V, and it is closed under scalar multiplication since λ0V=0V\lambda 0_V = 0_V (In any vector space 0Fv=0V0_F v = 0_V, λ0V=0V\lambda 0_V = 0_V, (λ)v=(λv)(-\lambda)v = -(\lambda v), (1F)v=v(-1_F)v = -v, and λv=0V\lambda v = 0_V forces λ=0F\lambda = 0_F or v=0Vv = 0_V). So for each j<nj < n the family U(j)U^{(j)} defined by

Ui(j):=Ui(ij),Uj(j):={0V}U^{(j)}_i := U_i \quad (i \ne j), \qquad U^{(j)}_j := \{0_V\}

is again a finite family of linear subspaces of VV indexed by i<ni < n, and we write

ijUi  :=  i<nUi(j),\sum_{i \ne j} U_i \;:=\; \sum_{i<n} U^{(j)}_i ,

a linear subspace of VV by The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family. Replacing the jj-th summand by {0V}\{0_V\}, rather than re-indexing over a smaller set, keeps every family on this page indexed by a natural number.

The definition. VV is the internal direct sum of the family UU, written

V  =  i<nUi,V \;=\; \bigoplus_{i<n} U_i ,

when both of the following hold:

  • (D1) i<nUi=V\displaystyle\sum_{i<n} U_i = V;
  • (D2) for every j<nj < n, UjijUi={0V}\displaystyle U_j \cap \sum_{i \ne j} U_i = \{0_V\}.

In (D2) the inclusion \supseteq is automatic, since UjU_j and ijUi\sum_{i \ne j} U_i are linear subspaces and each therefore contains 0V0_V; the content of (D2) is the inclusion \subseteq, that no nonzero vector of UjU_j is a sum of vectors drawn from the other summands.

Two summands

Take n=2n = 2 and write U:=U0U := U_0, W:=U1W := U_1. For j=0j = 0 the family U(0)U^{(0)} is {0V},W\{0_V\}, W, so i0Ui={0V+w:wW}=W\sum_{i \ne 0} U_i = \{\, 0_V + w : w \in W \,\} = W; for j=1j = 1 it is UU in the same way. So (D2) reduces to the single condition UW={0V}U \cap W = \{0_V\}, and

V=UWmeansU+W=V  and  UW={0V}.V = U \oplus W \quad\text{means}\quad U + W = V \ \text{ and } \ U \cap W = \{0_V\}.

For two summands, therefore, (D2) and the pairwise condition coincide; this is the familiar form of the definition.

Three or more summands: (D2) is not the pairwise condition

For n3n \ge 3 the condition (D2) is strictly stronger than requiring UiUj={0V}U_i \cap U_j = \{0_V\} for all iji \ne j.

That (D2) implies the pairwise condition is immediate: for iji \ne j with i,j<ni, j < n we have Ui=Ui(j)ijUiU_i = U^{(j)}_i \subseteq \sum_{i \ne j} U_i, since a sum of a family contains each of its summands (i<nUi=span(i<nUi)\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr), so the sum is the smallest linear subspace containing every UiU_i), so UjUiUjijUi={0V}U_j \cap U_i \subseteq U_j \cap \sum_{i \ne j} U_i = \{0_V\}, and the reverse inclusion holds because both are linear subspaces.

The converse fails, and it fails already for three summands: a family can satisfy (D1) and have all its pairwise intersections trivial while (D2) is false, so that decompositions are not unique. The companion examples page records a witness. A definition stated with the pairwise condition in place of (D2) would therefore be a different, and weaker, notion, and the characterisation by unique decomposition (V=i<nUiV = \bigoplus_{i<n} U_i if and only if every vVv \in V is i<nui\sum_{i<n} u_i with uiUiu_i \in U_i in exactly one way; equivalently, if and only if the sum is VV and i<nui=0V\sum_{i<n} u_i = 0_V with uiUiu_i \in U_i forces every ui=0Vu_i = 0_V) would be false for it.

The empty family

N\mathbb{N} contains 00, so n=0n = 0 is a genuine case. Then i<0Ui={0V}\sum_{i<0} U_i = \{0_V\} (The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family) and (D2) is vacuous, there being no j<0j < 0. So V=i<0UiV = \bigoplus_{i<0} U_i holds exactly when V={0V}V = \{0_V\}: the zero space is the direct sum of the empty family, and no other space is.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

V=i<nUiV = \bigoplus_{i<n} U_i if and only if every vVv \in V is i<nui\sum_{i<n} u_i with uiUiu_i \in U_i in exactly one way; equivalently, if and only if the sum is VV and i<nui=0V\sum_{i<n} u_i = 0_V with uiUiu_i \in U_i forces every ui=0Vu_i = 0_V

Statement

Let VV be a vector space over a field FF (Vector space over a field), let nNn \in \mathbb{N}, and let UU be a finite family of linear subspaces UiU_i of VV indexed by i<ni < n (The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family). Call a list u:nVu : n \to V admissible when uiUiu_i \in U_i for every i<ni < n. The following are equivalent.

Facts & Assumptions

Given: A field FF, a vector space VV over FF, a natural number nn, and a finite family of linear subspaces UiU_i of VV indexed by i<ni < n; a list u:nVu : n \to V is called admissible when uiUiu_i \in U_i for every i<ni < n.

[L1]

V=i<nUiV = \bigoplus_{i<n} U_i means (D1) i<nUi=V\sum_{i<n} U_i = V and (D2) UjijUi={0V}U_j \cap \sum_{i \ne j} U_i = \{0_V\} for every j<nj < n, where ijUi=i<nUi(j)\sum_{i \ne j} U_i = \sum_{i<n} U^{(j)}_i for the family U(j)U^{(j)} with Ui(j)=UiU^{(j)}_i = U_i for iji \ne j and Uj(j)={0V}U^{(j)}_j = \{0_V\} (Internal direct sum V=i<nUiV = \bigoplus_{i<n} U_i: the sum is everything and each summand meets the sum of the others only in 0V0_V).

[L2]

The elements of i<nUi\sum_{i<n} U_i are exactly the vectors i<nui\sum_{i<n} u_i with uu admissible; it is a linear subspace of VV; the mixed identity (F2) λi<nui+i<nwi=i<n(λui+wi)\lambda \sum_{i<n} u_i + \sum_{i<n} w_i = \sum_{i<n}(\lambda u_i + w_i) holds; and by (F3) with (F1), i<nui=uj+i<nui(j)\sum_{i<n} u_i = u_j + \sum_{i<n} u^{(j)}_i for j<nj < n, where u(j)u^{(j)} agrees with uu off jj and has uj(j)=0Vu^{(j)}_j = 0_V, while a list vanishing off a single index sums to its value there (The sum U+WU + W of two linear subspaces and the sum i<nUi\sum_{i<n} U_i of a finite family, The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity).

[L3]

A linear subspace contains 0V0_V and is closed under ++ and under scalar multiplication (Linear subspace of a vector space).

[L5]

Cancellation in the abelian group (V,+,0V)(V,+,0_V): if x+y=x+zx + y = x + z then y=zy = z, and if y+x=z+xy + x = z + x then y=zy = z (Cancellation in a group: gx=gygx = gy or xg=ygxg = yg forces x=yx = y; equivalently left and right translation by gg are bijections of GG, so gx=hgx = h and xg=hxg = h each have exactly one solution, Group and abelian group).

[L6]

(V,+,0V)(V,+,0_V) is an abelian group: ++ is associative and commutative, 0V0_V is a two-sided identity, and each xx has an additive inverse x-x with x+(x)=0V=(x)+xx + (-x) = 0_V = (-x) + x (Vector space over a field, Group and abelian group).

[L7]

The index ii runs over the von Neumann natural n={0,,n1}n = \{0,\dots,n-1\} (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

Proof

technique · direct
1.1

Let uu be admissible and j<nj < n. The list u(j)u^{(j)} is admissible for the family U(j)U^{(j)}, since ui(j)=uiUi=Ui(j)u^{(j)}_i = u_i \in U_i = U^{(j)}_i for iji \ne j and uj(j)=0V{0V}=Uj(j)u^{(j)}_j = 0_V \in \{0_V\} = U^{(j)}_j; hence s:=i<nui(j)s := \sum_{i<n} u^{(j)}_i lies in ijUi\sum_{i \ne j} U_i, and i<nui=uj+s\sum_{i<n} u_i = u_j + s.

L1L2L7
1.2

A linear subspace WW of VV is closed under additive inverses: for xWx \in W we have (1F)xW(-1_F)x \in W by closure under scalar multiplication, and (1F)x=x(-1_F)x = -x.

L3L4
1.3

Let j<nj < n and xUjx \in U_j. The list z:nVz : n \to V with zj=xz_j = x and zi=0Vz_i = 0_V for iji \ne j is admissible, each UiU_i containing 0V0_V, and it sums to xx.

L2L3L7
1.4

(c) implies (b). Assume (c). Existence: since i<nUi=V\sum_{i<n} U_i = V, every vVv \in V is i<nui\sum_{i<n} u_i for some admissible uu. Uniqueness: suppose uu and ww are admissible with i<nui=i<nwi=:v\sum_{i<n} u_i = \sum_{i<n} w_i =: v. The mixed identity with λ=1F\lambda = -1_F, applied to ww and uu in that order, gives (1F)i<nwi+i<nui=i<n((1F)wi+ui)(-1_F)\sum_{i<n} w_i + \sum_{i<n} u_i = \sum_{i<n}\bigl((-1_F)w_i + u_i\bigr), whose left-hand side is v+v=0V-v + v = 0_V; the list i(1F)wi+ui=(wi)+uii \mapsto (-1_F)w_i + u_i = (-w_i) + u_i is admissible, each UiU_i being closed under additive inverses and addition; so by (c) every (wi)+ui=0V=(wi)+wi(-w_i) + u_i = 0_V = (-w_i) + w_i, and cancelling wi-w_i on the left gives ui=wiu_i = w_i for every i<ni < n.

L2L3L4L5L6
2.1

(a) implies (c). Assume (a). Condition (D1) is the first half of (c). For the second, let uu be admissible with i<nui=0V\sum_{i<n} u_i = 0_V and let j<nj < n. Writing s=i<nui(j)ijUis = \sum_{i<n} u^{(j)}_i \in \sum_{i \ne j} U_i, we get uj+s=0Vu_j + s = 0_V, while (s)+s=0V(-s) + s = 0_V as well, so cancelling ss on the right gives uj=su_j = -s; and sijUi-s \in \sum_{i \ne j} U_i because that set is a linear subspace. Hence ujUjijUiu_j \in U_j \cap \sum_{i \ne j} U_i, which is {0V}\{0_V\} by (D2), so uj=0Vu_j = 0_V. As j<nj < n was arbitrary, uu is the all-zero list.

step 1.1step 1.2L1L2L5L6
2.2

(b) implies (a). Assume (b). For (D1): every vVv \in V is i<nui\sum_{i<n} u_i for some admissible uu, so Vi<nUiV \subseteq \sum_{i<n} U_i, and the reverse inclusion holds because i<nUi\sum_{i<n} U_i is a subset of VV. For (D2): let j<nj < n and xUjijUix \in U_j \cap \sum_{i \ne j} U_i. Then x=i<nwix = \sum_{i<n} w_i for some list ww admissible for U(j)U^{(j)}; such a ww has wj=0Vw_j = 0_V and wiUiw_i \in U_i for iji \ne j, so it is admissible for UU as well, UjU_j containing 0V0_V. The list zz of step 1.3 is also admissible and also sums to xx, so uniqueness in (b) forces z=wz = w, and in particular x=zj=wj=0Vx = z_j = w_j = 0_V. Since {0V}\{0_V\} is contained in the intersection anyway, (D2) holds.

step 1.3L1L2L3
3.1

Steps 2.1, 1.4 and 2.2 give (a) implies (c), (c) implies (b) and (b) implies (a), so the three conditions are equivalent.

step 1.4step 2.1step 2.2

Remarks

  • Condition (c) is the one used in practice. Checking uniqueness of every decomposition is checking a single one: that of 0V0_V. The reduction is the content of the implication from (c) to (b), and it works because the difference of two admissible decompositions of the same vector is an admissible decomposition of 0V0_V.

  • This is what makes (D2) the right condition. If the definition of a direct sum had asked only for pairwise trivial intersections, the equivalence above would fail for n3n \ge 3: the companion examples page exhibits three linear subspaces of a plane whose pairwise intersections are trivial, whose sum is everything, and for which some vector has two different decompositions. So the equivalence proved here is not available for the pairwise notion, and (D2) is exactly the strengthening that restores it.

  • The two-summand case reads as usual. For n=2n = 2, condition (a) says U+W=VU + W = V and UW={0V}U \cap W = \{0_V\} (Internal direct sum V=i<nUiV = \bigoplus_{i<n} U_i: the sum is everything and each summand meets the sum of the others only in 0V0_V), and the lemma says that this holds exactly when every vVv \in V is u+wu + w with uUu \in U and wWw \in W in exactly one way.

  • No finiteness of VV and no dimension anywhere. The family of summands is finite because the sum i<nUi\sum_{i<n} U_i is defined through a finite sum of vectors; VV itself is arbitrary, and nothing above counts anything.

5 · Examples, counterexamples and false statements

None yet.

Sources