Proof of the differential Bianchi identity

Here is another proof. The covariant derivatives satisfy the Jacobi identity $$ [nabla_mu,[nabla_nu,nabla_kappa]]+ [nabla_nu,[nabla_kappa,nabla_mu]]+[nabla_kappa,[nabla_mu,nabla_nu]]=0. $$ This can be verified directly, but it is also known that pretty much any associative algebra will satisfy the Jacobi identity, and the elements $nabla_1,...,nabla_n$ basically generate a formal associative algebra.

Then letting the Jacobi identity act on any vector field $X^rho$ we get for one of the terms $$ [nabla_kappa,[nabla_mu,nabla_nu]]X^rho=nabla_kappa[nabla_mu,nabla_nu]X^rho-[nabla_mu,nabla_nu]nabla_kappa X^rho=nabla_kappa(R^rho_{ sigmamunu}X^sigma)-R^rho_{ sigmamunu}nabla_kappa X^sigma + R^sigma_{ kappamunu}nabla_sigma X^rho =nabla_kappa R^rho_{ sigmamunu}X^sigma+R^rho_{ sigmamunu}nabla_kappa X^sigma-R^rho_{ sigmamunu}nabla_kappa X^sigma+R^sigma_{ kappamunu}nabla_sigma X^rho = nabla_kappa R^rho_{ sigmamunu}X^sigma+R^sigma_{ kappamunu}nabla_sigma X^rho. $$

Now writing this into the Jacobi identity gives $$ 0=left[nabla_kappa R^rho_{ sigmamunu}+text{ cyclic permutations on }kappa,mu,nuright] X^sigma+left[R^sigma_{ kappamunu}+text{ cyclic permutations}right]nabla_sigma X^rho. $$

The second term here vanishes identically because of the algebraic Bianchi identity (cyclic identity), and what we are left with is the differential Bianchi identity.

Alternatively, this can be taken to be a proof of both the differential and algebraic Bianchi identity, since at any point $x$ one may take $$ X^sigma(x)=delta^sigma_alpha,quad nabla_sigma X^rho(x)=0, $$ which gives the differential Bianchi identity, and take $$ X^sigma(x)=0,quad nabla_sigma X^rho(x)=delta^rho_sigma, $$ which gives the algebraic Bianchi identity.

In this proof I have assumed torsionlessness, but the generalization to the torsionful case is similar, though more laborous.