Proof of Gauss-Markov Theorem: Unaccountable Line I'm trying to follow Faraway's proof of the Gauss-Markov model in his book Linear Models with R, 2nd Ed., on pages 22-23, but I have been having numerous difficulties. The latest difficulty is thick in the weeds, so I will type out his proof exactly.

Suppose $E\varepsilon=0$ and $\operatorname{var}\varepsilon=\sigma^2I.$ Suppose also
that the structural part of the model, $EY=X\beta$ is correct. (Clearly these are big
assumptions and so we will address the implications of this later.) Let
$\psi=c^T\beta$ be an estimable function; then the Gauss-Markov theorem states that
in the class of all unbiased linear estimates of $\psi,\; \hat\psi=c^T\hat\beta$ has the
minimum variance and is unique.
We prove this theorem.
Suppose $a^Ty$ is some unbiased estimate of $c^T\beta$ so that:
\begin{align*} Ea^Ty&=c^T\beta\qquad\forall\beta\\
  a^TX\beta&=c^T\beta\qquad\forall\beta \end{align*} which means that
$a^TX=c^T.$ This implies that $c$ must be in the range space of $X^T$ [$X^Ta=c$, ACK]
which in turn implies that $c$ is also in the range space of $X^TX$
which means there exists a $\lambda$ such that $c=X^TX\lambda$ so:
$$c^T\hat\beta=\lambda^TX^TX\hat\beta=\lambda^TX^Ty$$ Now we can show
that the least squares estimator has the minimum variance - pick an
arbitrary estimate $a^Ty$ and compute its variance: \begin{align*}
  \operatorname{var}\!\left(a^Ty\right)
  &=\operatorname{var}\!\left(a^Ty-c^T\hat\beta+c^T\hat\beta\right)\\
  &=\operatorname{var}\!\left(a^Ty-\lambda^TX^Ty+c^T\hat\beta\right)\\
  &=\operatorname{var}\!\left(a^Ty-\lambda^TX^Ty\right) 
  +\operatorname{var}\!\left(c^T\hat\beta\right)  +2\operatorname{cov}\!\left(a^Ty-\lambda^TX^Ty,\lambda^TX^Ty\right) \end{align*} but
$$\operatorname{cov}\!\left(a^Ty-\lambda^TX^Ty,\lambda^TX^Ty\right)
  =\left(a^T-\lambda^TX^T\right)\sigma^2IX\lambda \\ \dots$$

My Question: The rest of the proof is very straight-forward, but: where did that last line come from? I'm just astonished at how many skipped steps that has to represent, and I am rather of the opinion that the rest of the steps in that section are trivial compared with this "and-then-a-miracle-occurred" kind of step.
As a general comment: I have searched through many proofs of the Gauss-Markov theorem. Why are the proofs so universally opaque? Is there a step-by-step proof of the Gauss-Markov theorem that does not assume too much of the reader?

They are omitting some algebraic manipulations which use some properties of covariance described here (this is the citation linked on wikipedia for these properties):
https://www.statlect.com/fundamentals-of-probability/covariance-matrix#hid9
$$\mathrm{cov}(a^Ty - \lambda^TX^Ty, \lambda^TX^Ty) = (a^T- \lambda^TX^T)\mathrm{cov}(y, \lambda^TX^Ty).$$
Here we are pulling out a constant factor from the left argument of $\mathrm{cov}$.
$$ = (a^T - \lambda^TX^T)\mathrm{cov}(y, y)X\lambda$$
Here we are pulling out a constant factor from the right argument of $\mathrm{cov}$ (but the right argument must be transposed when we do so).
Now we are left with the covariance matrix of the vector $y$. By assumption, $y_i$ and $y_j$ are uncorrelated for $i \neq j$ (this is independence of observations). So this is a diagonal matrix. And again by assumption, $\mathrm{var}(y_i) = \mathrm{var}(y_j) = \sigma^2$ for all $i, j$. This is homoskedasticity. So finally, you are left with the equality in the proof.
On the opacity of the proof: I think it is just about familiarity with properties of covariance and matrix algebra. I also found the Gauss Markov proof really hard to follow (the proof in Elements of Statistical Learning is not easier to read). But once you see it and understand the rules for covariance of linear transformations, I think it becomes easy to see why an author might omit those steps.
For many people, regression models are now their first introduction to statistics beyond combinatorics and simple probability theory, so it's natural to dive into a proof like this. But many texts are written assuming the reader is following a statistics curriculum which includes, I assume, a prerequisite course where you prove these kinds of properties and drill them in homework exercises. It may not have occurred to authors that there are people doing things "out of order" for whom the Gauss Markov theorem is very interesting, but who haven't become very familiar with these sorts of manipulations.
