Exterior covariant derivative on associated bundle Let $(P,\pi,M;G)$ be a principal fibre bundle over $M$ with connection $1$-form $A:TP\rightarrow \mathfrak{g}$. Let $\rho:G\rightarrow V$ be a representation. The connection $A$ now induces a covariant derivative as well as an exterior covariant derivative on every associated bundle $E:=P\times_G V$ over $M$.
Explicitly one can identify the tensorial $k$-forms of type $\rho$ on $P$ with values in $V$ with the $k$-forms on $M$ with values in the associated bundle: $\Lambda^k_{EH}(P,V)\cong\Lambda^k(M,V)$. On the first one gets the exterior differential $D^A$ by
$$D^A(\omega)(V_0,\ldots,V_k)=d\omega(\text{pr}_H(V_1),\ldots,\text{pr}_H(V_k)) \quad \omega\in\Lambda^k_\text{EH}(P,V).$$
Therefore one gets by identification an exterior covariant differential $d_A$ on $P\times_G V$. Explicitly written one gets
$$(d_A\eta)_x(w_0,\ldots,w_k)=[p,(d\overline{\eta})_p(w^*_0,\ldots,w^*_k)]$$
where $p\in P$ is a point with $\pi(p)=x$, the $w_i^*\in T_pP$ are the horizontal lifts of $w_i\in T_xM$ and $\overline{\eta}\in\Lambda^k_\text{EH}(P,V)$ is the corresponding $k$-form of $\eta\in\Lambda^k(M,P\times_G V)$. (Restriction on the $0$-forms gives a connection $\nabla$ on $P\times_G V$).
On the other hand one can define an exterior covariant derivative relative to some connection $\nabla:TM\times E\rightarrow E$ on a vector bundle $E\rightarrow M$ over $M$ by the following formula
$$
(d_\nabla\omega)(V_1,\dots,V_k)=\sum_{i=1}^k (-1)^i\nabla_{V_i}(\omega(V_1,\dots,\hat{V_i},\dots,V_k))+\sum_{i<j}^k (-1)^{i+j}\omega([V_i,V_j],V_1,\dots,\hat{V_i},\dots,\hat{V_j},\dots,V_k) \\
\omega\in\Lambda^k(M,E).
$$
Does someone know a proof, that these definitions on asociated bundles lead to the same exterior covariant differential $d_\nabla$? I think its not obvious, especially if you write out the definition of the first one in terms of the differential $D^A=d\circ\text{pr}_H$.
I'd be thanfull for every help. Also some reference. Most authors just consider vector bundles in terms of associated bundles and simply define $d_\nabla$ as the induced one.
 A: I think that, in the end, you just have to compute it. Depending on which intermediate results you have available that can become rather nasty. But that is generally a thing in differential geometry, the nicer and (lets say) cleaner a theory/formalism is, the more effort you have to put in to break it down to coordinate/more explicit expressions. "The nicer the front-end, the uglier the back-end".
However, a useful intermediate step may be the Leibniz rule for the exterior (covariant) derivative. Some authors also proceed as follows.
Let $E\to M$ be a vector bundle and $\nabla:\Omega^0(M;E)\to\Omega^1(M;E)$ be a covariant derivative on it. Here $\Omega^k(M;E)$ denotes the $k$-forms on $M$ with values in $E$, in particular, $\Gamma(E)=\Omega^0(M;E)$ and $\Gamma(T^*M\otimes E)=\Omega^1(M;E)$. Then you can show that there exists a unique map
$$
\widehat{\nabla}:\Omega^1(M;E)\to\Omega^2(M;E)
$$
such that
$$
\widehat{\nabla}(f\cdot \omega)=\text{d}f\wedge\omega+f\cdot\widehat{\nabla}\omega
$$
for all $f\in\mathcal{C}^\infty(M)$, $\omega\in\Omega^1(M;E)$ and that
$$
\widehat{\nabla}(\nu\otimes s)=\text{d}\nu\otimes s-\nu\wedge\nabla s
$$
for all $\nu\in\Omega^1(M)$, $s\in\Gamma(E)$.
The first Leibniz rule says that $\widehat{\nabla}$ is a derivation itself and the second distinguishes $\widehat{\nabla}$ as a continuation of $\nabla$. Note that before you need to make sense of the wedge-product $\Omega^1(M)\times\Omega^1(M;E)\to\Omega^2(M;E)$ and note that any section in $T^*M\otimes E$ is locally representable as a finite linear combination of forms like $\nu\otimes s$.
Existence is proven by giving your formula and I guess uniqueness should not be too difficult. You can generalize the Leibniz rules appropriately to obtain maps $\nabla^{(k)}:\Omega^k(M;E)\to\Omega^{k+1}(M;E)$ (with a "(-1) to some power"-factor, just as with the usual $\text{d}$ and $\wedge$).
From the other perspective, given a principal $G$-bundle $P\to M$ with a connection form $\mathcal{A}$ and a representation $\rho:G\to\text{GL}(V)$ on some $V$, you can show that the exterior covariant derivative $\text{d}^\mathcal{A}:\Omega^k(M,P\times_\rho V)\to\Omega^{k+1}(M,P\times_\rho V)$ admits the Leibniz rule
$$
\text{d}^{(\mathcal{A})}(\eta\wedge\omega)=\text{d}\eta\wedge\omega+(-1)^l\eta\wedge\text{d}^{(\mathcal{A})}\omega
$$
for all $\eta\in\Omega^l(M)$, $\omega\in\Omega^k(M;P\times_\rho V)$. With the uniqueness from above, that consequently gives back for $\text{d}^{(\mathcal{A})}$ your formula. Proving this Leibniz rule, as mentioned in the beginning, can get nasty, depending on how far the theory is developed in the forehand.
If you speak German I can refer to you a German textbook (H. Baum - Eichfeldtheorie, basically Section 3.4), but I'm sure many other books prove this formula as well.
