Dimension theorem for vector spaces

In mathematics, the dimension theorem for vector spaces states that all bases of a vector space have equally many elements. This number of elements may be finite, or given by an infinite cardinal number, and defines the dimension of the space.

Formally, the dimension theorem for vector spaces states that

If V is finitely generated, then it has a finite basis, and the result says that any two bases have the same number of elements.

While the proof of the existence of a basis for any vector space in the general case requires Zorn's lemma and is in fact equivalent to the axiom of choice, the uniqueness of the cardinality of the basis requires only the ultrafilter lemma, which is strictly weaker (the proof given below, however, assumes trichotomy, i.e., that all cardinal numbers are comparable, a statement which is also equivalent to the axiom of choice). The theorem can be generalized to arbitrary R-modules for rings R having invariant basis number.

The theorem for finitely generated case can be proved with elementary arguments of linear algebra, and requires no forms of the axiom of choice.

Assume that { a_i: i ∈ I } and { b_j: j ∈ J } are both bases, with the cardinality of I bigger than the cardinality of J. From this assumption we will derive a contradiction.

Assume that I is infinite.

Every b_j can be written as a finite sum

Since the cardinality of I is greater than that of J and the E_j's are finite subsets of I, the cardinality of I is also bigger than the cardinality of ${\displaystyle \bigcup _{j\in J}E_{j}}$. (Note that this argument works only for infinite I.) So there is some ${\displaystyle i_{0}\in I}$ which does not appear in any ${\displaystyle E_{j}}$. The corresponding ${\displaystyle a_{i_{0}}}$ can be expressed as a finite linear combination of ${\displaystyle b_{j}}$'s, which in turn can be expressed as finite linear combination of ${\displaystyle a_{i}}$'s, not involving ${\displaystyle a_{i_{0}}}$. Hence ${\displaystyle a_{i_{0}}}$ is linearly dependent on the other ${\displaystyle a_{i}}$'s.

...
Wikipedia