If $x$ and $y$ are linearly independent, there is a separating linear functional Let $E$ be a $\mathbb R$-vector space and $x,y\in E$ be linearly independent. How can we show that there is a $\varphi\in E^\ast$ with $\varphi(x)=0$ and $\varphi(y)=1$?

I guess we need to construct $\varphi$ in terms of the coordinate functionals $(\varphi_e)_{e\in B}$ related to a basis $B$ of $E$.

EDIT 1: If it's easier to prove, I'd specifically interested in the cases where $E$ is a Hilbert space or finite-dimensional (or both).

EDIT 2: Maybe I'm missing something, but shouldn't the claim trivially follow in the following way: Let $x_1:=x$ and $x_2:=y$. Since $x_1$ and $x_2$ are linearly independent, $U:=\mathbb Rx_1+\mathbb Rx_2$ is a $\mathbb R$-vector space of dimension $2$ and, by construction, $(x_1,x_2)$ is a basis of $U$. So, there are $\varphi_1,\varphi_2\in U^\ast$ with $\varphi_i(x_j)=\delta_{ij}$ for all $i,j\in\{1,2\}$. So, all we need to do is showing that $\varphi_2$ has a (not necessarily unique) linear extension to $E$.
If you assume that every vector space has a basis, you can also prove the corollary that every linearly independent set can be extended to a basis.

Indeed, if $\mathscr{A}$ is linearly independent and $U$ is the span of $\mathscr{A}$, the vector space $E/U$ has a basis $\mathscr{C}=\{x+U:x\in\mathscr{B}\}$ for some set $\mathscr{B}$. Then it's easy to prove that $\mathscr{A}\cup\mathscr{B}$ is a basis of $E$.

In your case take $\mathscr{A}=\{x,y\}$; once you get $\mathscr{B}$ as above, define $\varphi\colon E\to \mathbb{R}$ by
$$
\varphi(x)=0,\quad \varphi(y)=1,\quad \varphi(z)=0\ (z\in\mathscr{B})
$$
This is nothing else than the functional corresponding to $y$ in the dual basis of $\{x,y\}\cup\mathscr{B}$.

So you see that the trick is to choose a suitable basis.

In the case of a Hilbert space, you want $\varphi$ to be continuous. In this case you can use the fact that the span of $\{x,y\}$ is closed and you can take the orthogonal complement $K$ thereof. Then you can consider $\operatorname{span}(\{x\})\oplus K$ and apply Hahn-Banach.



Addition 1

How do you prove that every linearly independent set can be extended to a basis? One needs Zorn's lemma, as existence of bases for all vector spaces is equivalent to the axiom of choice (and to Zorn's lemma).

Let's fix a vector space $E$.

Let $\mathscr{A}$ be a linearly independent set in $E$. Consider the set $\mathfrak{I}$ consisting of all linearly independent sets $\mathscr{B}$ in $E$ such that $\mathscr{B}\supseteq\mathscr{A}$, ordered by set inclusion. The union of a chain of members of $\mathfrak{I}$ is again linearly independent, because linear independence is checked on finite subsets.

By Zorn's lemma, the set $\mathfrak{I}$ has a maximal element $\mathscr{C}$. I claim that $\mathscr{C}$ spans $E$. Otherwise there would exist $v\in E$ not in the span of $\mathscr{C}$; but then $\mathscr{C}\cup\{v\}$ would be linearly independent, contradicting maximality of $\mathscr{C}$.

Addition 2

Suppose you have as an axiom that every vector space has a basis. How can we prove the theorem above? The easiest way is to consider the subspace $U$ spanned by $\mathscr{A}$. The map
$$
\pi\colon E\to E/U,\qquad \pi(v)=v+U
$$
is linear. If $\mathscr{C}$ is a basis of $E/U$, whose existence is guaranteed by the axiom, then you can write $\mathscr{C}=\{x+U:x\in\mathscr{B}\}$ (choose a representative for every element of $\mathscr{C}$). The set $\mathscr{A}\cup\mathscr{B}$ is then a basis of $E$.

Indeed, suppose we have
$$
\alpha_1v_1+\dots+\alpha_mv_m+\beta_1x_1+\dots+\beta_nx_n=0
$$
with $v_i\in\mathscr{A}$ and $x_i\in\mathscr{B}$. Then applying $\pi$ we obtain
$$
\beta_1(x_1+U)+\dots+\beta_n(x_n+U)=0+U
$$
By linear independence of $\mathscr{C}$, we get $\beta_1=\dots=\beta_n=0$. Now, since $\mathscr{A}$ is linearly independent, also $\alpha_1=\dots=\alpha_m=0$.

Let's prove that $\mathscr{A}\cup\mathscr{B}$ is a spanning set. If $v\in E$, then $\pi(v)=v+U=\beta_1(x_1+U)+\dots+\beta_n(x_n+U)$, with $x_1,\dots,x_n\in\mathscr{B}$, because $\mathscr{C}$ is a spanning set of $E/U$. This implies that
$$
v-\beta_1x_1+\dots+\beta_nx_n\in U
$$
so we can write $v-\beta_1x_1+\dots+\beta_nx_n=\alpha_1v_1+\dots+\alpha_mv_m$, with $v_i\in\mathscr{A}$ and we're done.
If $E$ is infinite dimensional, it may not be "such an elementary linear algebra result".

In finite dimension $\geq 2$, take any $x_0$ in the hyperplane orthogonal to $\mathbb{R}x$ which is not also orthogonal to $\mathbb Ry$, then define $\varphi(y_0) = \frac{ \langle x_0, y_0\rangle}{\langle x_0, y \rangle}$.