CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge 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.

Every linear subspace $U$ of a vector space $V$ has a complement: a linear subspace $W$ with $V = U \oplus W$

Statement

Assume the Axiom of Choice, through Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$ , there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$ and Every vector space has a basis. Let $V$ be a vector space over a field $F$ (Vector space over a field) and let $U$ be a linear subspace of $V$ (Linear subspace of a vector space). Then there is a linear subspace $W$ of $V$ with

$V \;=\; U \oplus W$

(Internal direct sum $V = \bigoplus_{i<n} U_i$ : the sum is everything and each summand meets the sum of the others only in $0_V$ ), that is $U + W = V$ and $U \cap W = \{0_V\}$ .

No finiteness of $V$ , of $U$ or of any basis is assumed.

Facts & Assumptions

Given: The Axiom of Choice; a field $F$ ; a vector space $V$ over $F$ ; and a linear subspace $U$ of $V$ .

[L1]

$U$ is itself a vector space over $F$ , with the addition, the zero and the scalar multiplication of $V$ (Linear subspace of a vector space); every vector space has a basis (Every vector space has a basis); and for $A \subseteq U$ , " $A$ is a basis of $U$ " means $A$ is linearly independent as a subset of $V$ with $\operatorname{span}(A) = U$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, section on bases of a linear subspace, Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i<n} \lambda_i v_i = 0_V$ forces every $\lambda_i = 0_F$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

[L2]

If $L \subseteq S \subseteq V$ with $L$ linearly independent and $\operatorname{span}(S) = V$ , there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$ ; and $\operatorname{span}(V) = V$ (Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$ , there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$ , The span is monotone and idempotent, $\operatorname{span}(S) = S$ exactly when $S$ is a linear subspace, and $\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S)$ , claim 4).

[L3]

$\operatorname{span}(T)$ is a linear subspace of $V$ containing $T$ , contained in every linear subspace of $V$ containing $T$ , and monotone in $T$ (Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ , The span is monotone and idempotent, $\operatorname{span}(S) = S$ exactly when $S$ is a linear subspace, and $\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S)$ , $\operatorname{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $\operatorname{span}(\varnothing) = \{0_V\}$ ).

[L4]

For two linear subspaces, $U + W = \sum_{i<2}U_i$ and $\sum_{i<2}U_i = \operatorname{span}(U \cup W)$ (The sum $U + W$ of two linear subspaces and the sum $\sum_{i<n} U_i$ of a finite family, $\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ , so the sum is the smallest linear subspace containing every $U_i$ ).

[L5]

$\operatorname{span}(T)$ is already the set of $\sum_{i<p}\alpha_i a_i$ with $a : p \to T$ injective (A subset $S \subseteq V$ is linearly dependent if and only if some $s \in S$ lies in $\operatorname{span}(S \setminus \{s\})$ ; and $\operatorname{span}(S)$ is already the set of linear combinations of INJECTIVE finite lists into $S$ , claim 2).

[L6]

Concatenation: for $y : p \to X$ and $z : q \to X$ there is exactly one $c : p+q \to X$ with $c_i = y_i$ for $i < p$ and $c_{p+j} = z_j$ for $j < q$ ; when $X = V$ it satisfies $\sum_{i<p+q}c_i = \sum_{i<p}y_i + \sum_{j<q}z_j$ ; and if $y$ and $z$ are injective with disjoint images then $c$ is injective with image $y[p] \cup z[q]$ . A list into $V$ is linearly independent exactly when it is injective with linearly independent image (Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never $0_V$ , its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent, claims 3 and 6). The scalar case is the same statement read in $F$ , a vector space over itself (A field is a vector space over itself, and over any subfield $K \subseteq F$ every $F$ -vector space is a $K$ -vector space by restricting the scalars, claim 1).

[L7]

