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

If $V$ has a basis with $n$ elements and a basis with $m$ elements then $n = m$ ; and if $V$ has one finite basis then every basis of $V$ is finite

Statement

Let $V$ be a vector space over a field $F$ (Vector space over a field).

If $B$ and $B^{'}$ are bases 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 $B \approx n$ and $B^{'} \approx m$ for $n, m \in N$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ), then $n = m$ .
If $V$ has one finite basis (Finite, countably infinite, countable, uncountable), then every basis of $V$ is finite.

The infinite case is not claimed. Nothing here asserts that any two infinite bases of a space are equinumerous. The Steinitz argument gives invariance only when one of the bases is finite; the infinite case rests on cardinal arithmetic, which is not available at this point in the reading order, cardinal numbers being developed much later in the library. What replaces it here is the honest substitute on the companion page: a proper linear subspace with a basis equinumerous with a basis of the whole space, which compares two specific infinite bases through an explicit bijection and assigns no dimension to either space.

Facts & Assumptions

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

[L1]

A basis of $V$ is a linearly independent subset that spans $V$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, 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, Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ).

[L2]

If $V$ has a spanning subset $S$ with $S \approx p$ , then every linearly independent subset $L$ of $V$ is finite and the unique $q$ with $L \approx q$ satisfies $q \leq p$ (If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $N$ , which is drawn from The Steinitz exchange lemma: if $L \subseteq V$ is linearly independent and $S \subseteq V$ spans $V$ with $S$ finite of size $n$ , then $L$ is finite with $∣ L ∣ = m \leq n$ , and there is $T \subseteq S$ of size $n - m$ such that $L \cup T$ spans $V$ ).

[L3]

A finite set is equinumerous with exactly one natural number (The pigeonhole principle on $N$ , claim 3); $\approx$ is carried by bijections (Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection, Finite, countably infinite, countable, uncountable).

[L4]

$\leq$ on $N$ is a total order, in particular antisymmetric ( $\leq$ is a linear order on $N$ , Order on the natural numbers, The natural numbers $N$ (von Neumann)).

Proof

technique · direct

1.1

Let $B \approx n$ and $B^{'} \approx m$ be bases of $V$ . Then $B$ spans $V$ and is finite of size $n$ , while $B^{'}$ is linearly independent, so $B^{'}$ is finite and the unique $q$ with $B^{'} \approx q$ satisfies $q \leq n$ . Since $B^{'} \approx m$ as well, uniqueness gives $q = m$ , so $m \leq n$ .

L1L2L3

1.2

Exchanging the roles of the two bases, $B^{'}$ spans $V$ and is finite of size $m$ while $B$ is linearly independent, so the unique $q^{'}$ with $B \approx q^{'}$ satisfies $q^{'} \leq m$ ; and $B \approx n$ gives $q^{'} = n$ , so $n \leq m$ .

L1L2L3

1.3

Claim 2. Let $B$ be a finite basis of $V$ , say $B \approx p$ , and let $B^{'}$ be any basis of $V$ . Then $B$ spans $V$ and is finite of size $p$ , while $B^{'}$ is linearly independent, so $B^{'}$ is finite.

L1L2

2.1

Steps 1.1 and 1.2 give $m \leq n$ and $n \leq m$ , so $n = m$ by antisymmetry, which is claim 1; and claim 2 is step 1.3.

step 1.1step 1.2step 1.3L4∎

Remarks

This is the well-definedness obligation for Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis. Without claim 1 the phrase "the dimension of $V$ " would name nothing, since a space with a basis of $n$ elements might also have one of $m \neq n$ elements. Claim 2 is the companion statement that finiteness of some basis is a property of the space and not of the chosen basis.
Both halves come from one corollary, used twice. The only input is that an independent set cannot outnumber a finite spanning set; applying it in each direction gives the two inequalities, and antisymmetry of the order on $N$ closes the argument. Nothing here re-runs the exchange.
What "not available at this point in the reading order" means. The infinite invariance statement is a genuine theorem of set theory and algebra, and it is not being denied. It is simply not derivable from anything the library has established so far, since its standard proof compares cardinals; the page states what it can prove and marks the boundary rather than gesturing past it.

Depends on

Used by

Dependency tree · two levels

50 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

Dimension theorem for vector spaces (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed., Ch. 2 (standard reference, not scraped)
Sheldon Axler, Linear Algebra Done Right, 4th ed. (standard reference, not scraped)

If VV has a basis with nn elements and a basis with mm elements then n=mn=m; and if VV has one finite basis then every basis of VV is finite