[proofplan]
We define $\nabla^E$ by horizontally differentiating the equivariant function corresponding to a section of the associated bundle. The main point is to prove that the resulting class in $P\times_G V$ is independent of the chosen point in the principal fibre; this follows from $G$-equivariance of the principal connection and of the function $f_s$. We then verify smoothness locally, prove linearity and the Leibniz rule for a covariant derivative, and finally observe that the displayed formula determines the operator uniquely.
[/proofplan]
[step:Define the operator by horizontal differentiation]
Let $\pi:P\to M$ denote the smooth principal bundle projection. We use the standard section-equivariant-function correspondence for associated bundles: a section $s\in\Gamma(E)$ determines the smooth $\rho$-equivariant map $f_s:P\to V$ by the condition $s(\pi(p))=[p,f_s(p)]$, and conversely every smooth map $f:P\to V$ satisfying $f(pg)=\rho(g^{-1})f(p)$ determines a section of $E=P\times_G V$.
For $s\in\Gamma(E)$, define a candidate $E$-valued one-form
\begin{align*}
\nabla^E s:M\to T^*M\otimes E
\end{align*}
as follows. Let $x\in M$, let $X\in T_xM$, and choose $p\in P_x$. Since $\omega$ is a principal connection, the horizontal subspace $H_pP:=\ker \omega_p\subset T_pP$ satisfies that the restriction
\begin{align*}
d\pi_p|_{H_pP}:H_pP\to T_xM
\end{align*}
is a linear isomorphism. Let $\widetilde X_p\in H_pP$ denote the horizontal lift of $X$, namely the unique vector satisfying $d\pi_p(\widetilde X_p)=X$. Set
\begin{align*}
(\nabla^E s)_x(X):=[p,df_s|_p(\widetilde X_p)].
\end{align*}
This defines a value in the fibre $E_x=P_x\times_G V$, once independence of the chosen point $p\in P_x$ is proved.
[/step]
[step:Prove independence of the chosen point in the principal fibre]
Let $g\in G$ and replace $p$ by $pg$. Define the right action map $R_g:P\to P$ by $R_g(q)=qg$. Because $\omega$ is a principal connection, its defining right-equivariance property gives $R_g^*\omega=\operatorname{Ad}_{g^{-1}}\omega$. Hence $v\in\ker\omega_p$ implies $\omega_{pg}(d(R_g)_p v)=\operatorname{Ad}_{g^{-1}}(\omega_p(v))=0$, so the horizontal distribution is right $G$-invariant:
\begin{align*}
d(R_g)_p(H_pP)=H_{pg}P.
\end{align*}
Moreover $\pi\circ R_g=\pi$, hence
\begin{align*}
d\pi_{pg}(d(R_g)_p\widetilde X_p)=d\pi_p(\widetilde X_p)=X.
\end{align*}
By uniqueness of horizontal lifts,
\begin{align*}
\widetilde X_{pg}=d(R_g)_p\widetilde X_p.
\end{align*}
The equivariance identity for $f_s$ is
\begin{align*}
f_s\circ R_g=\rho(g^{-1})\circ f_s.
\end{align*}
Differentiating this identity at $p$ and applying it to $\widetilde X_p$ gives
\begin{align*}
df_s|_{pg}(d(R_g)_p\widetilde X_p)=\rho(g^{-1})df_s|_p(\widetilde X_p).
\end{align*}
Therefore
\begin{align*}
[pg,df_s|_{pg}(\widetilde X_{pg})]=[pg,\rho(g^{-1})df_s|_p(\widetilde X_p)]=[p,df_s|_p(\widetilde X_p)].
\end{align*}
Thus the definition is independent of the representative $p\in P_x$.
[guided]
We must check the only possible ambiguity in the formula: the fibre $P_x$ has many points, and any two are related by the principal right action. Let $p\in P_x$ and $g\in G$, so the other representative is $pg$. Define the right action map $R_g:P\to P$ by $R_g(q)=qg$.
The horizontal lift also changes in a controlled way. Since $\omega$ is a principal connection, its defining right-equivariance property gives $R_g^*\omega=\operatorname{Ad}_{g^{-1}}\omega$. Thus, if $v\in H_pP=\ker\omega_p$, then $\omega_{pg}(d(R_g)_p v)=\operatorname{Ad}_{g^{-1}}(\omega_p(v))=0$, so the horizontal subspaces are invariant under the right action:
\begin{align*}
d(R_g)_p(H_pP)=H_{pg}P.
\end{align*}
Because $\pi\circ R_g=\pi$, applying $d\pi$ to $d(R_g)_p\widetilde X_p$ gives
\begin{align*}
d\pi_{pg}(d(R_g)_p\widetilde X_p)=d\pi_p(\widetilde X_p)=X.
\end{align*}
So $d(R_g)_p\widetilde X_p$ is horizontal at $pg$ and projects to $X$. By uniqueness of horizontal lifts at $pg$,
\begin{align*}
\widetilde X_{pg}=d(R_g)_p\widetilde X_p.
\end{align*}
Now we compare the differentiated equivariant functions. The equivariance of $f_s:P\to V$ says
\begin{align*}
f_s(pg)=\rho(g^{-1})f_s(p)
\end{align*}
for every $p\in P$. Equivalently, as maps $P\to V$,
\begin{align*}
f_s\circ R_g=\rho(g^{-1})\circ f_s.
\end{align*}
Differentiating this identity at $p$ in the direction $\widetilde X_p$ gives
\begin{align*}
df_s|_{pg}(d(R_g)_p\widetilde X_p)=\rho(g^{-1})df_s|_p(\widetilde X_p),
\end{align*}
because $\rho(g^{-1}):V\to V$ is a [linear map](/page/Linear%20Map), so its derivative is itself. Combining this with the transformation rule for the horizontal lift gives
\begin{align*}
df_s|_{pg}(\widetilde X_{pg})=\rho(g^{-1})df_s|_p(\widetilde X_p).
\end{align*}
Finally, the associated vector bundle relation identifies
\begin{align*}
(pg,\rho(g^{-1})v)\sim(p,v)
\end{align*}
for every $v\in V$. Taking $v=df_s|_p(\widetilde X_p)$ proves
\begin{align*}
[pg,df_s|_{pg}(\widetilde X_{pg})]=[p,df_s|_p(\widetilde X_p)].
\end{align*}
Thus the formula does not depend on which point of the principal fibre is used.
[/guided]
[/step]
[step:Verify fibrewise linearity in the tangent vector]
Fix $s\in\Gamma(E)$ and $x\in M$. Let $X,Y\in T_xM$ and let $a,b\in\mathbb R$. Choose $p\in P_x$. Since $d\pi_p|_{H_pP}:H_pP\to T_xM$ is a linear isomorphism, the horizontal lift of $aX+bY$ is
\begin{align*}
a\widetilde X_p+b\widetilde Y_p.
\end{align*}
By linearity of the differential $df_s|_p:T_pP\to V$,
\begin{align*}
df_s|_p(a\widetilde X_p+b\widetilde Y_p)=a\,df_s|_p(\widetilde X_p)+b\,df_s|_p(\widetilde Y_p).
\end{align*}
The vector-space structure on $E_x=P_x\times_G V$ is induced from the vector-space structure on $V$, so
\begin{align*}
(\nabla^E s)_x(aX+bY)=a(\nabla^E s)_x(X)+b(\nabla^E s)_x(Y).
\end{align*}
Hence $(\nabla^E s)_x\in T_x^*M\otimes E_x$.
[/step]
[step:Check smoothness in a local trivialisation]
Let $U\subset M$ be an [open set](/page/Open%20Set) admitting a smooth local section
\begin{align*}
\sigma:U\to P.
\end{align*}
Let
\begin{align*}
u:U\to V
\end{align*}
be the local representative of $s$, defined by $u(x)=f_s(\sigma(x))$, so that $s(x)=[\sigma(x),u(x)]$. Let
\begin{align*}
A:=\sigma^*\omega\in\Omega^1(U;\mathfrak g)
\end{align*}
be the local connection form, and let
\begin{align*}
d\rho_e:\mathfrak g\to\mathfrak{gl}(V)
\end{align*}
be the infinitesimal representation. For $X\in T_xM$, define $\xi:=A_x(X)\in\mathfrak g$. Let
\begin{align*}
\exp:\mathfrak g\to G
\end{align*}
denote the Lie-group exponential map, and let $\xi_P\in\Gamma(TP)$ be the fundamental vector field defined by
\begin{align*}
\xi_P(p)=\frac{d}{dt}\big|_{t=0}p\exp(t\xi)
\end{align*}
for $p\in P$. We claim that the horizontal lift at $\sigma(x)$ is
\begin{align*}
d\sigma_x(X)-\xi_P(\sigma(x)).
\end{align*}
Let $\operatorname{id}_U:U\to U$ denote the identity map on $U$. Indeed, since $\pi\circ\sigma=\operatorname{id}_U$ and $\pi(\sigma(x)\exp(t\xi))=x$, we have
\begin{align*}
d\pi_{\sigma(x)}(d\sigma_x(X)-\xi_P(\sigma(x)))=X.
\end{align*}
Also, by definition of $A=\sigma^*\omega$ and by the normalization axiom in the definition of a principal connection, namely $\omega_p(\eta_P(p))=\eta$ for every $\eta\in\mathfrak g$ and $p\in P$,
\begin{align*}
\omega_{\sigma(x)}(d\sigma_x(X)-\xi_P(\sigma(x)))=A_x(X)-\xi=0.
\end{align*}
Thus this vector lies in $H_{\sigma(x)}P$ and projects to $X$, so it is the horizontal lift. Differentiating $f_s(\sigma(x)\exp(t\xi))=\rho(\exp(-t\xi))u(x)$ at $t=0$ gives
\begin{align*}
df_s|_{\sigma(x)}(\xi_P(\sigma(x)))=-d\rho_e(\xi)u(x).
\end{align*}
Therefore
\begin{align*}
df_s|_{\sigma(x)}(d\sigma_x(X)-\xi_P(\sigma(x)))=du_x(X)+d\rho_e(A_x(X))u(x).
\end{align*}
In the trivialisation $E|_U\cong U\times V$ induced by $\sigma$, the local expression for $\nabla^E s$ is thus
\begin{align*}
(\nabla^E s)_x(X)=\left[\sigma(x),du_x(X)+d\rho_e(A_x(X))u(x)\right].
\end{align*}
The maps $u$, $A$, and $d\rho_e$ are smooth, so this expression is smooth in $x$ and linear in $X$. Hence $\nabla^E s\in\Omega^1(M;E)$.
[/step]
[step:Verify additivity over sections and the Leibniz rule]
Let $s,t\in\Gamma(E)$ and $a,b\in\mathbb R$. The equivariant function corresponding to $as+bt$ is the map $f_{as+bt}:P\to V$ defined by $f_{as+bt}(p)=a f_s(p)+b f_t(p)$. For every $x\in M$, $X\in T_xM$, and $p\in P_x$, linearity of the differential gives
\begin{align*}
(\nabla^E(as+bt))_x(X)=a(\nabla^E s)_x(X)+b(\nabla^E t)_x(X).
\end{align*}
Now let
\begin{align*}
h:M\to\mathbb R
\end{align*}
be a smooth function. The equivariant function corresponding to $hs$ is the map $f_{hs}:P\to V$ defined by $f_{hs}(p)=h(\pi(p))f_s(p)$. For $p\in P_x$ and the horizontal lift $\widetilde X_p\in H_pP$, the product rule gives
\begin{align*}
df_{hs}|_p(\widetilde X_p)=d(h\circ\pi)_p(\widetilde X_p)f_s(p)+h(x)df_s|_p(\widetilde X_p).
\end{align*}
Since $d\pi_p(\widetilde X_p)=X$,
\begin{align*}
d(h\circ\pi)_p(\widetilde X_p)=dh_x(X).
\end{align*}
Thus
\begin{align*}
(\nabla^E(hs))_x(X)=dh_x(X)s(x)+h(x)(\nabla^E s)_x(X).
\end{align*}
So $\nabla^E$ is a covariant derivative on $E$.
[/step]
[step:Prove uniqueness from the horizontal lift formula]
Let
\begin{align*}
D:\Gamma(E)\to\Omega^1(M;E)
\end{align*}
be any covariant derivative satisfying the stated horizontal differentiation formula. For each $s\in\Gamma(E)$, $x\in M$, and $X\in T_xM$, choose any $p\in P_x$. The connection determines a unique horizontal lift $\widetilde X_p\in H_pP$, so the formula forces
\begin{align*}
(Ds)_x(X)=[p,df_s|_p(\widetilde X_p)].
\end{align*}
The right-hand side is exactly the value assigned by $\nabla^E$. Hence $Ds=\nabla^E s$ for every $s\in\Gamma(E)$, and therefore $D=\nabla^E$. This proves uniqueness and completes the construction of the induced covariant derivative.
[/step]
