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.
Best Answer
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.