[proofplan]
We define the left-evaluation map $L: V \to V^*$ by $v \mapsto B(v, \cdot)$ and show nondegeneracy makes it an isomorphism. The orthogonal complement $W^\perp$ is then identified with the preimage $L^{-1}(W^0)$ of the annihilator $W^0 \subset V^*$, whose dimension is computed via the [Rank-Nullity Theorem](/theorems/916) applied to the restriction map $V^* \to W^*$. The double-complement identity $(W^\perp)^\perp = W$ follows by combining the dimension formula with the inclusion $W \subset (W^\perp)^\perp$.
[/proofplan]
[step:Construct the isomorphism $L: V \to V^*$ from the nondegenerate form]
Define the linear map
\begin{align*}
L: V &\to V^* \\
v &\mapsto B(v, \cdot),
\end{align*}
where for each $v \in V$, the functional $B(v, \cdot): V \to k$ acts by $w \mapsto B(v, w)$. Linearity of $L$ follows from linearity of $B$ in the first argument: for all $v_1, v_2 \in V$, $\lambda \in k$, and $w \in V$,
\begin{align*}
L(\lambda v_1 + v_2)(w) = B(\lambda v_1 + v_2,\, w) = \lambda B(v_1, w) + B(v_2, w) = (\lambda L(v_1) + L(v_2))(w).
\end{align*}
We show $L$ is injective. If $v \in \ker L$, then $L(v) = 0$, meaning $B(v, w) = 0$ for all $w \in V$. Since $B$ is nondegenerate, this forces $v = 0$. Hence $\ker L = \{0\}$. Since $\dim V = \dim V^*$, the [Rank-Nullity Theorem](/theorems/916) gives $\dim \operatorname{im}(L) = \dim V$, so $L$ is an isomorphism.
[guided]
The key construction is a map that translates the bilinear form $B$ into the language of dual spaces. For each $v \in V$, "freezing" the first argument of $B$ yields a linear functional $B(v, \cdot) \in V^*$. Define
\begin{align*}
L: V &\to V^* \\
v &\mapsto B(v, \cdot).
\end{align*}
Why is $L$ itself linear (not just each $L(v)$)? Because $B$ is linear in the first argument. For any $v_1, v_2 \in V$, $\lambda \in k$, and test vector $w \in V$:
\begin{align*}
L(\lambda v_1 + v_2)(w) = B(\lambda v_1 + v_2,\, w) = \lambda B(v_1, w) + B(v_2, w) = (\lambda L(v_1) + L(v_2))(w).
\end{align*}
Since this holds for every $w$, we conclude $L(\lambda v_1 + v_2) = \lambda L(v_1) + L(v_2)$.
Is $L$ an isomorphism? The hypothesis that $B$ is nondegenerate means precisely that $\ker L = \{0\}$: if $L(v) = 0$, then $B(v, w) = 0$ for all $w \in V$, and nondegeneracy forces $v = 0$. Since $V$ is finite-dimensional, $\dim V^* = \dim V$, and an injective linear map between spaces of equal finite dimension is automatically surjective. By the [Rank-Nullity Theorem](/theorems/916), $\dim \operatorname{im}(L) = \dim V - 0 = \dim V$, confirming bijectivity.
This isomorphism $L: V \xrightarrow{\sim} V^*$ is the bridge between orthogonality under $B$ and annihilators in $V^*$.
[/guided]
[/step]
[step:Identify $W^\perp$ with the preimage of the annihilator $W^0$]
Define the annihilator of $W$ in $V^*$:
\begin{align*}
W^0 := \{f \in V^* : f(w) = 0 \text{ for all } w \in W\}.
\end{align*}
A vector $v \in V$ belongs to $W^\perp$ if and only if $B(v, w) = 0$ for all $w \in W$, which is equivalent to $L(v)(w) = 0$ for all $w \in W$, which is equivalent to $L(v) \in W^0$. Therefore
\begin{align*}
W^\perp = L^{-1}(W^0).
\end{align*}
Since $L$ is an isomorphism, it restricts to a linear bijection $L|_{W^\perp}: W^\perp \xrightarrow{\sim} W^0$, so $\dim W^\perp = \dim W^0$.
[/step]
[step:Compute $\dim W^0$ via the restriction map and conclude the dimension formula]
Define the restriction map
\begin{align*}
\rho: V^* &\to W^* \\
f &\mapsto f|_W.
\end{align*}
This is a linear map with $\ker \rho = W^0$. We verify surjectivity: given $g \in W^*$, choose a basis $(w_1, \ldots, w_m)$ of $W$ and extend it to a basis $(w_1, \ldots, w_m, v_{m+1}, \ldots, v_n)$ of $V$ where $n = \dim V$ and $m = \dim W$. Define $f \in V^*$ by $f(w_i) = g(w_i)$ for $1 \leq i \leq m$ and $f(v_j) = 0$ for $m+1 \leq j \leq n$, extended by linearity. Then $f|_W = g$, so $\rho$ is surjective.
By the [Rank-Nullity Theorem](/theorems/916) applied to $\rho$:
\begin{align*}
\dim V^* = \dim \ker \rho + \dim \operatorname{im}(\rho) = \dim W^0 + \dim W^*.
\end{align*}
Since $\dim V^* = \dim V$ and $\dim W^* = \dim W$, we obtain $\dim W^0 = \dim V - \dim W$. Combining with $\dim W^\perp = \dim W^0$:
\begin{align*}
\dim W + \dim W^\perp = \dim W + (\dim V - \dim W) = \dim V.
\end{align*}
[guided]
We need the dimension of the annihilator $W^0 \subset V^*$. The standard tool is the **restriction map**
\begin{align*}
\rho: V^* &\to W^* \\
f &\mapsto f|_W,
\end{align*}
which sends each linear functional on $V$ to its restriction to the subspace $W$. This is linear, and its kernel is precisely $W^0$: a functional $f \in V^*$ satisfies $\rho(f) = 0$ if and only if $f(w) = 0$ for all $w \in W$.
Is $\rho$ surjective? Given $g \in W^*$, we must produce $f \in V^*$ with $f|_W = g$. Choose a basis $(w_1, \ldots, w_m)$ of $W$ and extend to a basis $(w_1, \ldots, w_m, v_{m+1}, \ldots, v_n)$ of $V$. Define $f$ by $f(w_i) = g(w_i)$ for $i \leq m$ and $f(v_j) = 0$ for $j > m$, extended linearly. Then $f|_W = g$, confirming surjectivity.
The [Rank-Nullity Theorem](/theorems/916) applied to $\rho: V^* \to W^*$ gives:
\begin{align*}
n = \dim V^* = \dim \ker \rho + \dim \operatorname{im}(\rho) = \dim W^0 + m,
\end{align*}
where $n = \dim V$ and $m = \dim W$ (using $\dim V^* = \dim V$ and surjectivity of $\rho$). Solving: $\dim W^0 = n - m$. Since $\dim W^\perp = \dim W^0$ from the previous step:
\begin{align*}
\dim W + \dim W^\perp = m + (n - m) = n = \dim V.
\end{align*}
[/guided]
[/step]
[step:Prove the double-complement identity $(W^\perp)^\perp = W$]
First, we establish the inclusion $W \subset (W^\perp)^\perp$. Let $w \in W$ and let $v \in W^\perp$ be arbitrary. By definition of $W^\perp$, we have $B(v, w) = 0$. Since $B$ is either symmetric or skew-symmetric (the standard setting for this theorem), $B(w, v) = \pm B(v, w) = 0$. Therefore $B(w, v) = 0$ for all $v \in W^\perp$, which means $w \in (W^\perp)^\perp$. This gives $W \subset (W^\perp)^\perp$.
Next, we compute the dimension of $(W^\perp)^\perp$ by applying the dimension formula (proved above) with $W^\perp$ in place of $W$:
\begin{align*}
\dim(W^\perp)^\perp = \dim V - \dim W^\perp = \dim V - (\dim V - \dim W) = \dim W.
\end{align*}
Since $W \subset (W^\perp)^\perp$ and both subspaces have dimension $\dim W$, they must be equal: $(W^\perp)^\perp = W$.
[guided]
The double-complement identity requires two ingredients: an inclusion and a dimension count.
**Inclusion $W \subset (W^\perp)^\perp$.** Take any $w \in W$. We must show $w \in (W^\perp)^\perp$, meaning $B(w, v) = 0$ for every $v \in W^\perp$. Fix $v \in W^\perp$. By definition of $W^\perp$, $B(v, w') = 0$ for all $w' \in W$; in particular $B(v, w) = 0$. Since $B$ is symmetric or skew-symmetric, $B(w, v) = \pm B(v, w) = 0$. (For a general nondegenerate form, the same conclusion holds by using the right orthogonal complement and the analogous isomorphism $v \mapsto B(\cdot, v)$.) Hence $w \in (W^\perp)^\perp$.
**Dimension count.** We apply the dimension formula $\dim S + \dim S^\perp = \dim V$ with $S = W^\perp$:
\begin{align*}
\dim(W^\perp)^\perp = \dim V - \dim W^\perp = \dim V - (\dim V - \dim W) = \dim W.
\end{align*}
Since $W \subset (W^\perp)^\perp$ and $\dim W = \dim(W^\perp)^\perp$, a subspace of a finite-dimensional space that is contained in another subspace of the same dimension must equal it. Therefore $(W^\perp)^\perp = W$.
Why is the dimension argument necessary? The inclusion $W \subset (W^\perp)^\perp$ alone does not rule out $(W^\perp)^\perp$ being strictly larger than $W$. The dimension formula provides the matching dimension that forces equality.
[/guided]
[/step]