Relation between connection on vector bundle and Ehresmann connection on frame bundle I'll be using the conventions, notation and (numbered) results from Tu's Differential Geometry book.
Let $M$ be a smooth manifold, $E\to M$ a (real) vector bundle of rank $r$ with a connection $\nabla:\Gamma(E)\to\Omega^1(M)\otimes\Gamma(E)$. There is a way to obtain a connection on $E$ via the
Consider the frame bundle $\pi:\text{Fr}(E)\to M$ of $E$, which has an induced Ehresmann-connection $\omega\in\Omega^1(\text{Fr}(E),\text{Fr}(E)\times\mathfrak{gl}_r\mathbb R)$, and whose corresponding associated vector bundle $\text{Fr}(E)\times_1\mathbb R^k$ with respect to the identity representation $1:\text{GL}(r,\mathbb R)\to\text{GL}(r,\mathbb R)$ is canonically isomorphic to $E$.
Let's denote by $\Omega_1^k(\text{Fr}(E),\text{Fr}(E)\times\mathbb R^r)$ the $\mathbb R^r$-valued $k$-forms on the frame bundle which are right-invariant and horizontal, meaning that $r_g^*\omega=\omega$ and that $\omega$ vanishes as soon as an input vector is vertical. There is a covariant derivative
$$
D:\Omega_1^k(\text{Fr}(E),\text{Fr}(E)\times\mathbb R^r)\to \Omega_1^{k+1}(\text{Fr}(E),\text{Fr}(E)\times\mathbb R^r),\omega\mapsto (d\omega)^h,
$$
where $(d\omega)^h(v_1,\dots,v_{k+1})=dw(hv_1,\dots,hv_{k+1})$, where by $hv$ we mean the horizontal component of $v$. By Theorem 31.9 we have an identification
$$
\Omega_1^k(\text{Fr}(E),\text{Fr}(E)\times\mathfrak{gl}_r\mathbb R))\cong\Omega^k(M,\text{Fr}(E)\times_1\mathbb R^r),
$$
which means that the covariant derivative $D$ can be considered as a map
$$
\Omega^k(M)\otimes\Gamma(E)\to\Omega^{k+1}(M)\otimes\Gamma(E).
$$
My question is as follows:
I want to show that for $k=0$ this map corresponds to $\nabla$, but I'm not sure how to show this rigourously; due to the identifications made it is difficult for me to imagine how $D$ looks like as a map from $\Gamma(E)$ to $\Omega^1(M)\otimes\Gamma(E)$.
By Theorem 31.19 I know that for $\phi\in\Omega^0_1(\text{Fr}(E),\text{Fr}(E)\times\mathbb R^r)\cong\Gamma(\text{Fr}(E)\times\mathbb R^r)$ we have
$$
D\phi=d\phi+\omega\cdot\phi,
$$
where the action $\omega\cdot\phi$ is the natural action of $\omega\in\Omega^1(\text{Fr}(E))\otimes\Gamma(\text{Fr}(E)\times\mathfrak{gl}_r\mathbb R))$ on $\phi$. Note that the formula above looks a lot like the formula
$$
\nabla(f^i\sigma_i)=df^i\otimes\sigma_i+f^i\nabla\sigma_i=df^i\otimes\sigma+f^i\omega^j_i\otimes\sigma_j,
$$
where $\omega_\sigma=(\omega^i_j)$ is the connection matrix corresponding to the local frame $(\sigma_i)\subset\Gamma(E\vert_U)$. If we think of the local frame $(\sigma_i)$ as a section $\sigma\in\Gamma(\text{Fr}E\vert_U)$, then by Theorem 29.10 we have $\omega_\sigma=\sigma^*\omega$.
So I feel like I've got most of the ingredients, but I can't make it into a complete and formal argument.
Could someone help me out?
 A: Disclaimer: I've written everything out in painstaking detail, including explicit canonical isomorphisms, which definitely obscures the proof - but the point for me is to make it clear and explicit once and for all to avoid confusion later on.
The entire argument can be summarised by the following commutative diagram:

