Problem on Hahn-Banach and separation theorem

A problem on Hahn-Banach theorem and convex separation theorem:

Let $X$ be a real normed linear space. $E$ a convex subset of $X$ with nonempty interior, $F$ a linear subspace, with $(\operatorname{Int} E)\cap F=\emptyset$. Then there exists a bounded linear functional $f\in X^*, f\not\equiv0$, such that $f(E)\leq0,f(F)=0$.

I think the following corollary of Hahn-Banach theorem may be somewhat useful, but I can't figure out how to combine it with the convex separation theorem.

Let $A$ be a linear subspace of normed linear space $X$, $x_0\in X$, $d(x_0,A)>0$, then there exists $f\in X^*$ s.t. $f(A)=0,f(x_0)=d(x_0,A)$ and $||f||=1$.

Thanks for any help or suggestions.

The statement you want to prove is the classic first version of the Hahn-Banach Separation Theorem .

Usually one has available the Hahn-Banach Theorem, in the form

If $M\subset X$ is a subspace, $\varphi:M\to\mathbb R$ is linear, and $\mu$ is a real seminorm on $X$ (subadditive, $\mu(\lambda x)=\lambda\,\mu(x)$ for $\lambda\geq0$) with $|\varphi(x)|\leq\mu(x)$ for all $x\in M$, then there exists $\tilde\varphi:X\to\mathbb R$, linear, with $\tilde\varphi|_M=\varphi$ and $|\tilde\varphi(x)|\leq\mu(x)$ for all $x$.

Since the interior of a convex set is convex, we may assume that $E$ is open (as the inequality will hold for any limit point). Fix $e'\in E$, $f'\in F$; The condition $E\cap F=\varnothing$ guarantees $e'\ne f'$. Then the set $Z=E-F+f'-e'$ is convex, open and $0\in E-F+f'-e'$. If $\mu$ is its Minkowski Functional, the conditions on $Z$ (open convex neighbourhood of $0$) guarantee that $$\tag1 Z=\{x\in X:\ \mu(x)<1\}. $$

On the subspace $M=\mathbb R(f'-e')$, define $\varphi:M\to\mathbb R$ by $\varphi(\lambda(f'-e'))=\lambda$. Then $\varphi$ is linear. As $f'-e'\not\in Z$, we have $\mu(f'-e')\geq1$. So $$ |\varphi(\lambda(f'-e'))|=|\lambda|\leq|\lambda|\,\mu(f'-e')=\mu(\lambda(f'-e')). $$ That is, $|\varphi(x)|\leq\mu(x)$ for all $x\in M$. By the Hahn-Banach Theorem, there exists $\tilde\varphi:X\to\mathbb R$, linear, with $|\tilde\varphi(x)|\leq\mu(x)$ for all $x\in X$.

Now, for any $e\in E$, $f\in F$, $$ \tilde\varphi(e)-\tilde\varphi(f)+1=\tilde\varphi(e-f+f'-e)<1 $$ by $(1)$. Thus $$\tag2 \tilde\varphi(e)<\tilde\varphi(f),\qquad e\in E,\ f\in F. $$ Let $c=\sup\{\tilde\varphi(e):\ e\in E\}$. Then $c\leq\tilde\varphi(f)$ for all $f\in F$. Using that $F$ is a subspace, we get $c\leq t\tilde\varphi(f)$ for all $t\in\mathbb R$. This forces $\tilde\varphi(f)=0$ for all $f\in F$. Thus $$\tag3 \tilde\varphi(f)=0,\ \tilde\varphi(e)\leq0,\qquad f\in F,\ e\in E. $$ Finally, limit points of $E$ are also limit points of $Z$, and so they satisfy $\mu(x)\leq1$ as the Minkowski Functional is continuous. So the argument above still works, just with $\leq$ instead of $<$.