LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

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

Statement

Let $V$ be a vector space over a field $F$ (Vector space over a field). Let $I$ be the set of linearly independent subsets of $V$ (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent) and $S$ the set of spanning subsets of $V$ (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ), each partially ordered by inclusion (Partial order and partially ordered set). For $B \subseteq V$ the following are equivalent.

(a) $B$ is a basis of $V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
(b) $B$ is a maximal element of $(I, \subseteq)$ (Maximal element and greatest element): $B$ is linearly independent, and no linearly independent $A \subseteq V$ satisfies $B ⊊ A$ .
(c) $B$ is a minimal element of $(S, \subseteq)$ : $B$ spans $V$ , and no spanning $A \subseteq V$ satisfies $A ⊊ B$ .

Facts & Assumptions

Given: A field $F$ , a vector space $V$ over $F$ , and a subset $B \subseteq V$ .

[L1]

$B$ is a basis of $V$ when $B$ is linearly independent and $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).

[L2]

A subset $T \subseteq V$ is linearly dependent if and only if some $t \in T$ lies in $span (T ∖ {t})$ (A subset $S \subseteq V$ is linearly dependent if and only if some $s \in S$ lies in $span (S ∖ {s})$ ; and $span (S)$ is already the set of linear combinations of INJECTIVE finite lists into $S$ ).

[L3]

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

[L4]

Every subset of a linearly independent subset of $V$ is linearly independent (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, claim 7).

[L5]

$span (T)$ is a linear subspace of $V$ containing $T$ and contained in every linear subspace of $V$ containing $T$ ; and $T \subseteq T^{'}$ implies $span (T) \subseteq span (T^{'})$ (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ , The span is monotone and idempotent, $span (S) = S$ exactly when $S$ is a linear subspace, and $span (S \cup {0_{V}}) = span (S)$ , Linear subspace of a vector space).

[L6]

Inclusion is a partial order, and $m$ is maximal in a poset when no element is strictly above it, minimal when no element is strictly below it (Partial order and partially ordered set, Maximal element and greatest element).

Proof

technique · direct

1.1

(a) implies (b). Let $B$ be a basis, so $B$ is linearly independent and $span (B) = V$ . Suppose some linearly independent $A$ satisfies $B ⊊ A$ , and pick $w \in A ∖ B$ . Then $B \cup {w} \subseteq A$ , so $B \cup {w}$ is linearly independent. On the other hand $w \in V = span (B)$ , and $B = (B \cup {w}) ∖ {w}$ because $w \notin B$ , so $B \cup {w}$ is linearly dependent. These contradict each other, so no such $A$ exists and $B$ is maximal in the inclusion order on the linearly independent subsets.

L1L2L4L6

1.2

(b) implies (a). Let $B$ be maximal among the linearly independent subsets of $V$ . If some $w \in V$ had $w \notin span (B)$ , then $B \cup {w}$ would be linearly independent with $w \notin B$ , so $B ⊊ B \cup {w}$ , contradicting maximality. Hence $V \subseteq span (B)$ , and $span (B) \subseteq V$ always, so $span (B) = V$ and $B$ is a basis.

L1L3L5L6

1.3

(a) implies (c). Let $B$ be a basis, so $B$ spans $V$ . Suppose some spanning $A$ satisfies $A ⊊ B$ , and pick $b \in B ∖ A$ . Then $A \subseteq B ∖ {b}$ , so $V = span (A) \subseteq span (B ∖ {b})$ by monotonicity, and in particular $b \in span (B ∖ {b})$ . That makes $B$ linearly dependent, contradicting the assumption that $B$ is a basis. So $B$ is minimal among the spanning subsets.

L1L2L5L6

1.4

(c) implies (a). Let $B$ be minimal among the spanning subsets of $V$ , so $span (B) = V$ . If $B$ were linearly dependent, there would be $b \in B$ with $b \in span (B ∖ {b})$ ; then $span (B ∖ {b})$ is a linear subspace of $V$ containing $B ∖ {b}$ and also containing $b$ , hence containing $B$ , hence containing $span (B) = V$ by minimality of the span. So $B ∖ {b}$ spans $V$ while $B ∖ {b} ⊊ B$ , contradicting minimality of $B$ . Hence $B$ is linearly independent and is a basis.

L1L2L5L6

2.1

Steps 1.1 and 1.2 give the equivalence of (a) and (b), and steps 1.3 and 1.4 give the equivalence of (a) and (c); so all three conditions are equivalent.

step 1.1step 1.2step 1.3step 1.4∎

Remarks

Maximal and minimal, never greatest and least. There is in general no largest independent subset and no smallest spanning subset: a space usually has many bases, pairwise incomparable under inclusion, and Maximal element and greatest element is explicit that maximality does not imply greatestness. The companion page exhibits a three-element spanning set of $F^{2}$ containing three different bases.
This is the lemma that converts an existence problem into an order problem. Producing a basis becomes producing a maximal element of a poset, which is what Zorn's lemma does (Zorn's lemma); producing one inside a given spanning set becomes the same problem in a smaller poset. Both are carried out in 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 $span (S) = V$ , there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$ , whose poset is the one named in (b) above, cut down to the subsets lying between a given independent set and a given spanning set.
The two orders are the same order on different families. Nothing above compares an independent set with a spanning set; the maximality of (b) is taken inside $I$ and the minimality of (c) inside $S$ , and a basis is exactly a set that is extreme in both families at once.

Depends on

Used by

{(1,0), (0,1), (1,1)} spans F² and is linearly dependent, so a spanning set need not be a basis; each of its three two-element subsets is a basis Counterexample

Dependency tree · two levels

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

Sources

Basis (linear algebra) (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed., Ch. 2 (standard reference, not scraped)
Cambridge University Press excerpt: Vector spaces and bases (standard reference, not scraped)

For B⊆VB⊆V the following are equivalent: BB is a basis; BB is a maximal linearly independent subset of VV; BB is a minimal spanning subset of VV — maximality and minimality being in the inclusion order