The completion of a metrizable TVS is metrizable Let $E$ be metrizable topological vector spaces with a metric $d$. According to Theorem 5.2. in Trèves book, Topological Vector Spaces, Distributions and Kernels, there exists a complete Hausdorff TVS $\hat{E}$ and a mapping $i$ of $E$ into $\hat{E}$, linear, bicontinuous, one-to-one and $\overline{i(E)}=\hat{E}$ and the space $\hat{E}$ is unique, up to isomorphism.
We also have the following result:
Theorem: Let $F,G$ be two Hausdorff TVS, $A$ a dense subset of $F$, and $f$ a uniformly continuous mapping of $A$ into $G$. If $G$ is complete, there is a unique continuous mapping $\bar{f}$ of $F$ into $G$ which extends $F$. Moreover, $\bar{f}$ is uniformly continuous, and $\bar{f}$ is linear if $A$ is a subspace of $F$ and if $f$ is linear.
It's easy to prove that the completion of the cartesian product is topologically ismorphic to the cartesian product of the completions.
Remark:  I know how to build this metric by repeating the proof of the completion of a metric space, however that is not my question.

My question: Admitting the result that says all Hausdorff TVS admits a completion I want to prove that if in additional it is metrizable, then the completion is metrizable, that is:
i) There exists  a unique metric $\hat{d}$ in the completion $\hat{E}$ of $E$ which extends the metric $d$.
ii)The topology generated by this metric coincides with the original topology of the space $\hat{E}$.

Let $\mathscr{C}_E$ be the collection of all Cauchy filters on the TVS $E$ and define the following relation in $\mathscr{C}_E$:
$\mathscr{F} \sim_R \mathscr{G} \Leftrightarrow$ for all  neighborhood $U$ of the origin in $E$, there exists $A \in \mathscr{F}$, $B \in \mathscr{G}$ such that $A − B ⊂ U$.
The application above mentioned is give by $i:E \rightarrow \hat{E}$ given by $i(x)=\{\mathscr{F} \in \mathscr{C}_E:\mathscr{F}\rightarrow x\}=\{\mathscr{F} \in \mathscr{C}_E: \mathscr{F} \sim_R \mathscr{F}(x)\}$.
A basis for the filter of neighborhoods of the origin in $\hat{E}$ is given by:
$$\mathscr{B}=\{\hat{U}: \hat{U}=\{\hat{x} \in \hat{E}: U \hbox{ belongs to some representative of } \hat{x}  \} \}$$
as $U$ varies over the filter of neighborhoods of $0$ in $E$.
My attempt: I have already proved all the results mentioned above, as I believe they are the main ingredients to prove this result. The next step would be to extend the metric. For that, I thought of using the uniform continuity of the metric in each of the variables, that is, for each $x \in E$, the application $d_x:E \rightarrow [0,\infty)$ is uniformly continuous. By the Theorem above mentioned, there exists a extension $\bar{d_x}:\hat{E} \rightarrow [0,\infty)$ of $d_x$. But I don't know how to proceed in the proof.
 A: Proof of "i) & ii)" when d is an invariant metric.
(That is presented in this answer. In my second answer below, I treat general $d$ but only prove part of your claim. Example A2 shows that not all TVS metrics are uniformly continuous; hence your "Theorem" cannot be applied to general $d$ and hence I assume invariance below.)
A metric is invariant if $d(x+z,y+z)=d(x,y)$ for all $x,y,z$.
[By [RudinFA:1.24] or the Birkhoff--Kakutani theorem, any N1 (equivalently, metrizable) Hausdorff TVS has an invariant metric compatible with the topology etc.]
Now $A:=E\times E$ is dense in $F:=\hat{E}\times \hat{E}$. Set $G:=\mathbb{R}$ (or $\mathbb{C}$ if $E$ is complex). By your "Theorem" (and Lemma A below), $d:A\to G$ has a unique continuous extension $\bar d:F\to G$.
By continuity, its range lies in $[0,\infty)$ and the axioms of a metric are preserved (as $d(x_n,y_n)\to d(x,y)$ when $E\owns x_n\to x$, $E\owns y_x\to y$).
i) Any metric extending $d$ to $F$ is continuous and must hence match $\bar d$, by density, so $\bar d$ is unique.
ii) As $\bar d$ is continuous on $F$, its topology is coarser than that of $F$. The following proves that it is also finer, hence equal:
Let $V$ be a neighborhood of $x\in E$. By [RudinFA:1.11], $V$ contains the closure of a neighborhood $W$ of $x$. Let $\epsilon>0$ be such that $d(x,y)<\epsilon \Rightarrow y\in W$.
Set $U:=\{y\in\hat E\,\colon \bar d(x,y)<\epsilon\}$.
If $\bar d(x,y)<\epsilon$, pick $\{y_n\}\subset E$ such that $y_n\to y$.
Then, for big $n$, $\bar d(x,y_n)<\epsilon$; i.e., $y_n\in U\subset W$;
hence $y\in \bar W\subset V$, QED.
An alternative proof would show that $\hat E$ has a countable local base. By [RudinFA:1.24], it has an invariant metric compatible with its topology. (By continuity, that is unique etc.)
Background:
A map $f:A\to G$ is uniformly continuous, if for every neighborhood $W$ of $0_G$ there exists a neighborhood $V$ of $0_A$ such that
$a_1-a_2\in V$ implies $f(a_1)-f(a_2)\in W$. https://en.wikipedia.org/wiki/Uniform_continuity#Generalization_to_topological_vector_spaces
If $V$ is a neighborhood of $0_E$, then $V\times V$ is a neighborhood of $0_{E\times E}$. https://en.wikipedia.org/wiki/Product_topology
Lemma A: Any invariant metric $d:X\times X\to\mathbb{R}$ is uniformly continuous.
Proof: Given $\epsilon>0$, set $V:=\{x\in X\,\colon d(x,0)<\epsilon/2\}$.
If $x,y,x',y'\in X\times X$ and $(x,y)-(x',y')\in V\times V$,
then $|d(x,y)-d(x',y')|\le |d(x,y)-d(x',y)| + |d(x',y)-d(x',y')|
 \le d(x,x') + d(y,y') = d(x-x',0) + d(y-y',0) < \epsilon$,
