[proofplan] The flatness hypothesis says that the horizontal distribution is involutive, by the curvature-as-obstruction formula for brackets of horizontal vector fields. Frobenius then gives local horizontal integral manifolds in $P$. Around a chosen point $p_0\in P_x$, one such horizontal leaf projects diffeomorphically onto a small neighbourhood $U$ of $x$; principal equivariance transports this sheet to compatible horizontal sheets through every point of the reference fibre. A horizontal lift of any path in $U$ is forced by uniqueness to lie in the corresponding sheet, so its endpoint is determined only by the endpoint in the base. [/proofplan] [step:Convert flatness into local horizontal integral manifolds] For each $p\in P$, let $\mathcal{V}_p:=\ker d\pi_p\subset T_pP$ denote the vertical tangent space. Since $\mathcal{H}$ is a principal connection, each tangent space decomposes as \begin{align*} T_pP=\mathcal{H}_p\oplus \mathcal{V}_p, \end{align*} and the restriction $d\pi_p|_{\mathcal{H}_p}:\mathcal{H}_p\to T_{\pi(p)}M$ is a linear isomorphism. Because the curvature of $\mathcal{H}$ vanishes identically, the standard curvature-as-obstruction formula for principal connections implies that $\mathcal{H}$ is involutive: whenever $X,Y$ are smooth vector fields on an open subset of $P$ with $X_p,Y_p\in \mathcal{H}_p$ at every point where they are defined, the bracket satisfies $[X,Y]_p\in \mathcal{H}_p$. Here we are citing a result not yet in the wiki: the curvature-as-obstruction formula for brackets of horizontal vector fields. By the Frobenius theorem for involutive distributions, cited here as a result not yet in the wiki, for every $p\in P$ there is an immersed submanifold $L_p\subset P$ through $p$ such that \begin{align*} T_qL_p=\mathcal{H}_q \end{align*} for every $q\in L_p$ after restricting to a sufficiently small neighbourhood of $p$ inside the leaf. Thus $\mathcal{H}$ has local horizontal integral manifolds through every point of $P$. [guided] We first translate the analytic condition "flat connection" into the geometric condition needed for Frobenius. For each $p\in P$, define the vertical tangent space by \begin{align*} \mathcal{V}_p:=\ker d\pi_p\subset T_pP. \end{align*} A principal connection is precisely a smooth choice of horizontal subspaces $\mathcal{H}_p\subset T_pP$ complementary to the vertical spaces, so \begin{align*} T_pP=\mathcal{H}_p\oplus \mathcal{V}_p. \end{align*} This complement condition implies that $d\pi_p$ restricts to a linear isomorphism \begin{align*} d\pi_p|_{\mathcal{H}_p}:\mathcal{H}_p\to T_{\pi(p)}M. \end{align*} The reason is that the kernel of $d\pi_p$ is exactly $\mathcal{V}_p$, so $d\pi_p$ is injective on the complementary subspace $\mathcal{H}_p$; the dimensions match because $\dim \mathcal{H}_p=\dim M$. Now we use flatness. The curvature of a principal connection measures exactly the vertical component of the bracket of horizontal vector fields. Therefore, when the curvature vanishes identically, the bracket of two horizontal vector fields is again horizontal. More explicitly, if $X$ and $Y$ are smooth vector fields on an open subset of $P$ and satisfy $X_p,Y_p\in\mathcal{H}_p$ everywhere on their domain, then \begin{align*} [X,Y]_p\in\mathcal{H}_p. \end{align*} This is the standard curvature-as-obstruction formula for principal connections; we are citing a result not yet in the wiki: the curvature-as-obstruction formula for brackets of horizontal vector fields. This is exactly the hypothesis needed for Frobenius. By the Frobenius theorem for involutive distributions, also cited here as a result not yet in the wiki, an involutive smooth distribution is locally tangent to immersed integral submanifolds. Applying it to the distribution $\mathcal{H}\subset TP$, we obtain that for every $p\in P$ there is a local immersed submanifold $L_p\subset P$ through $p$ satisfying \begin{align*} T_qL_p=\mathcal{H}_q \end{align*} for every point $q$ of the local leaf. These leaves are the horizontal sheets along which parallel transport will become path-independent. [/guided] [/step] [step:Choose one horizontal sheet projecting diffeomorphically to the base] Fix $x\in M$, and choose $p_0\in P_x$. Let $L_0\subset P$ be a local horizontal integral manifold through $p_0$, so $T_{p_0}L_0=\mathcal{H}_{p_0}$. The differential of the restricted projection \begin{align*} \pi|_{L_0}:L_0\to M \end{align*} at $p_0$ is the isomorphism $d\pi_{p_0}|_{\mathcal{H}_{p_0}}:\mathcal{H}_{p_0}\to T_xM$. By the [inverse function theorem](/theorems/51), after replacing $L_0$ by a smaller open neighbourhood of $p_0$ inside the leaf, there is an open neighbourhood $U_0\subset M$ of $x$ such that \begin{align*} \pi|_{L_0}:L_0\to U_0 \end{align*} is a diffeomorphism. Choose a coordinate chart $(W,\varphi)$ on $M$ with $x\in W\subset U_0$. Shrink $W$ to a coordinate ball around $x$ and denote the resulting path-connected [open set](/page/Open%20Set) by $U$. Replace $L_0$ by $(\pi|_{L_0})^{-1}(U)$. Then \begin{align*} \pi|_{L_0}:L_0\to U \end{align*} is a diffeomorphism and $L_0$ remains tangent to $\mathcal{H}$ at every point. Define the smooth section $\sigma:U\to P$ by \begin{align*} \sigma=(\pi|_{L_0})^{-1}. \end{align*} Since $d\sigma_y(T_yM)=T_{\sigma(y)}L_0=\mathcal{H}_{\sigma(y)}$ for each $y\in U$, the section $\sigma$ is horizontal in the sense that its image is tangent to the connection. [/step] [step:Transport the horizontal sheet by the principal action] For each $g\in G$, let $R_g:P\to P$ denote the principal right action map $R_g(p)=p g$. Since $\mathcal{H}$ is a principal connection, it is $G$-equivariant: \begin{align*} d(R_g)_p(\mathcal{H}_p)=\mathcal{H}_{p g}. \end{align*} Define the translated horizontal sheet $L_g:=R_g(L_0)\subset P$. Because $\pi\circ R_g=\pi$, the restriction \begin{align*} \pi|_{L_g}:L_g\to U \end{align*} is a diffeomorphism. Define $\sigma_g:U\to P$ by $\sigma_g(y)=\sigma(y)g$. Then $\sigma_g(U)=L_g$ and $d\sigma_g(TU)\subset \mathcal{H}$. For every $y\in U$ and every $q\in P_y$, there is a unique $g\in G$ such that \begin{align*} q=\sigma(y)g. \end{align*} Existence and uniqueness follow from the fact that the principal right action of $G$ on each fibre $P_y$ is free and transitive. Hence the family of horizontal sheets $(L_g)_{g\in G}$ covers $\pi^{-1}(U)$, and each point of $\pi^{-1}(U)$ lies on exactly one such sheet. [/step] [step:Show every horizontal lift inside $U$ remains in its sheet] Let $a,b\in U$, let $\gamma:[0,1]\to U$ be a smooth path with $\gamma(0)=a$ and $\gamma(1)=b$, and let $q\in P_a$. Choose the unique $g\in G$ such that $q=\sigma(a)g$. Define a smooth curve $\widetilde{\gamma}_g:[0,1]\to P$ by \begin{align*} \widetilde{\gamma}_g(t)=\sigma(\gamma(t))g. \end{align*} Then $\pi(\widetilde{\gamma}_g(t))=\gamma(t)$ for every $t\in[0,1]$, and $\widetilde{\gamma}_g(0)=q$. Moreover, \begin{align*} \dot{\widetilde{\gamma}}_g(t)=d\sigma_g|_{\gamma(t)}(\dot{\gamma}(t))\in \mathcal{H}_{\widetilde{\gamma}_g(t)}. \end{align*} Thus $\widetilde{\gamma}_g$ is a horizontal lift of $\gamma$ starting at $q$. By uniqueness of horizontal lifts for an Ehresmann connection along a fixed smooth path, the parallel transport lift of $\gamma$ starting at $q$ is exactly $\widetilde{\gamma}_g$. Therefore \begin{align*} \tau_\gamma(q)=\widetilde{\gamma}_g(1)=\sigma(b)g. \end{align*} The expression $\sigma(b)g$ depends on $q$ and $b$, through the unique element $g$ determined by $q=\sigma(a)g$, but it does not depend on the path $\gamma$. [/step] [step:Conclude that parallel transport depends only on endpoints in the chosen neighbourhood] Let $\gamma_0,\gamma_1:[0,1]\to U$ be smooth paths with $\gamma_j(0)=a$ and $\gamma_j(1)=b$. For an arbitrary $q\in P_a$, let $g\in G$ be the unique element satisfying $q=\sigma(a)g$. Applying the previous step to each path gives \begin{align*} \tau_{\gamma_0}(q)=\sigma(b)g \end{align*} and \begin{align*} \tau_{\gamma_1}(q)=\sigma(b)g. \end{align*} Hence $\tau_{\gamma_0}(q)=\tau_{\gamma_1}(q)$ for every $q\in P_a$, so \begin{align*} \tau_{\gamma_0}=\tau_{\gamma_1}:P_a\to P_b. \end{align*} Since $a,b\in U$ and the two smooth paths in $U$ were arbitrary, parallel transport over $U$ is independent of the smooth path joining the prescribed endpoints. This proves the theorem. [/step]