A Conceptual Proof of Riesz's Lemma

Wikipedia's article on Riesz's lemma links to lecture notes by Paul Garret for a proof. Garrett presents the lemma as an independent substitute for orthogonality in Banach spaces. Unfortunately, this approach makes the proof technical and (I think) unmotivated.

There's a very clear proof that reduces the problem to the other substitute for orthogonality in Banach spaces: Hahn-Banach. The downsides are twofold. First, Hahn-Banach uses the axiom of choice (well, the Boolean Prime Ideal Theorem) in an essential way. If you're doing choiceless functional analysis (but who does that?), then Garrett's proof is your only option. Second, the clear proof doesn't seem to be easily available on the web. I can't do much about the first problem, but I can fix the second!

To show:

For $X$ a normed vector space, $Y$ a closed proper subspace and $\epsilon\in[0,1]$, there exists $x\in X$ of unit norm such that, for all $y\in Y$, $$|x-y|\geq1-\epsilon$$

Proof:

Fix any point $z\notin Y$, so that $d(z,Y)\geq 0$. Note that $d(\cdot,Y)$ is

(This is not enough to prove the theorem, since we have no control over $|z|$.)

By Hahn-Banach, the linear portion of $d(\cdot,Y)$ extends to a linear functional on all of $X$ that is also dominated by $d(\cdot,Y)$. Thus $Y$ is contained in the kernel of some nonzero functional $f$.

Without loss of generality, we may rescale $f$ to have unit norm, and and take some "approximate normer" $x\in X$ such that $|f(x)|\geq1-\epsilon$. But now, for any $y\in Y$, $$(1-\epsilon)-0=|f(x)-f(y)|\leq|f||x-y|=|x-y|$$

QED.