内積

1 を示す。条件 2、条件 1、複素共役が和と積を保つことにより
$$ \langle x,ay+bz\rangle=\overline{\langle ay+bz,x\rangle}=\overline{a\langle y,x\rangle+b\langle z,x\rangle}=\bar a\,\overline{\langle y,x\rangle}+\bar b\,\overline{\langle z,x\rangle}=\bar a\langle x,y\rangle+\bar b\langle x,z\rangle $$
である。$F=\mathbb{R}$ では $\bar a=a$、$\bar b=b$ である。
2 を示す。条件 1 により $\langle0,x\rangle=\langle0\cdot x,x\rangle=0\cdot\langle x,x\rangle=0$ であり、条件 2 により $\langle x,0\rangle=\overline{\langle0,x\rangle}=\bar0=0$ である。
3 を示す。条件 1 と本命題の 1 により $\langle ax,ax\rangle=a\langle x,ax\rangle=a\bar a\langle x,x\rangle=|a|^2\|x\|^2$ であり、両辺の非負の平方根をとれば $\|ax\|=|a|\|x\|$ である。
4 を示す。条件 1 と本命題の 1 により $\langle x+y,x+y\rangle=\langle x,x\rangle+\langle x,y\rangle+\langle y,x\rangle+\langle y,y\rangle$ であり、条件 2 により $\langle x,y\rangle+\langle y,x\rangle=\langle x,y\rangle+\overline{\langle x,y\rangle}=2\operatorname{Re}\langle x,y\rangle$ である。5 は 4 で $\langle x,y\rangle=0$ とおけばよい。$\square$

$\langle x,y\rangle=0$ なら左辺は $0$、右辺は非負なので不等式は成り立つ。以下 $\langle x,y\rangle\ne0$ とする。このとき prop-inner-product-basic の 2 により $y\ne0$ であり、条件 4 により $\|y\|>0$ である。
$c:=\langle x,y\rangle/|\langle x,y\rangle|$ とおく。$|c|=1$ であり、$\bar c\langle x,y\rangle=|\langle x,y\rangle|^2/|\langle x,y\rangle|=|\langle x,y\rangle|$ である。また条件 2 により $c\langle y,x\rangle=c\,\overline{\langle x,y\rangle}=\overline{\bar c\langle x,y\rangle}=|\langle x,y\rangle|$ である。実数 $t$ に対し、条件 1 と prop-inner-product-basic の 1 により
$$ f(t):=\|x-tcy\|^2=\langle x,x\rangle-t\bar c\langle x,y\rangle-tc\langle y,x\rangle+t^2c\bar c\langle y,y\rangle=\|x\|^2-2t|\langle x,y\rangle|+t^2\|y\|^2 $$
であり、条件 3 により $f(t)\ge0$ がすべての実数 $t$ について成り立つ。とくに $t_0:=|\langle x,y\rangle|/\|y\|^2$ を代入すると
$$ 0\le f(t_0)=\|x\|^2-\frac{2|\langle x,y\rangle|^2}{\|y\|^2}+\frac{|\langle x,y\rangle|^2}{\|y\|^2}=\|x\|^2-\frac{|\langle x,y\rangle|^2}{\|y\|^2} $$
である。両辺に $\|y\|^2>0$ を掛けて $|\langle x,y\rangle|^2\le\|x\|^2\|y\|^2$ を得、両辺の非負の平方根をとれば不等式が従う。（$t_0$ は 2 次関数 $f$ の最小点であり、$f(t_0)\ge0$ は $f$ の判別式が $0$ 以下であることと同じ内容である。）
等号について。まず $|\langle x,y\rangle|=\|x\|\|y\|$ と仮定する。$\langle x,y\rangle=0$ なら $\|x\|\|y\|=0$ であるから $x=0$ または $y=0$ であり、$0=0\cdot y$、$0=0\cdot x$ により $x,y$ は線形従属である。$\langle x,y\rangle\ne0$ なら、上の計算で $f(t_0)=\|x\|^2-|\langle x,y\rangle|^2/\|y\|^2=0$ であるから、条件 4 により $x-t_0cy=0$、すなわち $x=(t_0c)y$ であり、$x$ は $y$ のスカラー倍である。逆に $x=ay$（$a\in F$）なら、条件 1 と prop-inner-product-basic の 3 により $|\langle x,y\rangle|=|a|\,|\langle y,y\rangle|=|a|\|y\|^2=\|ay\|\|y\|=\|x\|\|y\|$ である。$y=ax$ の場合も同様である。$\square$

