ThmDex – An index of mathematical definitions, results, and conjectures.
P1097
Let $x, y \in I$ such that $\langle x, y \rangle = 0$. Since $\langle x, y \rangle \in \mathbb{R}$, applying R2413: Complex conjugate of real number and the conjugate symmetry of inner products, we conclude \begin{equation} \langle y, x \rangle = \overline{\langle x, y \rangle} = \langle x, y \rangle = 0 \end{equation} $\square$