For $W \leqslant V$, prove $\dim W + \dim W^\perp = \dim V$ I want to prove that if $W$ is a subspace of an inner product space $V$, then $\dim W + \dim W^\perp  = \dim V$. I have defined $x^\perp = \{ y : x \cdot y = 0\}$, where $\cdot$ denotes the dot product.
It is a pretty elementary result, but I'm not sure how to prove it, and the answer on A Similar Question seemed unclear to me. What is the simplest proof of this? I have also consulted This Answer, but I'm not sure where to take the hints given. I'm looking for a clear and explicit proof.
 A: Take a basis $w_1\dots w_k$ of $W$, extend it with $v_{k+1}\dots v_n$ to be a basis of $V$, then apply Gram-Schmidt procedure to obtain an orthonormal basis $u_1\dots u_k,\ u_{k+1}\dots u_n$ of $V$. Then the $u_i$, $i=k+1\dots n$ are in $W^\perp$. The systems $u_1\dots u_k$ and $u_{k+1}\dots u_n$ are bases of $W$ and $W^\perp$, respectively.
A: Can you prove that if $W \leq V$ and $V$ finite dimensional, then $V = W \oplus W^{\perp}$?
Then we can apply the following theorem:
$dim(W_1) + dim(W_2) = dim(W_1+W_2) + dim(W_1 \cap W_2)$ for any $2$ subspaces $W_1,W_2 \leq V$
Now, because $W\cap W^{\perp} = \{\vec 0\}$, and hence $dim(W\cap W^{\perp}) = 0$, it would follow that $dim(V) = dim(W \oplus W^{\perp} ) = dim(W + W^{\perp}) = dim(W) + dim(W^{\perp})$
If I have to provide a proof of any of the results I used, please write a comment and I will edit my post.
EDIT: oops, I just saw that this post was 3 years old. 
A: I'll suppose $V$ is finite dimensional.
This is such a basic property that I will not assume known even that any (sub)space has an orthonormal basis; I'll prove that along the way. If $b_1,\ldots,b_k$ is any orthonormal system in $V$ ($b_i\cdot b_j=\delta_{i,j}$ for all $i,j$), then the map $V\to V$ given by $v\mapsto (b_1\cdot v)b_1+\cdots+(b_k\cdot v)b_k$ is a projection of $V$ onto the span of $b_1,\ldots,b_k$ (it is a linear map whose image is contained in that span, and it maps vectors of that span to themselves). Now in the subspace $W$ choose a maximal orthonormal system as follows: starting from the empty system, as long a $W$ contains any nonzero vector orthogonal to the orthonormal system so far, choose such a vector, normalise it, and add it too the system. The orthogonality condition means that each newly chosen vector lies in the kernel of the projection defined by the orthonormal system so far, and being nonzero it therefore does not lie in the span of that system; this ensures that the system remains linearly independent. Since $W$ is finite dimensional the process terminates.
Now let $p:V\to V$ denote the projection defined by the completed orthonormal system. Its restriction $p|_W$ to $W$ maps $W$ to a subspace of $W$, and the process having terminated means $\ker(p|_W)=\{0\}$. This means (by rank-nullity) that its image is all of $W$ (and being a projection, $p|_W$ is indeed the identity on$~W$), so our orthonormal system spans all of $W$. Thus we have found an orthonormal basis of$~W$.
The image of $p$ is $W$, so its rank is $\dim W$, and $\ker(p)=W^\perp$. Then the rank-nullity theorem for $p$ precisely says $\dim W+\dim W^\perp=\dim V$.
As a bonus you get that $W\cap W^\perp=\ker(p|_W)=\{0\}$, so $W+W^\perp$ is a direct sum, whose dimension is $\dim W+\dim W^\perp=\dim V$; this establishes $V=W\oplus W^\perp$.