$(V,+,0_V)$ is an abelian group; $0_F y = 0_V$ ; $(-1_F)y = -y$ ; (V4) $(\lambda\mu)y = \lambda(\mu y)$ ; (F1) an all- $0_V$ list sums to $0_V$ ; and a scalar passes through a finite sum, so $(-1_F)\sum_{j<q}\beta_j b_j = \sum_{j<q}(-\beta_j)b_j$ (Vector space over a field, In any vector space $0_F v = 0_V$ , $\lambda 0_V = 0_V$ , $(-\lambda)v = -(\lambda v)$ , $(-1_F)v = -v$ , and $\lambda v = 0_V$ forces $\lambda = 0_F$ or $v = 0_V$ , Field, The sum $U + W$ of two linear subspaces and the sum $\sum_{i<n} U_i$ of a finite family, The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

[L8]

Indices run over von Neumann naturals (The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ) and injectivity is as in Injection, surjection, bijection.

Proof

technique · constructive

1.1

$U$ is a vector space over $F$ in its own right, so it has a basis $A$ ; equivalently $A \subseteq U$ is linearly independent as a subset of $V$ and $\operatorname{span}(A) = U$ .

L1construct

2.1

Since $A \subseteq V$ , $A$ is linearly independent and $\operatorname{span}(V) = V$ , the extension theorem supplies a basis $B$ of $V$ with $A \subseteq B \subseteq V$ . Put $W := \operatorname{span}(B \setminus A)$ , a linear subspace of $V$ .

step 1.1L2L3

3.1

$U + W = V$ . By step 2.1 and step 1.1 we have $A \subseteq \operatorname{span}(A) = U$ and $B \setminus A \subseteq \operatorname{span}(B \setminus A) = W$ , so $B = A \cup (B \setminus A) \subseteq U \cup W$ and hence $V = \operatorname{span}(B) \subseteq \operatorname{span}(U \cup W) = U + W$ . Conversely $\operatorname{span}(A) \subseteq \operatorname{span}(B)$ and $\operatorname{span}(B \setminus A) \subseteq \operatorname{span}(B)$ by monotonicity, so $U \cup W \subseteq \operatorname{span}(B) = V$ , and $\operatorname{span}(U \cup W) \subseteq V$ since $V$ is a linear subspace of itself containing $U \cup W$ .

step 1.1step 2.1L3L4

3.2

$U \cap W = \{0_V\}$ . Both are linear subspaces, so $0_V$ lies in the intersection. Conversely let $x \in U \cap W$ . Since $x \in \operatorname{span}(A)$ there are $p$ , an injective $a : p \to A$ and $\alpha : p \to F$ with $x = \sum_{i<p}\alpha_i a_i$ ; since $x \in \operatorname{span}(B \setminus A)$ there are $q$ , an injective $b : q \to B \setminus A$ and $\beta : q \to F$ with $x = \sum_{j<q}\beta_j b_j$ . The images $a[p] \subseteq A$ and $b[q] \subseteq B \setminus A$ are disjoint, so the concatenation $c : p+q \to B$ of $a$ and $b$ is injective, and the concatenation $\gamma : p+q \to F$ of $\alpha$ with $j \mapsto -\beta_j$ is a list of scalars; the list $i \mapsto \gamma_i c_i$ is the concatenation of $i \mapsto \alpha_i a_i$ and $j \mapsto (-\beta_j)b_j$ , so $\sum_{i<p+q}\gamma_i c_i = \sum_{i<p}\alpha_i a_i + \sum_{j<q}(-\beta_j)b_j = x + (-x) = 0_V$ . As $c$ is an injective list into the linearly independent set $B$ , it is a linearly independent list, so every $\gamma_i = 0_F$ ; in particular $\alpha_i = 0_F$ for every $i < p$ , whence every term $\alpha_i a_i$ is $0_V$ and $x = 0_V$ by (F1).

step 1.1step 2.1L5L6L7L8

4.1

Taking $W = \operatorname{span}(B \setminus A)$ , steps 3.1 and 3.2 give $U + W = V$ and $U \cap W = \{0_V\}$ , which for two summands is exactly $V = U \oplus W$ . So the required complement exists.

step 2.1step 3.1step 3.2L4discharge-construct∎

Remarks

The complement is not unique, and nothing above claims it is. In $F^{2}$ the span of the first standard unit vector has both the span of the second and the span of their sum as complements; the companion page uses those same three lines for a different failure, and the order-69 examples page uses them for a third. What the corollary produces is one complement, read off from one extension of one basis.
Choice is spent twice, in the same place. A basis of $U$ and an extension of it to a basis of $V$ both come from Zorn's lemma (Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$ , there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$ ). In finite dimension neither is needed: If $\dim_F V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_F U \le n$ , and $\dim_F U = n$ if and only if $U = V$ produces a basis of $U$ without any choice principle, and the same greatest-size argument extends it.
Why the intersection argument avoids ordered bases. For an infinite $B$ there is no ordered basis to compare coordinates in, so the argument runs on the finite injective lists that actually occur, supplied by A subset $S \subseteq V$ is linearly dependent if and only if some $s \in S$ lies in $\operatorname{span}(S \setminus \{s\})$ ; and $\operatorname{span}(S)$ is already the set of linear combinations of INJECTIVE finite lists into $S$ , and concatenates two of them into one list into $B$ . That is what makes the proof independent of any finiteness assumption.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 92 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Direct sum of modules (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed., Ch. 1 (standard reference, not scraped)
University of Colorado notes: Linear algebra and vector spaces (standard reference, not scraped)

Every linear subspace UUU of a vector space VVV has a complement: a linear subspace WWW with V=U⊕WV = U \oplus WV=U⊕W