How to prove a norm identity for a Banach space and its dual Is the following claim true? It feels like it should be true, but I don't really know how to show it.

Let $X$ be a Banach space, and $x \in X$ an element of it. Then there exists a functional $\phi \in X^*$ such that $\| \phi \| = 1$ and $\| x \| = | \phi(x) |$.

If I'm not mistaken, it would suffice to say that there exists a sequence $(\phi_k)_{k = 1}^\infty$ of unit functionals for which $| \phi_k (x) | \to \| x \|$, since the unit ball in $X^*$ is compact in the weak topology. However, I don't know how to prove the former result.
EDIT: I forgot to actually define $\psi$ as $\psi(\lambda x) = \lambda$.
My intuition is that I should be able to invoke Hahn-Banach and define a linear function $\psi$ on $\mathbb{C} x \subseteq X$ bounded by the norm $\rho(x) = \| x \|$ on $X$, then extend it from $\mathbb{C} x$ to all of $X$. Is this a correct application of Hahn-Banach?
 A: You don't need completeness of $X$. This is true in normed spaces. Your last idea is a good one:
We may assume $x \neq 0$.
Define the functional
$$\varphi: \Bbb{C}x \to \Bbb{C}: \lambda x \mapsto \lambda \Vert x \Vert$$
Then it is easily checked that $\Vert \varphi \Vert =1$ (the inequality $\leq$ is obvious, and then note that $\varphi(x/\Vert x \Vert) = 1$ so also $\Vert \varphi\Vert \geq 1$). By Hahn-Banach, we can extend to a functional $\tilde{\varphi}: X \to \Bbb{C}$ with $\Vert \tilde{\varphi} \Vert =1$ and this is the functional you are looking for.
A: Yes, this is a perfect application. You can start by defining a functional on the one-dimensional space spanned by $x$ as $\phi(ax)=a\|x\|$ which has norm $=1$ and extend using HB.
A: W.l.o.g say $x \neq 0$. As you said then look at the subspace $\mathbb{C}x$ and the map $\phi(\lambda x) = \lambda \| x \|$ defined on $\mathbb{C}x$. Then $\phi$ is of course well-defined, linear, bounded and it holds
\begin{align}
\phi(x) = \| x \| \, \text{ and } \, \| \phi \| = \sup_{\| \lambda x \| \leq 1, \, \lambda \in \mathbb{C}} |\lambda | \| x \| = 1.
\end{align}
Using Hahn-Banach you can then extend $\phi$ to and element $\Phi\in X^*$ with $\| \Phi \| = 1$.
