Complex Norms and Realification

The canonical image of $r$ is the class of the constant polynomial $r$ by [F1]. Since $i$ is the class of $x$ by [F2], this is also the class of $r+0x$, namely $r+0i$. Uniqueness of complex coordinates in [F3] identifies that image with $r+0i$.

If $r=0$ then $r^2=0$, and if $r\mathrm{\ne }0$ then [F6] gives $r^2>0$. Thus $r^2\ge 0$ in either case, so [F7] guarantees that its nonnegative square root exists.

By [F5], $\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}\ge 0$. If $r\ge 0$, then $\mathrm{\mid }r\mathrm{\mid }=r$; if $r<0$, then $\mathrm{\mid }r\mathrm{\mid }=-r$. In either case $\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}^2=r^2$, including $r=0$.

By [F4] and step 1.1, the modulus of the canonical image of $r$ is $\sqrt{r^2+0^2}=\sqrt{r^2}$, whose radicand is nonnegative by step 1.2.

Step 2.1 and step 1.3 identify the complex modulus of the canonical image of $r$ and $\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}$ as nonnegative square roots of the same $r^2$. By uniqueness in [F7], they are equal.

Since realification preserves the set, zero vector, and addition, the separation and triangle conditions in [F1] hold unchanged on $V_{\mathbb{R}}$. The codomain remains $\mathbb{R}$.

For $r\in \mathbb{R}$ and $v\in V$, [F2] gives $r{\cdot }_{V_{\mathbb{R}}}v={\lambda }_{r}v$. Hence [F1] and [F3] give $N(r{\cdot }_{V_{\mathbb{R}}}v)=N({\lambda }_{r}v)=\mathrm{\mid }{\lambda }_r{\mathrm{\mid }}_{\mathbb{C}}N(v)=\mathrm{\mid }r{\mathrm{\mid }}_{\mathbb{R}}N(v)$. Together with step 1.1, this is exactly the real norm criterion [F4].

The set and addition are unchanged by [F2], so additive inverses and differences are unchanged as well. The realified norm's induced metric is therefore $N(u-v)$ by [F5], the same function $d_N$ defined in the statement, with the same values on the same pairs.

If $n=0$, [F3], [F5] and [F6] say that the only vector is zero and its empty sum is $0$. If $n>0$ and $z=0$, pointwise equality in [F2] makes each coordinate zero; [F4] makes each summand zero, and the finite sum in [F5] is then zero. Conversely, if $N_1(z)=0$, the nonnegative summands from [F4] satisfy the zero-sum condition in [F8], so every $\mathrm{\mid }{z}_j{\mathrm{\mid }}_{\mathbb{C}}=0$ and hence every $z_j=0$ by [F4]. Pointwise equality [F1] identifies $z$ with the zero function [F2]. Thus $N_1(z)=0$ iff $z=0$ for every $n$, as required in [F9].

For every $\lambda \in \mathbb{C}$, the finite-list sum in [F5], pointwise scalar multiplication from [F2], and multiplicativity from [F4] give $N_1(\lambda z)={\sum }_{j<n}\mathrm{\mid }\lambda z_j{\mathrm{\mid }}_{\mathbb{C}}={\sum }_{j<n}\mathrm{\mid }\lambda {\mathrm{\mid }}_{\mathbb{C}}\mathrm{\mid }{z}_j{\mathrm{\mid }}_{\mathbb{C}}=\mathrm{\mid }\lambda {\mathrm{\mid }}_{\mathbb{C}}{N}_1(z)$, where the last equality is finite-sum scaling by the real scalar $\mathrm{\mid }\lambda {\mathrm{\mid }}_{\mathbb{C}}$ from [F7]. This is the complex absolute homogeneity clause in [F9].

Pointwise addition from [F2], the finite-list sum from [F5], and complex modulus subadditivity from [F4] give $\mathrm{\mid }{z}_j+w_j{\mathrm{\mid }}_{\mathbb{C}}\le \mathrm{\mid }{z}_j{\mathrm{\mid }}_{\mathbb{C}}+\mathrm{\mid }{w}_j{\mathrm{\mid }}_{\mathbb{C}}$ for every $j<n$. Finite-sum monotonicity and additivity [F7, F8] therefore give $N_1(z+w)={\sum }_{j<n}\mathrm{\mid }{z}_j+w_j{\mathrm{\mid }}_{\mathbb{C}}\le {\sum }_{j<n}(\mathrm{\mid }{z}_j{\mathrm{\mid }}_{\mathbb{C}}+\mathrm{\mid }{w}_j{\mathrm{\mid }}_{\mathbb{C}})=N_1(z)+N_1(w)$. Together with steps 1.1 and 1.2, this is the triangle clause in [F9], so all three complex norm criteria hold.

For $w\in W$, $N_W(w)=0$ iff $N(w)=0$ iff $w=0$ by [F1], so the restriction separates zero.

If $w\in W$ and $\lambda \in \mathbb{C}$, then $\lambda w\in W$ by [F2] and $N_W(\lambda w)=N(\lambda w)=\mathrm{\mid }\lambda {\mathrm{\mid }}_{\mathbb{C}}N(w)=\mathrm{\mid }\lambda {\mathrm{\mid }}_{\mathbb{C}}{N}_W(w)$ by [F1]. If $u,w\in W$, then $u+w\in W$ and $N_W(u+w)=N(u+w)\le N(u)+N(w)=N_W(u)+N_W(w)$, again by [F1]. Thus the restricted function has the full complex homogeneity and triangle properties as well.