TheoremStatement: AI-adaptedProof: 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.

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$

Statement

Assume the Axiom of Choice (The Axiom of Choice), which is what Zorn's lemma is proved from. Let $V$ be a vector space over a field $F$ (Vector space over a field) and let $L \subseteq S \subseteq V$ with $L$ 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) and $\operatorname{span}(S) = V$ (Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ). Then there is a basis $B$ of $V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) with

$L \;\subseteq\; B \;\subseteq\; S .$

Facts & Assumptions

Given: The Axiom of Choice; a field $F$ ; a vector space $V$ over $F$ ; and subsets $L \subseteq S \subseteq V$ with $L$ linearly independent and $\operatorname{span}(S) = V$ .

[L1]

Zorn's lemma: a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma, Maximal element and greatest element, Upper bound, least upper bound, and strict upper bound, Chain in a poset). The hypothesis quantifies over every chain, the empty one included, and the empty set is a chain (Chain in a poset).

[L2]

Inclusion is a partial order on any collection of sets, and every element of a poset is an upper bound of the empty subset, vacuously (Partial order and partially ordered set, Upper bound, least upper bound, and strict upper bound).

[L3]

The union of a nonempty chain of linearly independent subsets of $V$ , ordered by inclusion, is linearly independent ( $S \subseteq V$ is linearly independent if and only if every finite subset of $S$ is; consequently the union of a nonempty chain of linearly independent subsets of $V$ , ordered by inclusion, is linearly independent, claim 2).

[L4]

If $A \subseteq V$ is linearly independent and $w \notin \operatorname{span}(A)$ , then $w \notin A$ and $A \cup \{w\}$ is linearly independent (If $S \subseteq V$ is linearly independent and $w \notin \operatorname{span}(S)$ then $S \cup \{w\}$ is linearly independent and $\operatorname{span}(S) \subsetneq \operatorname{span}(S \cup \{w\})$ ; and if $w \in \operatorname{span}(S)$ then $\operatorname{span}(S \cup \{w\}) = \operatorname{span}(S)$ , claim 2).

[L5]

$\operatorname{span}(T)$ is a linear subspace of $V$ containing $T$ and contained in every linear subspace of $V$ containing $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)$ , Linear subspace of a vector space).

[L6]

A basis of $V$ is a linearly independent subset $B$ with $\operatorname{span}(B) = V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

Proof

technique · constructive

1.1

Let $P$ be the set of all $A$ with $L \subseteq A \subseteq S$ and $A$ linearly independent. It is a set, being a subcollection of the power set of $S$ , and inclusion partially orders it.

constructL2

1.2

$P$ is nonempty, since $L$ itself is linearly independent and satisfies $L \subseteq L \subseteq S$ .

1.3

Every chain $\mathcal{C} \subseteq P$ has an upper bound in $P$ . If $\mathcal{C} = \varnothing$ , then $L \in P$ is an upper bound, vacuously; this case is not optional, since Zorn's lemma as proved here quantifies over every chain and the empty set is a chain, and the union of the empty chain is $\varnothing$ , which need not contain $L$ . If $\mathcal{C} \ne \varnothing$ , put $A^{*} := \bigcup\mathcal{C}$ : it is linearly independent, being the union of a nonempty chain of linearly independent sets; it contains $L$ , since $\mathcal{C}$ has a member and every member contains $L$ ; and it is contained in $S$ , since every member is. So $A^{*} \in P$ , and it contains every member of $\mathcal{C}$ .

L1L2L3

2.1

By Zorn's lemma applied to the nonempty poset of step 1.1, in which every chain has an upper bound by step 1.3, there is a maximal element $B$ of $P$ : $B$ is linearly independent, $L \subseteq B \subseteq S$ , and no member of $P$ strictly contains $B$ .

step 1.1step 1.2step 1.3L1

3.1

$\operatorname{span}(B) = V$ . Let $s \in S$ and suppose $s \notin \operatorname{span}(B)$ ; then $B \cup \{s\}$ is linearly independent and $s \notin B$ , so $B \subsetneq B \cup \{s\}$ , while $L \subseteq B \cup \{s\} \subseteq S$ , putting $B \cup \{s\}$ in $P$ strictly above $B$ and contradicting maximality. Hence $S \subseteq \operatorname{span}(B)$ , so $\operatorname{span}(B)$ is a linear subspace of $V$ containing $S$ and therefore contains $\operatorname{span}(S) = V$ ; the reverse inclusion is automatic, so $\operatorname{span}(B) = V$ .

step 2.1L4L5

4.1

The set $B$ produced in step 2.1 is linearly independent and, by step 3.1, spans $V$ , so it is a basis of $V$ with $L \subseteq B \subseteq S$ .

step 2.1step 3.1L6discharge-construct∎

Remarks

Both classical statements are instances of this one. "Every vector space has a basis" is the case $L = \varnothing$ , $S = V$ (Every vector space has a basis), and "every spanning set contains a basis" is the case $L = \varnothing$ (Every spanning subset of a vector space contains a basis). They are corollaries of this single Zorn argument rather than two separate ones, which is why the two hypotheses are stated together in the statement above.
The choice is declared, not hidden. The only non-constructive ingredient is Zorn's lemma, and that item records that the Axiom of Choice is used exactly once inside it. Nothing else above appeals to a choice principle: the poset, its order and the upper bound of a chain are all written down explicitly. Zorn's lemma is equivalent to the Axiom of Choice over ZF (The Axiom of Choice and Zorn's lemma are equivalent), so the cost of this theorem is exactly that axiom.
The empty chain is a real case here. Zorn's lemma as proved in this library has no nonemptiness clause on chains, and its own remarks note that requiring every chain to have an upper bound already forces the poset to be nonempty. In the poset above the union of the empty chain is $\varnothing$ , which lies in $P$ only when $L = \varnothing$ ; the upper bound supplied instead is $L$ . Skipping this case would leave a hole in the verification of Zorn's hypothesis.
Maximality is used exactly once, in step 3.1, and only to exclude one extra vector at a time. That is why If $S \subseteq V$ is linearly independent and $w \notin \operatorname{span}(S)$ then $S \cup \{w\}$ is linearly independent and $\operatorname{span}(S) \subsetneq \operatorname{span}(S \cup \{w\})$ ; and if $w \in \operatorname{span}(S)$ then $\operatorname{span}(S \cup \{w\}) = \operatorname{span}(S)$ is stated separately: it is the whole content of the step, and the same lemma does the same job in For $B \subseteq V$ the following are equivalent: $B$ is a basis; $B$ is a maximal linearly independent subset of $V$ ; $B$ is a minimal spanning subset of $V$ — maximality and minimality being in the inclusion order and in 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$ .

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 69 results over 19 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) (standard reference, not scraped)
Zorn's lemma (Wikipedia) (standard reference, not scraped)
University of Colorado notes: Linear algebra and vector spaces (standard reference, not scraped)

Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if L⊆S⊆VL \subseteq S \subseteq VL⊆S⊆V with LLL independent and span⁡(S)=V\operatorname{span}(S) = Vspan(S)=V, there is a basis BBB of VVV with L⊆B⊆SL \subseteq B \subseteq SL⊆B⊆S