[proofplan] We show $W \cap W^\perp = \{\mathbf{0}\}$ by positive-definiteness, then compute $\dim W^\perp = n - k$ using a surjective map $V \to \mathbb{F}^k$ whose kernel is $W^\perp$. Combining $\dim W + \dim W^\perp = n$ with the trivial intersection gives $V = W \oplus W^\perp$. [/proofplan] [step:Show $W \cap W^\perp = \{\mathbf{0}\}$ by positive-definiteness] If $v \in W \cap W^\perp$, then $v \in W$ and $(v, w) = 0$ for all $w \in W$. In particular, taking $w = v$: $(v, v) = 0$. By positive-definiteness of the inner product, $v = \mathbf{0}$. [/step] [step:Compute $\dim W^\perp = n - k$ via a surjective linear map] Choose an orthonormal basis $(e_1, \dots, e_k)$ for $W$ by [Gram-Schmidt](/theorems/435). Define $\Phi: V \to \mathbb{F}^k$ by \begin{align*} \Phi(v) = \bigl((e_1, v),\; (e_2, v),\; \dots,\; (e_k, v)\bigr). \end{align*} This map is linear (the inner product is linear in the second argument). A vector $v$ lies in $\ker\Phi$ if and only if $(e_i, v) = 0$ for all $i = 1, \dots, k$, which holds if and only if $v \in W^\perp$ (since $(e_1, \dots, e_k)$ spans $W$). So $\ker\Phi = W^\perp$. The map $\Phi$ is surjective: for any $(c_1, \dots, c_k) \in \mathbb{F}^k$, the vector $v = \sum_{i=1}^k c_i\,e_i$ satisfies $\Phi(v) = (c_1, \dots, c_k)$ by orthonormality. By [Rank-Nullity](/theorems/384): $\dim W^\perp = \dim\ker\Phi = \dim V - \dim\mathrm{im}\,\Phi = n - k$. [guided] We need $\dim W^\perp = n - k$ to conclude the direct sum. The map $\Phi$ is designed so that its kernel captures exactly the orthogonal complement. A vector $v$ is orthogonal to $W$ if and only if $(w, v) = 0$ for every $w \in W$. Since $(e_1, \dots, e_k)$ is a basis for $W$, it suffices to check $(e_i, v) = 0$ for $i = 1, \dots, k$ (by linearity of the inner product in the first argument), and this is exactly the condition $\Phi(v) = \mathbf{0}$, so $\ker\Phi = W^\perp$. To show surjectivity, observe that $\Phi(e_j) = (\delta_{1j}, \delta_{2j}, \dots, \delta_{kj})$ is the $j$-th standard basis vector of $\mathbb{F}^k$ for $j = 1, \dots, k$, so $\Phi(e_1), \dots, \Phi(e_k)$ span $\mathbb{F}^k$ and $\Phi$ is surjective. By [Rank-Nullity](/theorems/384): $\dim W^\perp = n - k$. [/guided] [/step] [step:Conclude $V = W \oplus W^\perp$ by the dimension count] We have $\dim(W + W^\perp) = \dim W + \dim W^\perp - \dim(W \cap W^\perp) = k + (n - k) - 0 = n = \dim V$. So $V = W + W^\perp$, and since $W \cap W^\perp = \{\mathbf{0}\}$, the sum is direct. By construction, $(w, w') = 0$ for all $w \in W$ and $w' \in W^\perp$, so the direct sum is orthogonal. [/step]