Let X be a Banach Space, and $\phi_x:X^*\rightarrow \mathbb{C}$ be the operator defined by $\phi_x(f)=f(x)$, where $f$ is a linear bounded form in $X$.
I am trying to prove that the operator $\psi:X\rightarrow X^{**}$ defined by $\psi(x)=\phi_x$ is injective:
$$ \psi(x)=\psi(y) \Rightarrow \phi_x=\phi_y \Rightarrow \forall f \in X^*\;\; \phi_x(f)=\phi_y(f) \Rightarrow \forall f \in X^*\;\; f(x)=f(y) $$
How can I conclude with $x=y$? ($f$ is linear but a priori not injective)
If $x\neq y$, let $Y\subset X$ be the span of $x-y$ and let $f_0:Y\to \mathbb{C}$ be the linear functional sending $x-y$ to $\|x-y\|$. By Hahn-Banach, $f_0$ extends to an $f\in X^*$ of norm $1$. By construction, $f(x-y)=f_0(x-y)\neq 0$, so $f(x)\neq f(y)$.