A normed space is locally compact if and only if it is finite-dimensional

Assume $X$ admits an ordered basis of length $n$. If $\mathbb{K}=\mathbb{R}$, the coordinate space ${\mathbb{R}}^n$ is locally compact by [L4] when $n\ge 1$, and ${\mathbb{R}}^0=\{0\}$ is compact, hence locally compact. If $\mathbb{K}=\mathbb{C}$, then ${\mathbb{C}}^n$ identifies with ${\mathbb{R}}^{2n}$ by [L5], so the same conclusion holds there. By [L1], $X$ is homeomorphic to that coordinate space, hence locally compact.

Assume now that $X$ is locally compact. By [L6], applied to the norm metric, $0$ has a compact neighbourhood $K$ containing some open ball $B(0,r)$ with $r>0$. The closed ball $\bar{B}(0,\frac{r}{2}):=\{x\in X:\mathrm{\parallel }x\mathrm{\parallel }\le \frac{r}{2}\}$ is a closed subset of $K$ and is therefore compact.

For the successor step, let $M_m:=\mathrm{span}\{x_0,\dots ,x_m\}$. The finite list $x_0,\dots ,x_m$ generates $M_m$, so by deleting dependent terms if necessary one gets an ordered basis of finite length for $M_m$. Thus $M_m⊊X$ by the contradiction hypothesis, and A finite-dimensional normed subspace is closed makes $M_m$ closed. Applying [L2] with $\alpha =1\mathrm{/}2$ yields a unit vector $x_{m+1}$ with $\mathrm{dist}(x_{m+1},M_m)>1\mathrm{/}2$. In particular $\mathrm{\parallel }{x}_{m+1}-x_j\mathrm{\parallel }>1\mathrm{/}2$ for every $j\le m$. [L2, A finite-dimensional normed subspace is closed, choose]

Suppose for contradiction that $X$ admits no ordered basis of finite length. We recursively build, for each $m\ge 0$, unit vectors $x_0,\dots ,x_m\in X$ such that $\mathrm{\parallel }{x}_j-x_k\mathrm{\parallel }>\frac{1}{2}(j\mathrm{\ne }k)\mathrm{.}$ For $m=0$ choose any nonzero $x_0$ and normalize it.

Every $x_j$ lies in the closed ball $\bar{B}(0,r\mathrm{/}2)$ after rescaling by $r\mathrm{/}2$: namely $y_j:=(r\mathrm{/}2)x_j$ satisfies $\mathrm{\parallel }{y}_j\mathrm{\parallel }=r\mathrm{/}2$, so $y_j$ lies in that compact set. Also $\mathrm{\parallel }{y}_j-y_k\mathrm{\parallel }=\frac{r}{2}\mathrm{\parallel }{x}_j-x_k\mathrm{\parallel }>\frac{r}{4}(j\mathrm{\ne }k)\mathrm{.}$

By [L3], the compact metric space $\bar{B}(0,r\mathrm{/}2)$ is totally bounded. Taking $\epsilon =r\mathrm{/}8$, it admits a finite $\epsilon$-net. But one $\epsilon$-ball can contain at most one of the points $y_j$, since distinct ones are more than $r\mathrm{/}4=2\epsilon$ apart. Therefore a finite $\epsilon$-net cannot cover arbitrarily large finite sets $\{y_0,\dots ,y_m\}$, contradiction.

The contradiction in step 4.1 shows that $X$ must admit an ordered basis of finite length. Together with step 1.1, this proves the equivalence.