ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1372 on D34: Inner product
Inner product is zero if either argument is zero
Formulation 0
Let $I$ be an D1128: Inner product space over $\mathbb{C}$ such that
(i) $0_I$ is a D737: Zero vector in $I$
(ii) $\langle \cdot, \cdot \rangle$ is the D34: Inner product in $I$
(iii) $x \in I$ is a D1129: Vector in $I$
Then \begin{equation} \langle x, 0_I \rangle = \langle 0_I, x \rangle = 0 \end{equation}
Proofs
Proof 0
Let $I$ be an D1128: Inner product space over $\mathbb{C}$ such that
(i) $0_I$ is a D737: Zero vector in $I$
(ii) $\langle \cdot, \cdot \rangle$ is the D34: Inner product in $I$
(iii) $x \in I$ is a D1129: Vector in $I$
This result is a particular case of R1371: Bilinear map is zero if either argument is zero. $\square$