Cauchy–Schwarz: $\mathrm{\mid }⟨x,y⟩\mathrm{\mid }\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }y\mathrm{\parallel }$, with equality exactly for dependent pairs

If $y=0$, then $⟨x,y⟩=⟨x,0\cdot y⟩=0\cdot ⟨x,y⟩=0$ by conjugate-linearity in the second argument, and $\mathrm{\parallel }y\mathrm{\parallel }=0$; hence $\mathrm{\mid }⟨x,y⟩\mathrm{\mid }=0=\mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }y\mathrm{\parallel }$, while $x,y$ are dependent with witness scalars $(a,b)=(0,1)$ because $0\cdot x+1\cdot 0=0$ and $b\mathrm{\ne }0$.

Suppose now $y\mathrm{\ne }0$ and set $c=⟨x,y⟩\mathrm{/}⟨y,y⟩$, a well-defined scalar because $⟨y,y⟩=\mathrm{\parallel }y{\mathrm{\parallel }}^2>0$; expanding with linearity in the first argument, conjugate-linearity in the second and conjugate symmetry gives $0\le \mathrm{\parallel }x-cy{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2-c\overline{⟨x,y⟩}-\bar{c}⟨x,y⟩+\mathrm{\mid }c{\mathrm{\mid }}^2\mathrm{\parallel }y{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2-\mathrm{\mid }⟨x,y⟩{\mathrm{\mid }}^2\mathrm{/}\mathrm{\parallel }y{\mathrm{\parallel }}^2$.

Multiplying step 1.2 by the positive number $\mathrm{\parallel }y{\mathrm{\parallel }}^2$ gives $\mathrm{\mid }⟨x,y⟩{\mathrm{\mid }}^2\le \mathrm{\parallel }x{\mathrm{\parallel }}^2\mathrm{\parallel }y{\mathrm{\parallel }}^2$, and since $\mathrm{\mid }⟨x,y⟩\mathrm{\mid }$, $\mathrm{\parallel }x\mathrm{\parallel }$ and $\mathrm{\parallel }y\mathrm{\parallel }$ are nonnegative, monotonicity of squaring on the nonnegatives gives the inequality $\mathrm{\mid }⟨x,y⟩\mathrm{\mid }\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }y\mathrm{\parallel }$.

If $x,y$ are dependent, then either $y=0$, which is step 1.1, or $x=cy$ for some scalar $c$ with $y\mathrm{\ne }0$; in the second case $⟨x,y⟩=c\mathrm{\parallel }y{\mathrm{\parallel }}^2$ and $\mathrm{\parallel }cy{\mathrm{\parallel }}^2=⟨cy,cy⟩=\mathrm{\mid }c{\mathrm{\mid }}^2\mathrm{\parallel }y{\mathrm{\parallel }}^2$ with both norms nonnegative, so $\mathrm{\parallel }x\mathrm{\parallel }=\mathrm{\mid }c\mathrm{\mid }\mathrm{\parallel }y\mathrm{\parallel }$ by uniqueness of nonnegative square roots, and $\mathrm{\mid }⟨x,y⟩\mathrm{\mid }=\mathrm{\mid }c\mathrm{\mid }\mathrm{\parallel }y{\mathrm{\parallel }}^2=\mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }y\mathrm{\parallel }$.

Conversely suppose $\mathrm{\mid }⟨x,y⟩\mathrm{\mid }=\mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }y\mathrm{\parallel }$ and $y\mathrm{\ne }0$; then $\mathrm{\parallel }y{\mathrm{\parallel }}^2>0$ and step 1.2 gives $\mathrm{\parallel }x-cy{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2-\mathrm{\parallel }x{\mathrm{\parallel }}^2=0$, so $x-cy=0$ by positive definiteness, that is $x=cy$ and the pair is dependent by [A7]; together with steps 1.1 and 2.2 this proves the inequality and both directions of the equality statement.