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 infinite, and defines the dimension of the vector space. Formally, the dimension theorem for vector spaces states that As a basis is a generating set that is linearly independent, the theorem is a consequence of the following theorem, which is also useful: In particular if is finitely generated, then all its bases are finite and 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 theorem can be generalized to arbitrary -modules for rings having invariant basis number. In the finitely generated case the proof uses only elementary arguments of algebra, and does not require the axiom of choice nor its weaker variants.
Proof
Let be a vector space, be a linearly independent set of elements of, and be a generating set. One has to prove that the cardinality of is not larger than that of. If is finite, this results from the Steinitz exchange lemma. If is finite, a proof based on matrix theory is also possible. Assume that is infinite. If is finite, there is nothing to prove. Thus, we may assume that is also infinite. Let us suppose that the cardinality of is larger than that of. We have to prove that this leads to a contradiction. By Zorn's lemma, every linearly independent set is contained in a maximal linearly independent set. This maximality implies that spans and is therefore a basis. As the cardinality of is greater than or equal to the cardinality of, one may replace with, that is, one may suppose, without loss of generality, that is a basis. Thus, every can be written as a finite sum where is a finite subset of As is infinite, has the same cardinality as. Therefore has cardinality smaller than that of. So there is some which does not appear in any. The corresponding can be expressed as a finite linear combination of s, which in turn can be expressed as finite linear combination of s, not involving. Hence is linearly dependent on the other s, which provides the desired contradiction.
