If $M=M^{\perp\perp}$ for every closed subspace $M$ of a pre-Hilbert space then $H$ is complete

We will show that the embedding $i:H\hookrightarrow \hat H$ of $H$ into its completion is onto. Given $z\in \hat H\setminus \{0\}$, the subspace $M=\{x\in H:\langle i(x),z\rangle =0\}$ is closed in $H$ and its orthogonal complement $M^\perp$ is different from $\{0\}$ since otherwise $M=M^{\perp\perp}=\{0\}^\perp=H$ which implies $z=0$. For fixed $y\in M^\perp\setminus \{0\}$ and the linear functionals $\varphi(x)= \langle x,y\rangle$ and $\psi(x)=\langle i(x),z\rangle$ we have kern$(\psi)=M\subseteq$ kern$(\varphi)$ which implies $\varphi=a\psi$ for some scalar $a$ (indeed, if $e\in H$ satisfies $\psi(e)=1$ we get $x-\psi(x)e\in$ kern$(\psi)$ so that $0=\varphi(x-\psi(x)e)=\varphi(x)-a\psi(x)$ for all $x\in H$ with $a=\varphi(e)$). Now, the functionals on $\hat H$ given by $\langle\cdot,i(y)\rangle$ and $\langle\cdot, az\rangle$ coincide on the dense subspace $i(H)$ and hence on $\hat H$ which implies $i(y)=az$. Since $a\neq 0$ this gives $z\in i(H)$.

I hope there aren't any gaps, I tried to write my previous proof in a less convoluted way. Feel free to ask for any clarifications as I was really a novice when I wrote this and right now I am not being able to feel that there are any gaps in my intuition about this proof, but it might have gone terribly wrong.

The proof:

Let $X$ be a pre Hilbert Space in which for every closed subspace $M$ we have $M = M^{\perp \perp}$.

We want to prove that $X$ is Hilbert. We will do it by embedding $X$ in it's completion $\overline{X}$ and proving that they are equal.

Let's call $\overset{\sim}{X}$ the space of continuous linear functionals of $X$ and $\overset{\sim}{\overline{X}}$ the one of continuous linear functionals over $\overline{X}$

Let's observe that given $f \in \overset{\sim}{\overline{X}}$, $f_{|X} \in \overset{\sim}{X}$. Also, given $f \in \overset{\sim}{X}$ there exists a unique extension $\overline{f} : \overline{X} \to \overset{\sim}{\overline{X}}$. So we have a canonical correspondence between $\overset{\sim}{X}$ and $\overset{\sim}{\overline{X}}$, we will treat both spaces as if they were the same.

Let define the following conjugate linear operators $$ T: \overline{X} \rightarrow \overset{\sim}{ \overline{X} } \qquad T (x)(y) = (x,y) $$ If $T(x_{1})=T(x_{2})$ then $(x_{1}-x_{2},y)=0$ for all $y \in \overline{X}$ which implies $\| x_{1}-x_{2} \|^{2} = (x_{1}-x_{2},x_{1}-x_{2})=0$ so $x_{1}=x_{2}$, so $T$ is injective.

Let's assume that $x_{0} \in \overline{X} - X$ and arrive a contradiction, so we will know that $X = \overline{X}$.

Let's call $N_{f} = f^{-1} (0) \cap X$. This is clearly a closed subspace of $X$, so by hyphotesis $N_{f} = N_{f}^{\perp \perp}$. If $N_{f} = \{ 0 \}^{\perp} $, then

$$ N_{f} = N_{f}^{\perp \perp} = (N_{f}^{\perp} )^{\perp} = \{ 0 \}^{\perp} = X $$ Which would imply $f=0$, and as $T$ is injective, $T(x_{0}) = f = 0$ would imply $x_{0} =0$. But $x_{0} \in \overline{X} - X$, and as $0 \in X$ it cannot be $x_{0} = 0$.

Let's see that $N_{f}^{\perp} = \{ 0 \}$ and arrive the desired contradiction. Take an arbitrary $x \in N_{f}^{\perp}$, let's see that $x = 0$.

As $x \in N_{f}^{\perp}$, $(x,y) =0$ holds for every $y \in N_{f}$. So $T(x)(y) = 0$ for all $y \in N_{f}$, then $N_{f} \subset Ker ( T(x) )$. This implies that either $T(x)=0$ or $T(x) = \lambda f = \lambda T(x_{0})$ with $\lambda \neq 0$ as the span of a linear functional is characterized by the kernel of it's generator, and this kernel is either the entire space or has codimension $1$. If $T(x) = 0$ then $x=0$, as $T$ is injective, and we are done.

On the other case $T(x) = T( \lambda x_{0} )$ so $x = \lambda x_{0}$. As $\lambda \neq 0$ and $x_{0} \neq 0$, we have $x \neq 0$. So as $x \in N_{f} \subset X$, we have $ X \cap span (x_{0}) \neq \{ 0 \}$. So there is a $\mu \neq 0$ such that $\mu x_{0} \in X$. But as $X$ is a vector space $x_{0} = \mu^{-1} \mu x_{0} \in X$, which contradicts the fact that $x_{0} \not\in X$.

One way or another, we have reached a contradiction.