which arrises by looking locally $(U\subset M)$. The point to note is that the map
$$
\Gamma(U\times\mathbb R^r)\to\Omega^0_\rho(U\times\text{GL}_r\mathbb R,\mathbb R^r)
$$
in the diagram is the pull-back map $\pi^*$, and that the map
$$
\Omega^1_\rho(U\times\text{GL}_r\mathbb R,\mathbb R^r)\to \Omega^1(U)\otimes\Gamma(U\times\mathbb R^r)
$$
in the diagram is the pull-back $\sigma^*$ (where $\sigma\in\Gamma(\text{Fr}E\vert_U)$ is a local section we arrive at by choosing a local trivialisation).
Remark: Initially I wrote the text below without the diagram, and in the end I realised which diagram belongs to my proof. Since the diagram is very clear, I've put it first, but now comes the original text-based proof:
Choose a local trivialisation $\phi:E\vert_U\stackrel{\sim}{\to} U\times\mathbb R^r$, and write $\sigma_i=\Gamma(\phi)^{-1}(e_i)$ (where $\Gamma$ is the section functor). We have an induced trivialisation
$$
\Phi:\text{Fr}E\vert_U\stackrel{\sim}{\to} U\times\text{GL}_r\mathbb R,
$$
and we let $\sigma=\Gamma(\Phi)^{-1}(I)$, which means fiber-wise that $\sigma_p:e_i\mapsto\sigma_i\vert_p$. Our trivialisation induces an isomorphism between vector bundles:
$$
\text{Fr}E\vert_U\times_1\mathbb R^r\simeq(U\times\text{GL}_r\mathbb R)\times_1\mathbb R^r\cong U\times\mathbb R^r.
$$
Under these identifications, the inverse of the isomorphism in Theorem 31.9 is locally given given by the pull-back of the projection map $\pi^*$:
\begin{multline*}
\pi^*:\Omega^k(U)\otimes\Gamma(U\times\mathbb R^k)\stackrel{1\otimes\Gamma\phi^{-1}}{\longrightarrow}\Omega^k(U)\otimes\Gamma(\text{Fr}E\vert_U\times_1\mathbb R^k)\\
\stackrel{\pi^*}{\to}\Omega^k(\text{Fr}E\vert_U)\otimes\Gamma(\pi^*(\text{Fr}E\vert_U\times_1\mathbb R^k))\to
\Omega^k(\text{Fr}E\vert_U)\otimes\Gamma(\text{Fr}E\vert_U\times\mathbb R^k).
\end{multline*}
We can verify explicitly that the map above on the sections sends $e_i$ indeed to its pull-back $\pi^*e_i=e_i\in\Gamma(U\times\mathbb R^r)$:
\begin{gather*}
\Gamma(U\times\mathbb R^r)\simeq\Gamma(\text{Fr}E\vert_U\times_1\mathbb R^r)\to\Gamma(\pi^*(\text{Fr}E\vert_U\times_1\mathbb R^r))\cong\Gamma(\text{Fr}E\vert_U\times\mathbb R^r)\\
(p\mapsto (p,e_i))\mapsto (p\mapsto [\sigma_p,e_i])\mapsto (\tau_p\mapsto (\tau_p,[\sigma_p,e_i]))\mapsto(\tau_p\mapsto (\tau_p,e_i)).
\end{gather*}
Write
$$
\omega=\sum\tilde\omega^i_j\otimes e^i_j\in\Omega^1(\text{Fr}E\vert_U)\otimes\Gamma(\text{Fr}E\vert_U\times\mathfrak{gl}_r\mathbb R),
$$
for the restricted connection form $\text{Fr}E\vert_U$, and write
$$
\omega_\sigma=\sum\omega^i_j\otimes e^i_j\in\Omega^1(U)\otimes\Gamma(U\times\mathfrak{gl}_r\mathbb R)
$$
for the local connection form of relative to the frame $\sigma$, meaning that $\nabla\sigma_i=\omega^j_i\sigma_j$. Since $\sigma^*\omega=\omega_\sigma$ we have $\sigma^*\tilde\omega^i_j=\omega^i_j$. Note that
$$
\omega\cdot e_i=\tilde\omega^j_i e_j,
$$
while $d(e_i)=0$, so
$$
D(e_i)=d(e_i)+\omega\cdot e_i=\tilde\omega^j_i e_j
$$
To go back to $\Omega^1(U)\otimes\Gamma(U\times\mathbb R^r)$, we simply need to pull back along $\sigma$ to obtain $\sigma^*\omega^j_i e_j=\omega^j_i e_j$;  because $\sigma$ corresponds to the trivial section of $\text{Fr}E\vert_U\simeq(U\times\text{GL}_r\mathbb R))$ and by the naturality of $\omega\mapsto\omega^\flat$ we may apply the lemma below.
Lemma.
Let $P=M\times G\to M$ be a trivial principal $G$ bundle, $\rho:G\to\text{GL}(V)$ a representation. Denote by $\phi:P\times_\rho V\cong M\times V,[(x,g),v]\mapsto (x,v)$ the identification with the trivial bundle. Let $\sigma:M\to P,m\mapsto (m,e)$ be the canonical section of the trivial bundle. Then the isomorphism $\omega\mapsto\omega^\flat$ in Theorem 31.9 under our identification with the trivial bundle is given by the pull-back under $\sigma$:
$$
\sigma^*:\Omega^k_\rho(P,P\times V)\stackrel{(-)^\flat}{\to} \Omega^k(M)\otimes\Gamma(P\times_\rho V)\stackrel{\phi}{\to}\Omega^k(M)\otimes\Gamma(M\times V).
$$
Proof.
Let $\omega\in\Omega^k_\rho(P,P\times V)$. Write
$$
\omega_p(v_1,\dots,v_k)=(p,\overline\omega_p(v_1,\dots,v_k))\in\{p\}\times V.
$$
Then
\begin{align*}
\phi\omega^\flat_x(v_1,\dots,v_k)&=\phi[\omega_{\sigma(x)}(T_x\sigma v_1,\dots,T_x\sigma v_k)]=\phi[\omega_{(x,e)}(T_x\sigma v_1,\dots, T_x\sigma v_k)]\\
&=\phi[(x,e),\overline\omega_{(x,e)}(T_x\sigma v_1,\dots, T_x\sigma v_k)]=(x,\sigma^*\overline\omega_x(v_1,\dots,v_k)).
\end{align*}
$\tag{$\square$}$
So we see that our induced map sends $\sigma_i$ to $\omega^j_i\sigma_j=\nabla\sigma_i$. Since we also have the Leibniz condition, it follows that our induced map corresponds to the original connection $\nabla$.