1 を示す。$\|x\|\ge0$ は平方根の定義による。$\|x\|=0$ は $\langle x,x\rangle=0$ と同値であり、条件 4 によりこれは $x=0$ を導く。逆に $x=0$ なら prop-inner-product-basic の 2 により $\langle0,0\rangle=0$ である。2 は prop-inner-product-basic の 3 である。
3 を示す。prop-inner-product-basic の 4、複素数の実部が絶対値以下であること $\operatorname{Re}w\le|w|$、および thm-inner-product-cauchy-schwarz により
$$ \|x+y\|^2=\|x\|^2+2\operatorname{Re}\langle x,y\rangle+\|y\|^2\le\|x\|^2+2|\langle x,y\rangle|+\|y\|^2\le\|x\|^2+2\|x\|\|y\|+\|y\|^2=(\|x\|+\|y\|)^2 $$
である。両辺は非負なので平方根をとって $\|x+y\|\le\|x\|+\|y\|$ を得る。
等号について。$\|x+y\|=\|x\|+\|y\|$ が成り立つのは上の 2 つの不等号がともに等号のとき、すなわち $\operatorname{Re}\langle x,y\rangle=|\langle x,y\rangle|$ かつ $|\langle x,y\rangle|=\|x\|\|y\|$ のときである。$y=0$ ならこれは成り立ち、$y=0\cdot x$ である。$y\ne0$ のとき、thm-inner-product-cauchy-schwarz の等号条件により $x=ay$ となる $a\in F$ が存在し、$\langle x,y\rangle=a\|y\|^2$ である。$\operatorname{Re}(a\|y\|^2)=|a|\|y\|^2$ と $\|y\|^2>0$ から $\operatorname{Re}a=|a|$、すなわち $a$ は非負実数である。逆に $x=ay$（$a\ge0$）なら、2 により $\|x+y\|=\|(a+1)y\|=(a+1)\|y\|=a\|y\|+\|y\|=\|x\|+\|y\|$ である。$y=ax$（$a\ge0$）の場合も同様である。
4 を示す。3 により $\|x\|=\|(x-y)+y\|\le\|x-y\|+\|y\|$ であるから $\|x\|-\|y\|\le\|x-y\|$ である。$x$ と $y$ を入れ替えると $\|y\|-\|x\|\le\|y-x\|=\|x-y\|$（2 で $a=-1$）であり、あわせて 4 を得る。
最後に $d$ が距離であることを確かめる。$d(x,y)=\|x-y\|\ge0$ であり、$d(x,y)=0$ と $x-y=0$ は 1 により同値である。$d(y,x)=\|y-x\|=\|(-1)(x-y)\|=\|x-y\|=d(x,y)$ は 2 による。$d(x,z)=\|(x-y)+(y-z)\|\le\|x-y\|+\|y-z\|=d(x,y)+d(y,z)$ は 3 による。$\square$

prop-inner-product-basic の 4 を $y$ の代わりに $\lambda y$（$\lambda\in F$）について書き、同 1 により $\langle x,\lambda y\rangle=\bar\lambda\langle x,y\rangle$ であることを使うと
$$ \|x+\lambda y\|^2=\|x\|^2+2\operatorname{Re}\bigl(\bar\lambda\langle x,y\rangle\bigr)+|\lambda|^2\|y\|^2 $$
を得る。
1 を示す。$F=\mathbb{R}$ で $\lambda=1,-1$ とおくと $\|x\pm y\|^2=\|x\|^2\pm2\langle x,y\rangle+\|y\|^2$ であり、辺々引いて $\|x+y\|^2-\|x-y\|^2=4\langle x,y\rangle$ である。
2 を示す。$w:=\langle x,y\rangle=a+bi$（$a,b\in\mathbb{R}$）とおく。$\lambda=i^k$（$k=0,1,2,3$）について $|\lambda|=1$、$\bar\lambda=i^{-k}$ であるから
$$ \|x+i^ky\|^2=\|x\|^2+\|y\|^2+2\operatorname{Re}(i^{-k}w) $$
である。$i^{-k}w$ の実部は、$k=0,1,2,3$ の順に $\operatorname{Re}(w)=a$、$\operatorname{Re}(-iw)=\operatorname{Re}(b-ai)=b$、$\operatorname{Re}(-w)=-a$、$\operatorname{Re}(iw)=\operatorname{Re}(-b+ai)=-b$ である。両辺に $i^k$ を掛けて $k=0$ から $3$ まで加えると、$\sum_{k=0}^{3}i^k=1+i-1-i=0$ により第 1 項は消え、
$$ \sum_{k=0}^{3}i^k\|x+i^ky\|^2=2\bigl(a+ib+(-1)(-a)+(-i)(-b)\bigr)=2(2a+2ib)=4w $$
を得る。
一意性について。$\langle\cdot,\cdot\rangle_1$、$\langle\cdot,\cdot\rangle_2$ が同じノルムを定めるなら、1 または 2 の右辺は両者で一致するので、任意の $x,y$ について $\langle x,y\rangle_1=\langle x,y\rangle_2$ である。$\square$

