CorollaryStatement: Literature-sourcedProof: AI-generatedSession-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 vector space has a basis

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$ . Then every vector space $V$ over a field $F$ (Vector space over a field) has a basis (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

In particular the zero space has a basis, namely $\varnothing$ .

Facts & Assumptions

Given: A field $F$ and a vector space $V$ over $F$ .

[L1]

$\varnothing$ is linearly independent (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]

$\operatorname{span}(T) = T$ if and only if $T$ is a linear subspace of $V$ , and $V$ is a linear subspace of itself (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, Linear subspace of a vector space, Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ).

[L3]

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$ (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$ ).

Proof

technique · direct

1.1

$V$ is a linear subspace of itself, so $\operatorname{span}(V) = V$ : the whole space satisfies the three closure conditions trivially, and the span of a linear subspace is that subspace.

1.2

The empty set is linearly independent and $\varnothing \subseteq V \subseteq V$ .

2.1

By steps 1.1 and 1.2 the extension theorem applies with $L := \varnothing$ and $S := V$ , and yields a basis $B$ of $V$ with $\varnothing \subseteq B \subseteq V$ ; so $V$ has a basis. When $V = \{0_V\}$ the basis produced is $\varnothing$ , the only linearly independent subset of that space.

step 1.1step 1.2L3∎

Remarks

The converse is a theorem of Blass, and it is not proved here. The implication proved above runs from the Axiom of Choice, through Zorn's lemma, to the existence of bases. The opposite implication also holds: the statement that every vector space over every field has a basis implies the Axiom of Choice. That is a hard result of Andreas Blass, published in 1984 as "Existence of bases implies the axiom of choice"; this library does not prove it, does not use it, and nothing here rests on it. It is recorded because it fixes the exact strength of the statement above: existence of bases is not merely a consequence of choice, it is equivalent to it over ZF. The reference is listed in the sources of this item.
Where the choice is spent. In Zorn's lemma, once, and nowhere else on this page. Every other existence statement here is explicit: the standard basis of $F^{n}$ (The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$ ; hence $\dim_F F^{n} = n$ , and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$ ) is written down, and so is the infinite basis of the eventually zero families on the companion page. The contrast between those and the present corollary — which produces a basis of $\mathbb{R}$ over $\mathbb{Q}$ while exhibiting none, as the companion page records — is the point of keeping them on the same page.
This says nothing about the size of the basis. For a space with no finite basis, Finite-dimensional vector space, and its dimension $\dim_F V$ ; infinite-dimensional means having no finite basis assigns no dimension at all, and the corollary correspondingly asserts only existence.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 63 results over 20 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

Basis (linear algebra) (Wikipedia) — where A. Blass, Existence of bases implies the axiom of choice, Contemporary Mathematics 31 (1984), 31-33, is recorded (standard reference, not scraped)
Axiom of choice (Wikipedia) (standard reference, not scraped)
Cambridge University Press excerpt: Vector spaces and bases (standard reference, not scraped)