Solution (source code)

= Solution

<Zorn lemma> states that a <partially ordered set> in which every <chain in a partially ordered set> has an upper bound has a <maximal element>. Include the empty <chain in a partially ordered set>, so the hypotheses imply that the <set> $P$ is nonempty. Suppose there were no <maximal element>. Every <chain in a partially ordered set> $C$ has an upper bound $u$, and some $v>u$; therefore the <set> of elements strictly above every member of $C$ is nonempty. The <axiom of choice> selects one such element $f(C)$ for each <chain in a partially ordered set> (and an element of $P$ when $C$ is empty).

By <Hartogs theorem>, there is an <ordinal> $\kappa$ which does not inject into $P$. <Transfinite recursion> defines $x_\alpha=f(\{x_\beta:\beta<\alpha\})$ for all $\alpha<\kappa$: previous elements form a strictly increasing <chain in a partially ordered set>, including at <limit ordinal> stages. All $x_\alpha$ are distinct, giving the forbidden injection. This proves <Zorn lemma>; \b[the choice of $f$ is the use of the <axiom of choice>].

Apply <Zorn lemma> to <linearly independent> <subsets> of $\mathbb R$ over $\mathbb Q$, ordered by inclusion. A <union> along a <chain in a partially ordered set> is <linearly independent> because each finite linear relation occurs in one member of that <chain in a partially ordered set>. A maximal independent <set> spans $\mathbb R$, since a <vector> outside its span could be adjoined. Thus \b[$\mathbb R$ has a Hamel <basis> over $\mathbb Q$].

For a finite <basis>, the <Steinitz exchange lemma> proves equality of <basis> sizes. This also rules out an infinite <basis> when a finite spanning <set> exists: write each member of the finite spanning <set> using finitely many elements of another <basis>; their finite <union> spans, and independence leaves no other <basis> elements. If a <basis> $B$ is infinite with <cardinality> $\lambda$, the finite-support description of every <vector> and countability of $\mathbb Q$ give
$$
 \lambda\leq|V|\leq\sum_{n<\omega}|B|^n|\mathbb Q|^n=\lambda.
$$
Here infinite <cardinal arithmetic> uses the <axiom of choice>. Thus any infinite <basis> has <cardinality> $|V|$, proving \b[all <bases> have the same <cardinality>]. The zero space has its unique empty <basis>.