Norm satisfying Parallelogram Law induced by Inner Product/Complex Case

== Theorem ==
Let $V$ be a vector space over $\R$.
Let $\norm \cdot : V \to \R$ be a norm on $V$ such that: 
:$\norm {x + y}^2 + \norm {x - y}^2 = 2 \paren {\norm x^2 + \norm y^2}$
for each $x, y \in V$.
Then the function $\innerprod \cdot \cdot : V \times V \to \C$ defined by: 
:$\ds \innerprod x y = \frac 1 4 \sum_{k \mathop = 0}^3 i^k \norm {x + i^k y}^2$
for each $x, y \in V$, is an inner product on $V$.
Further, $\norm {\, \cdot \,}$ is the inner product norm of $\struct {V, \innerprod \cdot \cdot}$.
== Proof ==
We write out:
:$\innerprod x y = \dfrac 1 4 \paren {\norm {x + y}^2 + i \norm {x + i y}^2 - \norm {x - y}^2 - i \norm {x - i y}^2}$
We show that $\innerprod \cdot \cdot$ is an inner product. 
=== Proof of conjugate symmetry ===
For each $x, y \in V$, we have:
=== Proof of linearity in first argument ===
First, for each $x, y \in V$, we have:
We also have:
:$\ds \map \Re {\innerprod x y} = \frac 1 4 \paren {\norm {x + y}^2 - \norm {x - y}^2}$
Let $V_\R$ be the realification of $V$.
Define $\innerprod \cdot \cdot_\R : V \times V \to \R$ by:
:$\innerprod x y_\R = \map \Re {\innerprod x y}$
Note that by hypothesis:
:$\norm {x + y}^2 + \norm {x - y}^2 = 2 \paren {\norm x^2 + \norm y^2}$ for each $x, y \in V$.
By Norm satisfying Parallelogram Law induced by Inner Product: Real Case, we have that $\innerprod \cdot \cdot_\R$ is an inner product on $V_\R$.
We therefore have:
:$\innerprod {x + y} z_\R = \innerprod x z_\R + \innerprod y z_\R$
for each $x, y, z \in V$.
That is:
:$\map \Re {\innerprod {x + y} z} = \map \Re {\innerprod x z} + \map \Re {\innerprod y z}$
for each $x, y, z \in V$.
In particular:
:$\map \Re {\innerprod {i x + i y} z} = \map \Re {\innerprod {i x} z} + \map \Re {\innerprod {i y} z}$
for each $x, y \in V$, so that:
:$\map \Re {i \innerprod {x + y} z} = \map \Re {i \innerprod x z} + \map \Re {i \innerprod y z}$
From Imaginary Part of Complex Product, we have:
:$\map \Re {i z} = -\map \Im z$
for each $z \in \C$.
We therefore have:
:$-\map \Im {\innerprod {x + y} z} = -\map \Im {\innerprod x z} - \map \Im {\innerprod y z}$
and hence:
:$\map \Im {\innerprod {x + y} z} = \map \Im {\innerprod x z} + \map \Im {\innerprod y z}$
for each $x, y, z \in V$.
We can conclude that:
for each $x, y, z \in V$.
Finally, let $\alpha, \beta \in \R$ and $x, y \in V$.
We then have, for $\lambda = \alpha + i \beta$:
Hence $\innerprod \cdot \cdot$ is linear in its first argument.
=== Proof of non-negative definiteness ===
For each $x \in V$, we have:
We also have:
:$\map \Re {\innerprod x x} = \frac 1 4 \paren {\norm {2 x}^2 - \norm { {\mathbf 0}_V}^2} = \norm x^2 \ge 0$
by and . 
Hence we have:
:$\innerprod x x \in \R_{\ge 0}$ for each $x \in V$. 
=== Proof of positiveness ===
We have:
:$\innerprod x x = \norm x^2$ 
for each $x \in V$.
Hence from , we have $\innerprod x x = 0$ $x = {\mathbf 0}_V$. 
=== Proof that $\innerprod \cdot \cdot$ induces $\norm {\, \cdot \,}$ ===
As above we have:
:$\innerprod x x = \norm x^2$
for each $x \in V$.
Hence we have:
:$\norm x = \sqrt {\innerprod x x}$ for each $x \in V$.
From the definition of the inner product norm, $\innerprod \cdot \cdot$ induces $\norm {\, \cdot \,}$.
Category:Norm satisfying Parallelogram Law induced by Inner Product