Real Inner Product Spaces

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $V$ be a real vector space, with sum $u+v$, scalar multiple $\lambda v$ and zero vector $0_V$. Consider a function $\langle\cdot,\cdot\rangle:V\times V\to\mathbb{R}$ and the following conditions, for all $u,v,w\in V$ and all $\lambda\in\mathbb{R}$.

(i) Symmetry.

$$\langle u,v\rangle=\langle v,u\rangle.$$

(ii) Additivity in the first argument.

$$\langle u+v,w\rangle=\langle u,w\rangle+\langle v,w\rangle.$$

(iii) Homogeneity in the first argument.

$$\langle \lambda u,v\rangle=\lambda\,\langle u,v\rangle.$$

(iv) Positive definiteness. $\langle v,v\rangle\ge0$, and $\langle v,v\rangle=0$ only if $v=0_V$.

(v) Inner product. A function $\langle\cdot,\cdot\rangle:V\times V\to\mathbb{R}$ is an inner product on $V$ if it satisfies (i), (ii), (iii) and (iv).

(vi) Real inner product space. A real inner product space is a real vector space $V$ together with an inner product $\langle\cdot,\cdot\rangle$ on $V$.

(vii) Induced norm. In a real inner product space $V$, the norm of $v\in V$ is the square root

$$\|v\|=\sqrt{\langle v,v\rangle},$$

which is defined since $\langle v,v\rangle\ge0$ by (iv). The function $v\mapsto\|v\|$ is the induced norm of $V$.