I am studying the proof of Gilbert-Varshamov Bound from Xing's Book "Coding Theory" and I find it quite dense. I searched it a little bit and I found this useful post in MSE. Then, I tried to prove it on my own and elaborate more:
Theorem. (Gilbert-Varshamov Bound) Let $q\in \Bbb Z_{\geq 2}$ be a prime power and $n,d\in \Bbb Z^+$ be positive integers such that $d\in \{2,\dots,n\}$, $k\in \{1,\dots,n\}$. If $$V_q^{n-1}(d-2)<q^{n-k},$$ then there exists a linear $[n,k]$-code $C\leq \Bbb F_q^n$ over $ \Bbb F_q$ with minimum distance at least $d$.
Proof.
We pick $m$ distinct non-zero vectors $$v_1,\dots,v_m\in \ \Bbb F_q^{n-k}\setminus\{0\},$$ where $m\leq n-1$.
Goal: We want to pick a $c_j$ which is not in the linear span of $d-2$ or fewer vectors from $\{c_1,\dots,c_{j-1}\}$.
Take $i\in \{1,\dots,m\}$ of them: $\{v_{j_1},\dots,v_{j_i}\}\subseteq \{v_1,\dots,v_m\}$. Then, the number of linear combinations \begin{align*} a_1v_{j_1}+\dotsb+a_iv_{j_i},\quad \text{with } (a_1,\dots,a_i)\neq (0,\dots,0) \tag{$*$} \end{align*} that we can construct is $(q-1)^i$. Moreover, the number of the linear combinations of this form, for any possible choice of these $i$ vectors of $v_1,\dots,v_m$, is $$(q-1)^i\cdot \binom{m}{i}.$$ Then, for $i=1,2,\dots,r$ where $r\leq \min \{d-2,m\}$, the number of all the linear combinations of the form $(*)$, that is the linear combinations of $m$ non-zero vectors with non-zero coefficients, that we can construct are \begin{align*} \sum_{i=1}^r \binom{m}{i}(q-1)^i\leq \sum_{i=1}^{d-2}\binom{n-1}{i}(q-1)^i \lneqq q^{n-k}-1=|\Bbb F_q^{n-k}\setminus\{0\}|. \tag{$**$} \end{align*} So, say $S:=\{\text{all the linear combinations of the form $(*)$},\ \forall i=1,2,\dots,r\leq \min \{d-2,m\}\}\subseteq \Bbb F_q^{n-k}\setminus\{0\}$. Hence, by $(**)$, $S\subsetneqq\Bbb F_q^{n-k}\setminus\{0\}$. This tells us, that there is a non-zero vector of $\Bbb F_q^{n-k}$, which is not a linear combination of any choice of $i\in \{1,\dots,r\}$ vectors of $v_1,\dots,v_m$. Therefore, there is a non-zero vector of $\Bbb F_q^{n-k}$, that doesn't belong to any of the vector spaces $\mathrm{Span}\{v_{j_1},\dots,v_{j_i}\}$ that are spanned by any choice of the $i\in \{1,\dots,r\}$ vectors of $v_1,\dots,v_m$.
Now, we will use the result we proved above, in order to construct an $(n-k)\times n$ matrix $H\in M_{(n-k)\times n}(\Bbb F_q)$ such that any $d-1$ columns are linearly independent.
We choose a basis $S_1,\dots,S_{n-k}\in\Bbb F_q^{n-k}$ of $\Bbb F_q^{n-k}$. With these vectors we fill the first $n-k$ columns of $H$.
Subsequently we pick a vector $S_{n-k+1}\in \Bbb F_q^{n-k}$ for the $n-k+1$ column of $H$, such that it doesn't belong to any vector subspace that is spanned of any choice of $i\in\{1,\dots,d-2\}$ vectors of $S_1,\dots,S_{n-k}$. Therefore, $$S_{n-k+1}\notin \mathrm{Span}\{S_{j_1},\dots,S_{j_{d-2}}\},$$ where $\{j_1,\dots,j_{d-2}\}\subseteq\{1,\dots,n-k\}$. Note that we are sure that there always exists such a vector, by the result we proved before. Hence, any such choice of the $S_{j_1},\dots,S_{j_{d-2}},S_{n-k+1}$, forms a linearly independent set. So, any choice of $d-1$ columns of them are linearly independent.
We work likewise for any column of $H$, until we fill the whole matrix.
So, any $d-1$ columns of $H$ are linearly independent.
Lastly, we form the linear code $$C=\{x\in \Bbb F_q^n:Hx^\mathrm{T}=0\}\leq \Bbb F_q^n.$$ Then, $H$ is a parity check matrix for $C$ and since every $d-1$ columns of $C$ are linearly independent, $\mathrm{d}(C)\geq d$, as required. $\quad \square$
Questions.
1) Is my proof complete and correct?
2) Is there any othere source (book/notes/article) where I could find this proof written in more detail?
Thank you.