[proofplan] The proof converts the symplectic complement into an ordinary annihilator in the dual [vector space](/page/Vector%20Space). The nondegenerate form $\omega$ gives an isomorphism $\Phi:V\to V^*$, and $W^\omega$ is exactly the preimage under $\Phi$ of the annihilator $W^0\subset V^*$. We compute the dimension of $W^0$ by the restriction map $V^*\to W^*$, which gives the dimension formula. Finally, skew-symmetry gives the inclusion $W\subset (W^\omega)^\omega$, and the dimension formula applied to $W^\omega$ forces equality. [/proofplan] [step:Identify the symplectic complement with an annihilator in the dual space] Define the [linear map](/page/Linear%20Map) \begin{align*} \Phi:V\to V^* \end{align*} by \begin{align*} \Phi(v)(u):=\omega(v,u) \end{align*} for $v,u\in V$. Since $\omega$ is nondegenerate, $\ker\Phi=\{0\}$. Because $V$ is finite-dimensional and $\dim V=\dim V^*$, the injective linear map $\Phi$ is an isomorphism. Define the annihilator of $W$ in $V^*$ by \begin{align*} W^0:=\{\ell\in V^*:\ell(w)=0\text{ for every }w\in W\}. \end{align*} For $v\in V$, we have \begin{align*} v\in W^\omega \iff \omega(v,w)=0\text{ for every }w\in W \iff \Phi(v)\in W^0. \end{align*} Thus \begin{align*} W^\omega=\Phi^{-1}(W^0). \end{align*} Since $\Phi$ is an isomorphism, it restricts to a linear isomorphism $W^\omega\to W^0$, so \begin{align*} \dim W^\omega=\dim W^0. \end{align*} [/step] [step:Compute the dimension of the annihilator by restriction to $W$] Define the restriction map \begin{align*} \rho:V^*\to W^* \end{align*} by \begin{align*} \rho(\ell):=\ell|_W \end{align*} for $\ell\in V^*$. Its kernel is exactly $W^0$. The map $\rho$ is surjective: if $\alpha\in W^*$, choose a basis $(e_1,\dots,e_k)$ of $W$ and extend it to a basis $(e_1,\dots,e_k,e_{k+1},\dots,e_m)$ of $V$. Define $\ell\in V^*$ by $\ell(e_i)=\alpha(e_i)$ for $1\le i\le k$ and $\ell(e_j)=0$ for $k<j\le m$. Then $\rho(\ell)=\alpha$. By rank-nullity applied to $\rho$, \begin{align*} \dim V^*=\dim\ker\rho+\dim W^*. \end{align*} Using $\ker\rho=W^0$, $\dim V^*=\dim V$, and $\dim W^*=\dim W$, we obtain \begin{align*} \dim W^0=\dim V-\dim W. \end{align*} Together with $\dim W^\omega=\dim W^0$, this gives \begin{align*} \dim W+\dim W^\omega=\dim V. \end{align*} [guided] We need the dimension of $W^\omega$, but the previous step reduced this to the dimension of the annihilator $W^0\subset V^*$. The clean way to compute $\dim W^0$ is to use the restriction map from linear functionals on $V$ to linear functionals on $W$. Define \begin{align*} \rho:V^*\to W^* \end{align*} by \begin{align*} \rho(\ell):=\ell|_W \end{align*} for each $\ell\in V^*$. The kernel of $\rho$ consists exactly of those linear functionals on $V$ whose restriction to $W$ is zero. By the definition of the annihilator, this kernel is \begin{align*} \ker\rho=W^0. \end{align*} We next verify that $\rho$ is surjective. Let $\alpha\in W^*$ be any linear functional on $W$. Choose a basis $(e_1,\dots,e_k)$ of $W$, and extend it to a basis $(e_1,\dots,e_k,e_{k+1},\dots,e_m)$ of $V$. Define a linear functional $\ell\in V^*$ on this basis by setting $\ell(e_i)=\alpha(e_i)$ for $1\le i\le k$ and $\ell(e_j)=0$ for $k<j\le m$, then extending linearly to all of $V$. For every vector $w\in W$, write $w=\sum_{i=1}^k a_i e_i$ with scalars $a_1,\dots,a_k\in\mathbb R$. Then \begin{align*} \ell(w)=\sum_{i=1}^k a_i\ell(e_i)=\sum_{i=1}^k a_i\alpha(e_i)=\alpha(w). \end{align*} Hence $\rho(\ell)=\alpha$, so $\rho$ is surjective. Now apply rank-nullity to the linear map $\rho:V^*\to W^*$. Since $\rho$ is surjective, its image has dimension $\dim W^*$, and rank-nullity gives \begin{align*} \dim V^*=\dim\ker\rho+\dim W^*. \end{align*} Substituting $\ker\rho=W^0$, $\dim V^*=\dim V$, and $\dim W^*=\dim W$, we get \begin{align*} \dim W^0=\dim V-\dim W. \end{align*} The previous step proved $\dim W^\omega=\dim W^0$, so \begin{align*} \dim W^\omega=\dim V-\dim W. \end{align*} Rearranging gives the desired dimension formula: \begin{align*} \dim W+\dim W^\omega=\dim V. \end{align*} [/guided] [/step] [step:Use skew-symmetry and dimensions to identify the double symplectic complement] We first prove the inclusion $W\subset (W^\omega)^\omega$. Let $w\in W$ and let $x\in W^\omega$. By definition of $W^\omega$, \begin{align*} \omega(x,w)=0. \end{align*} Since $\omega$ is skew-symmetric, \begin{align*} \omega(w,x)=-\omega(x,w)=0. \end{align*} Thus $w\in (W^\omega)^\omega$, proving $W\subset (W^\omega)^\omega$. Apply the dimension formula already proved to the subspace $W^\omega\subset V$. This gives \begin{align*} \dim W^\omega+\dim (W^\omega)^\omega=\dim V. \end{align*} The dimension formula for $W$ gives \begin{align*} \dim W+\dim W^\omega=\dim V. \end{align*} Subtracting $\dim W^\omega$ from both equalities yields \begin{align*} \dim (W^\omega)^\omega=\dim W. \end{align*} The inclusion $W\subset (W^\omega)^\omega$ is therefore an inclusion of finite-dimensional subspaces of equal dimension, so \begin{align*} (W^\omega)^\omega=W. \end{align*} This completes the proof. [/step]