The closed unit ball is compact if and only if the normed space is finite-dimensional

Assume $X$ admits an ordered basis of length $n$, and let $T:{\mathbb{K}}^n\to X$ be the coordinate isomorphism from [L1]. Then $T^{-1}[{\bar{B}}_X]$ is closed in ${\mathbb{K}}^n$, because $T$ is continuous, and bounded in the coordinate ${\mathrm{\ell }}^1$ norm, because $T^{-1}$ is bounded.

Assume conversely that ${\bar{B}}_X$ is compact. Then [L4] makes it totally bounded. Suppose for contradiction that $X$ admits no ordered basis of finite length.

Let $F\subseteq {\bar{B}}_X$ be a finite $1\mathrm{/}2$-net, and put $M:=\mathrm{span}(F)$. The finite set $F$ generates $M$, so by deleting dependent terms one gets an ordered basis of finite length for $M$; thus [L3] makes $M$ closed. Since $X$ is not finitely generated, $M⊊X$.

In the real case $\mathbb{K}=\mathbb{R}$, if $n=0$ then ${\bar{B}}_X=\{0\}$ is compact. If $n\ge 1$, step 1.1 and [L5] show that $T^{-1}[{\bar{B}}_X]$ is compact in ${\mathbb{R}}^n$, hence ${\bar{B}}_X$ is compact as its homeomorphic image.

In the complex case $\mathbb{K}=\mathbb{C}$, [L6] identifies ${\mathbb{C}}^n$ with ${\mathbb{R}}^{2n}$. Under that identification the coordinate ${\mathrm{\ell }}^1$ norm is equivalent to a real norm on ${\mathbb{R}}^{2n}$, so the bounded closed set $T^{-1}[{\bar{B}}_X]$ is also closed and bounded in Euclidean space. If $n=0$ it is a singleton; if $n\ge 1$, [L5] makes it compact in ${\mathbb{R}}^{2n}$, hence compact in ${\mathbb{C}}^n$ and therefore in $X$.

Applying [L2] with $\alpha =1\mathrm{/}2$ gives a unit vector $x\in X$ with $\mathrm{dist}(x,M)>1\mathrm{/}2$. Since $F$ is a $1\mathrm{/}2$-net in the unit ball and $x\in {\bar{B}}_X$, some $y\in F$ satisfies $\mathrm{\parallel }x-y\mathrm{\parallel }<1\mathrm{/}2$. But $y\in M$, which contradicts $\mathrm{dist}(x,M)>1\mathrm{/}2$.

Therefore $X$ must admit an ordered basis of finite length. Together with steps 2.1 and 2.2, this proves the equivalence.