I do seek a formal proof for the following statement.
Let $V$ be a vector space such that $dimV=n$, let $S⊂V$ and let $v_1,…,v_r$ be a basis for $S$, then $S^⊥$ has $n-r$ linearly independepent vectors.
$$.$$Here I present my proof which is not quite formal.
$$.$$ Since $dimV=n$, then $V$ has $n$ linearly independent vectors, by the Rank-nullity theorem:
$$dimV=dimS+dimS^⊥$$
Furthermore, each element of $S$ is orthogonal to every element of $S^⊥$, then it follows that the set $S+S^⊥$ is linearly independent and thus constitute a basis for $V$. Now, the dimension of $V$ equals the number of linearly independent vectors in that space which is $n$, the basis of $S$ has $r$ linearly independent vectors and hence its dimension is $r$, using the Rank=Nullity theorem we get:
$$n-r=dimS^⊥$$
Similarly I proved the Rank-Nullity theorem by establishing a linear map on some vector space and etc. I would be very glad if you could share a more rigorous proof of this statement which I find quite interesting, thanks for your time.
Best Answer
By the way, once you establish the equation \begin{equation} \dim V = \dim S + \dim S^{\perp} \end{equation} or equivalently, \begin{align} \dim S^{\perp} &= \dim V - \dim S \\ &= n - r \end{align} there isn't much more to explain; the proof is complete at this point.
To establish this equality, what I'd do is show that we have a direct sum decomposition $V = S \oplus S^{\perp}$, which means $S \cap S^{\perp} = \{ 0\}$ and for every $v \in V$, there exist $x \in S$ and $y \in S^{\perp}$ such that $v = x+y$. This is useful, because whenever there is such a direct sum decomposition, if $\beta_S$ is a basis for $S$ and $\beta_{S^{\perp}}$ is a basis for $S^{\perp}$, then their union $\beta_S \cup \beta_{S^{\perp}}$ will be a basis for $V$ (if this isn't obvious to you, you should attempt a proof). In particular, $\beta_S$ and $\beta_{S^{\perp}}$ are disjoint, thereby giving the equality \begin{equation} \dim V = |\beta_S \cup \beta_{S^{\perp}}| = |\beta_S| + |\beta_{S^{\perp}}| = \dim S + \dim S^{\perp} \end{equation}