[proofplan]
The proof is to show that the two pieces of data encode the same vertical projection. First, a principal connection gives a splitting of each tangent space into horizontal and vertical parts, and the principal action identifies each vertical tangent space with the Lie algebra $\mathfrak g$; composing the vertical projection with this identification gives a connection form. Conversely, a connection form has kernel complementary to the vertical tangent space because it reproduces fundamental vector fields, and its equivariance makes this kernel invariant under the right $G$-action. Finally, the two constructions are inverse because both recover exactly the same horizontal subspace and vertical component.
[/proofplan]
[step:Identify vertical tangent vectors with Lie algebra elements]
For each $p \in P$, define the orbit map
\begin{align*}
a_p: G \to P, \quad h \mapsto p \cdot h.
\end{align*}
Its differential at the identity is the [linear map](/page/Linear%20Map)
\begin{align*}
d(a_p)_e: \mathfrak g \to T_pP, \quad \xi \mapsto (\xi_P)_p.
\end{align*}
Since $\nu(p \cdot h)=\nu(p)$ for every $h \in G$, the image of $d(a_p)_e$ lies in $V_pP := \ker d\nu_p$. In a local principal trivialization over a neighbourhood $U \subset M$ of $\nu(p)$, the bundle is identified with $U \times G$, the point $p$ is identified with $(x,h_0)$, and $a_p$ is identified with the map $k \mapsto (x,h_0k)$. Its differential identifies $T_eG=\mathfrak g$ isomorphically with the tangent space to the fibre $\{x\}\times G$. Hence
\begin{align*}
\theta_p: \mathfrak g \to V_pP, \quad \xi \mapsto (\xi_P)_p
\end{align*}
is a linear isomorphism for every $p \in P$.
[guided]
We first isolate the basic fact that makes connection forms possible: vertical tangent vectors are precisely infinitesimal group motions. Fix $p \in P$ and define the orbit map
\begin{align*}
a_p: G \to P, \quad h \mapsto p \cdot h.
\end{align*}
The differential of this map at the identity element $e \in G$ is
\begin{align*}
d(a_p)_e: T_eG \to T_pP.
\end{align*}
Since $T_eG=\mathfrak g$, and since the fundamental vector field associated to $\xi \in \mathfrak g$ is defined by differentiating the curve $t \mapsto p \cdot \exp(t\xi)$ at $t=0$, this differential is exactly
\begin{align*}
d(a_p)_e(\xi) = (\xi_P)_p.
\end{align*}
Why does this land in the vertical tangent space? The curve $t \mapsto p \cdot \exp(t\xi)$ lies entirely in the fibre over $\nu(p)$, because the right action preserves fibres:
\begin{align*}
\nu(p \cdot \exp(t\xi)) = \nu(p).
\end{align*}
Differentiating this constant curve in $M$ gives
\begin{align*}
d\nu_p((\xi_P)_p)=0.
\end{align*}
Thus $d(a_p)_e(\mathfrak g) \subseteq V_pP$, where $V_pP := \ker d\nu_p$.
It remains to know that every vertical tangent vector arises this way and that the Lie algebra element is unique. Choose a local principal trivialization over an open neighbourhood $U \subset M$ of $\nu(p)$. Under this trivialization, $P|_U$ is identified with $U \times G$, the point $p$ is identified with a point $(x,h_0)$, and the right action is identified with
\begin{align*}
(x,h)\cdot k = (x,hk).
\end{align*}
Therefore the orbit map $a_p$ becomes
\begin{align*}
k \mapsto (x,h_0k).
\end{align*}
The tangent space to the fibre through $(x,h_0)$ is the tangent space to $\{x\}\times G$, and the differential of right translation by $h_0$ identifies $T_eG$ isomorphically with that tangent space. Hence
\begin{align*}
\theta_p: \mathfrak g \to V_pP, \quad \xi \mapsto (\xi_P)_p
\end{align*}
is a linear isomorphism.
[/guided]
[/step]
[step:Construct a connection form from an invariant horizontal distribution]
Let $HP \subset TP$ be a principal connection. For each $p \in P$, let
\begin{align*}
\pi_p^V: T_pP \to V_pP
\end{align*}
denote the projection onto $V_pP := \ker d\nu_p$ along the direct sum decomposition $T_pP=H_pP\oplus V_pP$. Define
\begin{align*}
\omega_p: T_pP \to \mathfrak g, \quad X \mapsto \theta_p^{-1}(\pi_p^V X).
\end{align*}
Because $HP$ and $VP:=\ker d\nu$ are smooth subbundles, the projection $p \mapsto \pi_p^V$ is smooth, and because $p \mapsto \theta_p$ is the smooth infinitesimal action map, $\omega$ is a smooth $\mathfrak g$-valued $1$-form.
For reproduction, take $p \in P$ and $\xi \in \mathfrak g$. Since $(\xi_P)_p \in V_pP$, its vertical projection is itself, so
\begin{align*}
\omega_p((\xi_P)_p)=\theta_p^{-1}((\xi_P)_p)=\xi.
\end{align*}
It remains to verify equivariance. Fix $g \in G$. For $\xi \in \mathfrak g$, the transformation rule for fundamental vector fields under right translation is
\begin{align*}
d(R_g)_p((\xi_P)_p)=((\operatorname{Ad}_{g^{-1}}\xi)_P)_{p\cdot g}.
\end{align*}
Indeed, the left-hand side is the derivative at $t=0$ of $p\cdot \exp(t\xi)\cdot g$, and
\begin{align*}
p\cdot \exp(t\xi)\cdot g = p\cdot g\cdot g^{-1}\exp(t\xi)g = p\cdot g\cdot \exp(t\operatorname{Ad}_{g^{-1}}\xi).
\end{align*}
Thus differentiating at $t=0$ gives the displayed identity.
Now let $X \in T_pP$, and write $X=X^H+X^V$ with $X^H\in H_pP$ and $X^V\in V_pP$. Let $\xi=\omega_p(X)$, so $X^V=(\xi_P)_p$. Since $HP$ is right-invariant, $d(R_g)_pX^H\in H_{p\cdot g}P$, and since $R_g$ preserves fibres, $d(R_g)_pX^V\in V_{p\cdot g}P$. Therefore the vertical part of $d(R_g)_pX$ is $d(R_g)_pX^V$, and the preceding transformation rule gives
\begin{align*}
\omega_{p\cdot g}(d(R_g)_pX)=\operatorname{Ad}_{g^{-1}}\xi=\operatorname{Ad}_{g^{-1}}(\omega_p(X)).
\end{align*}
This is exactly $(R_g)^*\omega=\operatorname{Ad}_{g^{-1}}\omega$.
[/step]
[step:Construct an invariant horizontal distribution from a connection form]
Let $\omega \in \Omega^1(P;\mathfrak g)$ be a connection form. Define
\begin{align*}
H_pP := \ker \omega_p \subset T_pP
\end{align*}
for each $p \in P$. Since $\omega$ is smooth and since $\omega_p|_{V_pP}:V_pP\to \mathfrak g$ is inverse to $\theta_p$ by the reproduction property, $\omega_p$ has constant rank $\dim G$. Hence $HP=\ker\omega$ is a smooth subbundle of $TP$.
We prove that $H_pP$ is complementary to $V_pP$. If $X\in H_pP\cap V_pP$, then $X=(\xi_P)_p$ for a unique $\xi \in \mathfrak g$. Since $X\in \ker\omega_p$,
\begin{align*}
0=\omega_p(X)=\omega_p((\xi_P)_p)=\xi.
\end{align*}
Thus $X=0$, so $H_pP\cap V_pP=\{0\}$. Also $\omega_p:T_pP\to\mathfrak g$ is surjective because it maps $(\xi_P)_p$ to $\xi$ for every $\xi\in\mathfrak g$. Therefore
\begin{align*}
\dim H_pP = \dim T_pP-\dim\mathfrak g.
\end{align*}
Since $\dim V_pP=\dim\mathfrak g$, the zero intersection and the dimension count imply
\begin{align*}
T_pP=H_pP\oplus V_pP.
\end{align*}
Finally, $HP$ is right-invariant. If $X\in H_pP$, then $\omega_p(X)=0$. Using the equivariance of $\omega$,
\begin{align*}
\omega_{p\cdot g}(d(R_g)_pX)=\operatorname{Ad}_{g^{-1}}(\omega_p(X))=0.
\end{align*}
Thus $d(R_g)_pX\in H_{p\cdot g}P$, so
\begin{align*}
d(R_g)_p(H_pP)\subseteq H_{p\cdot g}P.
\end{align*}
Applying the same inclusion to $g^{-1}$ at the point $p\cdot g$ gives the reverse inclusion, hence
\begin{align*}
d(R_g)_p(H_pP)=H_{p\cdot g}P.
\end{align*}
[/step]
[step:Verify that the two constructions are inverse]
Start with a principal connection $HP$ and construct $\omega$ by
\begin{align*}
\omega_p(X)=\theta_p^{-1}(\pi_p^VX).
\end{align*}
The horizontal distribution recovered from $\omega$ is $\ker\omega$. For $X\in T_pP$,
\begin{align*}
\omega_p(X)=0
\end{align*}
if and only if
\begin{align*}
\pi_p^VX=0,
\end{align*}
which holds if and only if $X\in H_pP$. Hence the recovered horizontal distribution is the original one.
Conversely, start with a connection form $\omega$ and set $H_pP=\ker\omega_p$. Let $\pi_p^V:T_pP\to V_pP$ be the projection along $H_pP$. For any $X\in T_pP$, the vertical vector $\pi_p^VX$ has the form $(\xi_P)_p$ for the unique $\xi\in\mathfrak g$ satisfying $\xi=\theta_p^{-1}(\pi_p^VX)$. Since $X-\pi_p^VX\in H_pP=\ker\omega_p$, the reproduction property gives
\begin{align*}
\omega_p(X)=\omega_p(\pi_p^VX)=\omega_p((\xi_P)_p)=\xi.
\end{align*}
Thus the form reconstructed from the horizontal distribution is
\begin{align*}
X \mapsto \theta_p^{-1}(\pi_p^VX),
\end{align*}
which equals the original $\omega_p$. Therefore the two constructions are mutually inverse, giving the desired bijection.
[/step]