by Lemma B and invariance, QED.
Example A2. Let $d(x,y):=|x^3-y^3|$. It is a metric on $\mathbb{R}$, compatible with its topology, but it is not uniformly continuous, because if $\epsilon>0$ and $V$ is a neighborhood of $(0,0)$,
then (pick $a>0$ such that $(0,-a)\in V$) we have $(x,x)-(x,x+a)=(0,-a)\in V\times V$ but $d(x,x+a)=(x+a)^3-x^3 = 3x^2a+3xa^2+a^3>\epsilon=d(x,x)+\epsilon$ for big $x\in\mathbb{R}$.
Lemma B: $|d(x,y)-d(z,y)| \le d(x,z)$ for any $x,y,z\in X$ and any metric space $(X,d)$.
Proof: $d(x,y)\le d(x,z) + d(z,y)$ (triangle inequality);
hence $d(x,y)-d(z,y) \le d(x,z)$.
Analogously, $d(z,y)-d(x,y) \le d(x,z)$, QED.
A: I prove part of your result below ("Theorem T") (although that could be deduced from the invariant result in my other answer above, but the proof below is simple and elementary) and then conjecture that your whole claim does not hold for general $d$ (although Theorem T does). See the other answer for the proof of your whole claim for invariant metrics.
Theorem T. Let $E$ be a Hausdorff TVS under a metric $d$. Then its completion (any complete Hausdorff TVS in which $E$ is dense) is metrizable.
Proof: Theorem BK yields us a countable local base $V_1,V_2,\ldots$ of $E$ (i.e., open sets containing $0$ such that some of them is contained in every neighborhood of $0$). Let $(E',\tau')$ be the completion of $(E,\tau)$.
For each $n$, pick $W_k\in\tau'$ (the topology of $E'$) such that $V_k=W_k\cap E$ (this $W_k$ exists, by definition, as the topology $\tau$ of $E$ is that inherited from $E'$).
To prove $E'$ metrizable, we only need to prove that $\{W_k\}$ is a local basis, i.e., that $0\in W'\in\tau'$ implies $W_n\subset W'$ for some $n$.
Pick $W\in\tau'$ such that $0\in \bar W\subset W'$ [RudinFA:1.11].
Pick $n$ such that $V_n\subset W\subset E$. Then $V_n\cap{\bar W}^c=\emptyset$ ($\dagger$).
Set $G:=W_n\cap {\bar W}^c\in\tau'$.
Now $G\cap E = (W_n\cap E)\cap {\bar W}^c = \emptyset$, by ($\dagger$);
hence $G=\emptyset$ (as $E$ is dense and $G$ is open);
i.e., $W_n\subset\bar W\subset W'$, QED.
Theorem BK. A Hausdorff TVS is metrizable iff it has a countable local base.
Conjecture U. I guess that the following is not true in general and that it is not difficult to construct a counter example (from an example where $\tau$-Cauchy sequences do not coincide with $d$-Cauchy sequences).
"Then $d$ has a unique continuous extension $d':E'\times E'\to[0,\infty)$,
and $d'$ is compatible with the topology of $E'$." FALSE?
But I may well be wrong, so "conjecture" is maybe a too strong word here. Sorry, I don't have time for that now (and I think that most readers need just Theorem T and/or the invariant case).
Here you find more on completions but not the missing part: https://en.wikipedia.org/wiki/Complete_topological_vector_space#Completions
