Proof of The Standard Inner Product Makes the Complex Coordinate Space an Inner Product Space

Let $u,v,w\in\mathbb{C}^{n}$ and $\lambda\in\mathbb{C}$, with components and componentwise operations as in The Complex Coordinate Space. All sums are the finite sums of that definition, with the properties of Properties of Finite Sums, and we use the properties of conjugation and of the modulus recorded in Properties of Complex Conjugation and Modulus. Conditions 1-4 are those of Complex Inner Product Space.

Condition 1 (conjugate symmetry). By claim 3 of Properties of Finite Sums, then the multiplicativity and involutivity of conjugation (claim 1 of Properties of Complex Conjugation and Modulus), and commutativity of multiplication,

Condition 2 (additivity in the second argument). The $k$-th component of $v+w$ is $v_{k}+w_{k}$, so by the distributive law and claim 1 of Properties of Finite Sums,

Condition 3 (homogeneity in the second argument). The $k$-th component of $\lambda v$ is $\lambda v_{k}$, so by commutativity and associativity of multiplication and claim 2 of Properties of Finite Sums,

Condition 4 (positive definiteness). By claim 3 of Properties of Complex Conjugation and Modulus and commutativity of multiplication, $\overline{u_{k}}u_{k}=u_{k}\overline{u_{k}}=|u_{k}|^{2}$ for every $k$, so

Each $|u_{k}|$ is a real number with $0\le|u_{k}|$, hence $0\le|u_{k}|^{2}$ by the second order-compatibility condition of ordered fields. Since sums of real numbers formed in $\mathbb{C}$ coincide with those formed in $\mathbb{R}$, by condition 1 of The Complex Numbers together with the recursion defining finite sums, the displayed sum is a real number, and $0\le\langle u,u\rangle$ by claim 4 of Properties of Finite Sums. If moreover $\langle u,u\rangle=0$, the same claim gives $|u_{k}|^{2}=0$ for every $k$; a field has no zero divisors, so $|u_{k}|=0$, and then $u_{k}=0$ by claim 3 of Properties of Complex Conjugation and Modulus. Thus every component of $u$ is $0$, that is, $u$ is the zero vector of The Complex Coordinate Space is a Complex Vector Space.

Hence all four conditions hold, which proves claim 1.

Claim 2. By Norm Induced by a Complex Inner Product, $\lVert u\rVert^{2}=\langle u,u\rangle$, which equals $\sum_{k=1}^{n}|u_{k}|^{2}$ by the computation above.