Complex Subspace Realification

The sets and additions underlying $W_{\mathbb{R}}$ and $V_{\mathbb{R}}$ are the original sets and additions by [F2]. By [F10], $W$ contains zero and is closed under addition and every complex scalar; therefore it is closed under the restricted real scalar action as well, so $W_{\mathbb{R}}$ is a real linear subspace of $V_{\mathbb{R}}$.

If ${\sum }_{j<n}(a_j{b}_j+c_j(i{b}_j))=0$ with $a_j,c_j\in \mathbb{R}$, distributivity and scalar associativity [F16] give ${\sum }_{j<n}(a_j+i{c}_j)b_j=0$. The supplied complex basis list is injective by [F6] and has independent image by [F5], so [F17] makes it linearly independent; [F15] then forces each $a_j+i{c}_j=0$. Uniqueness of the coordinates in [F7] gives $a_j=c_j=0$. Thus the displayed real list is linearly independent.

By [F1], $N_W=N{\mathrm{\mid }}_W$. For $w\in W$, $N_W(w)=0$ exactly when $N(w)=0$, hence exactly when $w=0$ by [F9]. For $u,w\in W$, closure under addition from [F10] and the ambient triangle inequality give $N_W(u+w)\le N_W(u)+N_W(w)$. For every $\lambda \in \mathbb{C}$, $\lambda w\in W$ by [F10], and [F9] gives $N_W(\lambda w)=\mathrm{\mid }\lambda {\mathrm{\mid }}_{\mathbb{C}}{N}_W(w)$. Thus $(W,N_W)$ is a complex normed space, so [F3] applies to both $V$ and $W$; with [F4], this makes $W_{\mathbb{R}}$ a real normed subspace of $V_{\mathbb{R}}$.

Assume the supplied ordered complex basis exists. Its image spans $W$ by [F6] and [F12], so [F14] gives, for any $w\in W$, complex coefficients $z_j$ with $w={\sum }_{j<n}{z}_j{b}_j$, a finite linear combination in the sense of [F13]. Write each $z_j=a_j+i{c}_j$ using [F7]. Distributivity and scalar associativity [F16] give $w={\sum }_{j<n}(a_j{b}_j+c_j(i{b}_j))$, a real linear combination of the displayed list; conversely every such real combination lies in $W$ because $W$ is complex-linear. Hence the list spans $W_{\mathbb{R}}$.

For $w,w^{\mathrm{\prime }}\in W$, subtraction is unchanged by realification [F2, F16] and the norms are unchanged by [F3], so $d_{W_{\mathbb{R}}}(w,w^{\mathrm{\prime }})=N_W(w-w^{\mathrm{\prime }})=N_V(w-w^{\mathrm{\prime }})=d_{V_{\mathbb{R}}}(w,w^{\mathrm{\prime }})$. By [F11], this is exactly the restriction of the ambient metric to $W\times W$.

If $n=0$, [F6] makes the supplied empty list an ordered basis and [F8] gives $W=\{0\}$; the empty real list is a basis of the same realification by [F2] and [F8]. If $n>0$, steps 2.2 and 1.2 show the displayed list spans and is linearly independent. By [F17] it is injective with independent image, and step 2.2 gives that image's span as $W_{\mathbb{R}}$; [F5] and [F12] make the image a basis, so [F6] makes the list an ordered real basis.