Solution (source code)

= Solution

Assume $V_{YY}$ is invertible. Put
$$
R=X-\mu_X-V_{XY}V_{YY}^{-1}(Y-\mu_Y).
$$
This and $Y$ are jointly <multivariate normal>, with $\operatorname{Cov}(R,Y)=0$ and $\operatorname{Cov}(R)=V_{XX}-V_{XY}V_{YY}^{-1}V_{YX}$. Their joint Gaussian <characteristic function> factors when the cross covariance vanishes, so they are independent. Conditioning on $Y=y$ therefore leaves the law of $R$ unchanged, proving
$$
\boxed{X\mid Y=y\sim N(\mu_X+V_{XY}V_{YY}^{-1}(y-\mu_Y),\ V_{XX}-V_{XY}V_{YY}^{-1}V_{YX})}.
$$