$q(z):=s(z,z)$ とおく。半双線形性により、任意の $\lambda\in\mathbb{C}$ について
$$ q(x+\lambda y)=s(x,x)+\bar\lambda s(x,y)+\lambda s(y,x)+|\lambda|^2s(y,y) $$
である。$\lambda=i^k$（$k=0,1,2,3$）とおき、両辺に $i^k$ を掛けて加えると、$\sum_ki^k=0$ により $s(x,x)$ と $s(y,y)$ の項は消え、$\sum_ki^k\overline{i^k}=\sum_k1=4$、$\sum_ki^ki^k=\sum_k(-1)^k=0$ により
$$ \sum_{k=0}^{3}i^kq(x+i^ky)=4s(x,y) $$
を得る（半双線形形式の極化恒等式）。$x$ と $y$ を入れ替えると $4s(y,x)=\sum_ki^kq(y+i^kx)$ である。ここで $y+i^kx=i^k(x+i^{-k}y)$ であり、半双線形性から $q(i^kz)=i^k\overline{i^k}q(z)=q(z)$ であるから $q(y+i^kx)=q(x+i^{-k}y)$ である。$k$ を $4$ を法として $-k$ に置き換えて和を取り直すと
$$ 4s(y,x)=\sum_{k=0}^{3}i^{-k}q(x+i^ky) $$
である。仮定により各 $q(x+i^ky)$ は実数なので、右辺は $\sum_ki^kq(x+i^ky)=4s(x,y)$ の複素共役に等しい。よって $s(y,x)=\overline{s(x,y)}$ である。
後半について。条件 3 は各 $s(x,x)$ が非負の実数であることを主張するので、前半が適用できる。$\square$

1 は条件 2 により $\langle y,x\rangle=\overline{\langle x,y\rangle}=\bar0=0$ であることによる。2 は prop-inner-product-basic の 2 である。3 は条件 4 と本命題の 2 による。4 は、$y=x$ ととれば $\langle x,x\rangle=0$ となり 3 から従う。5 は prop-inner-product-basic の 1 により $\langle x,\sum_kb_ky_k\rangle=\sum_k\overline{b_k}\langle x,y_k\rangle=0$ であることによる。
6 を示す。$a_1x_1+\cdots+a_nx_n=0$（$a_k\in F$）とする。両辺と $x_j$ の内積をとると、条件 1 と直交性により $0=\sum_ka_k\langle x_k,x_j\rangle=a_j\langle x_j,x_j\rangle=a_j\|x_j\|^2$ であり、$x_j\ne0$ より $\|x_j\|^2>0$ であるから $a_j=0$ である。よって線形独立である。ノルムの等式は $n$ についての帰納法による。$n=1$ は自明であり、$n\ge2$ のとき $x:=x_1+\cdots+x_{n-1}$ とおくと 5 により $x_n\perp x$、したがって 1 により $x\perp x_n$ であり、prop-inner-product-basic の 5 と帰納法の仮定により $\|x+x_n\|^2=\|x\|^2+\|x_n\|^2=\|x_1\|^2+\cdots+\|x_n\|^2$ である。$\square$

1 を示す。$s_A(x,y)=\sum_{i,j}a_{ij}x_j\overline{y_i}$ は $x$ の各成分について 1 次であり、$y$ の各成分の複素共役について 1 次であるから、$s_A(ax+bx',y)=as_A(x,y)+bs_A(x',y)$ および $s_A(x,ay+by')=\bar as_A(x,y)+\bar bs_A(x,y')$ が成り立つ。
2 を示す。$s_A(x,y)=y^{*}Ax$ は $1\times1$ 行列（スカラー）なので、その複素共役は共役転置に等しく、$\overline{s_A(x,y)}=(y^{*}Ax)^{*}=x^{*}A^{*}y$ である。一方 $s_A(y,x)=x^{*}Ay$ である。したがって $s_A$ が共役対称であることは、すべての $x,y$ について $x^{*}Ay=x^{*}A^{*}y$ が成り立つことと同値である。$A^{*}=A$ ならこれは明らかに成り立つ。逆にこれが成り立つなら、$x=e_i$、$y=e_j$ とおいて $e_i^{*}Ae_j=a_{ij}$、$e_i^{*}A^{*}e_j=\overline{a_{ji}}$ を得るので $a_{ij}=\overline{a_{ji}}$、すなわち $A^{*}=A$ である。$F=\mathbb{R}$ では $A^{*}=A^{\mathsf{T}}$ である。
3 を示す。$s_A$ は 1 により条件 1 を満たす。条件 2 は 2 により $A^{*}=A$ と同値である。$A^{*}=A$ のとき $s_A(x,x)=x^{*}Ax$ は 2 により実数であり、条件 3・4 をあわせたものは「$x\ne0$ ならば $x^{*}Ax>0$」と同値である。
4 を示す。$x=\sum_jx_je_j$、$y=\sum_iy_ie_i$ と書くと、条件 1 と prop-inner-product-basic の 1 により
$$ \langle x,y\rangle=\Bigl\langle\sum_jx_je_j,\sum_iy_ie_i\Bigr\rangle=\sum_{i,j}x_j\overline{y_i}\langle e_j,e_i\rangle=\sum_{i,j}a_{ij}x_j\overline{y_i}=s_A(x,y) $$
である。一意性について、$s_A=s_B$ なら $x=e_j$、$y=e_i$ とおいて $a_{ij}=s_A(e_j,e_i)=s_B(e_j,e_i)=b_{ij}$ である。$\square$