How can I prove this exercise using Hahn Banach theorem? 
Let $X$ be a normed space, $Y$ a closed subspace of $X$ and $x\in X\setminus Y$. I need to prove that there exists $\bar f\in X^*$ s.t. $\bar f=0$ on $Y$ and $\bar f(x)=\inf \{||x-y||: y\in Y\}=:d(x,Y)$

My idea was the following. Let me define $$p=d(\cdot, Y):X\setminus Y\rightarrow \Bbb{R}; x\mapsto d(x,Y)$$ and $$f:Y\rightarrow \Bbb{R}; y\mapsto 0$$Then clearly $p$ is sublinear and $f$ is linear such that $f\leq q$. Now applying Hahn-Banach theorem we get that there exists $\bar f\in X^*$ such that $\bar f(x)=f(x)=0$ for all $x\in Y$ and $\bar f(x)\leq p(x)=d(x,Y)$ for all $x\in X$.
Now I thought that I would be done if I could show that $\bar f=p(x)$ for all $x\in X\setminus Y$. But I don't see how to do this. Could someone help me?
Edit
Could I finish the proof as follows: Let me assume $\bar f(x)<d(x,Y)$ for all $x\in X$ then pick $x\in Y$ so $$0=\bar f(x)<0$$ which is a contradiction, hence $\bar f(x)=p(x)$?
 A: First of all, as a general comment, you are mixing $x$ as a fixed element in the original statement and after that you use it as a general element of $X$. That will most likely confuse you.
Second, applying Hahn-Banach that way there are two problems:

*

*taking $\bar f=0$ is a perfectly acceptable extension and so you miss the possibility of getting the concrete choice for $\tilde f(x)$.


*you have no guarantee that $\bar f$ will be bounded.
Third, note that your argument does not use that $Y$ is closed, which is essential for the original statement to be true.
Fourth, the definition you are trying is not linear!
Instead, you could consider the space $\tilde Y=\operatorname{span}\{Y,x\}$, and define $f(y+\lambda x)=\lambda$ (this is well-defined because $x\not\in Y$ guarantees that $y,x$ are linearly independent). Let us look at the norm of $f$ (note that the case $\lambda=0$ cannot contribute to the sup):
\begin{align}
\|f\|
&=\sup\Big\{\frac{|f(y+\lambda x)|}{\|y+\lambda x\|}:\ y\in Y,\ \lambda\ne0\Big\}\\[0.3cm]
&=\sup\Big\{\frac{|\lambda |}{\|y+\lambda x\|}:\ y\in Y,\ \lambda\ne0\Big\}\\[0.3cm]
&=\sup\Big\{\frac{1}{\|y/\lambda+  x\|}:\ y\in Y,\ \lambda\ne0\Big\}\\[0.3cm]
&=\sup\Big\{\frac{1}{\|y-  x\|}:\ y\in Y\Big\}\\[0.3cm]
&=\frac{1}{\inf\{\|y-  x\|:\ y\in Y\}}\\[0.3cm]
&=\frac1{\operatorname{dist}(x,Y)}.
\end{align}
Now we know that $f$ is bounded on $\tilde Y$, and then by Hahn-Banach there exists $\bar g\in X^*$ with $\|\bar g\|=\|f\|$ and $\bar g|_{\tilde Y}=f$. This gives
$$
\bar g(y)=0,\qquad y\in Y,\qquad\qquad \bar g(x)=1.
$$
Now you can simply define
$$
\bar f(z)=\operatorname{dist}(x,Y)\,\bar g(z). 
$$
A: Consider the quotient space $X / Y$, which is a normed space with norm $\|[x]\| = d(x, Y)$. By the Hahn Banach theorem, there is $f \in (X / Y)^*$ such that $\|f\| = \|[x]\| = d(x, Y)$. There is an isometric isomorphism $(X / Y)^* \approx Y^{\perp}$ given by $f \mapsto f \circ \pi$, where $\pi : X \to X / Y$ is defined by $\pi x = [x]$. Thus $\overline{f} := f \circ \pi$ is your desired functional.
