$x\in X$ LCS, $f\in X^\ast$ s.t. $f(x)=1$, $f|_Y=0$ Let $X$ be a locally convex space (topology induced by a family of seminorms $P$ which separates points) and $Y\subset X$ a closed subspace. Assume $x\in X\setminus Y$. Show that there exists a $f\in X^\ast$ such that $f|_Y=0$ and $f(x)=1$.
My attempt: $Z:= X/Y$ is also a LCS (closedness of $Y$ guarantees that $X/Y$ is Hausdorff) and then there exists a $g\in Z^*$ such that $g(x+Y) \neq 0$ (Here I use Hahn-Banach in the sense that the dual is separating points of a LCS). The quotient map $q: X \to X/Y$ is also continuous and therefore, normalizing $f:= g \circ q$ gives the desired functional.
Is this correct and is there a more direct proof? E.g. use Hahn-Banach with semi-norms and define an appropriate functional on $Y\oplus \text{span}(x)$. I tried this but could not achieve that the function $y+\lambda x \mapsto \lambda p(x)$ was dominated by the seminorm $p$.
I am also happy if someone could verify the proof or spot mistakes.
 A: Your proof is correct, and in my opinion, that is the nicest proof of the assertion.
There is, however, one terminological glitch, you wrote "$X/Y$ separates points", but that should be "$X/Y$ is separated", or "$X/Y$ is Hausdorff". (The seminorms that separate points still controlled the muscle memory, I guess.) And maybe it would be better to say "normalize" before saying $f = g\circ q$ "will do the job". But that is pedantry.
We can use the Hahn-Banach theorem(s) of course also in different ways to prove it.
For example, since $x\notin Y$ and $Y$ is closed, there is a convex balanced neighbourhood $U$ of $0$ such that $(x+U)\cap Y = \varnothing$. Since $U$ is balanced, $x \notin Y + U$. The Minkowski functional $p$ of $Y+U$ is then a continuous seminorm on $X$, with $p(x) \geqslant 1$. Then the linear form $\lambda \colon \operatorname{span} \{x\} \to \mathbb{K}$ (where $\mathbb{K} \in \{\mathbb{R},\mathbb{C}\}$, whichever is the base field) given by $\alpha x\mapsto \alpha$ is dominated by $p$, and an extension $f$ of $\lambda$ to $X$ that is dominated by $p$ does the required. Domination by $p$ implies continuity, and since $p\lvert_Y \leqslant 1$ it follows that $p\lvert_Y \equiv 0$ and hence $f\lvert_Y \equiv 0$.
