[proofplan] We prove both directions using local sections. An existing $H$-reduction gives local sections of the reduced bundle, and the transition element between two such sections lies in the same $H$-torsor, hence belongs to $H$. Conversely, if the transition functions are $H$-valued, the local subbundles $V_a \times H$ glue inside the local trivialisations of $P$ to form a principal $H$-bundle $Q$. Finally, the extension of structure group $Q \times_H G$ is identified with the original principal $G$-bundle by the map induced from the right $G$-action on $P$. [/proofplan]

[step:Derive $H$-valued transition functions from an existing reduction] Assume first that $P$ admits an $H$-reduction. Thus there is a smooth principal right $H$-bundle $\rho: Q \to M$ and an $H$-equivariant smooth embedding $\iota: Q \hookrightarrow P$ over $M$ whose extension of structure group is isomorphic to $P$. Choose an open cover $(V_a)_{a \in A}$ of $M$ over which $Q$ admits smooth local sections. For each $a \in A$, let $t_a: V_a \to Q$ be a smooth local section of $\rho$, and define $s_a: V_a \to P$ by $s_a = \iota \circ t_a$. Since $\iota$ is a map over $M$, each $s_a$ is a smooth local section of $\pi: P \to M$. For $x \in V_a \cap V_b$, the points $t_a(x)$ and $t_b(x)$ lie in the same fiber $Q_x := \rho^{-1}(\{x\})$. Since $Q_x$ is a right $H$-torsor, there is a unique element $h_{ab}(x) \in H$ such that \begin{align*} t_b(x) = t_a(x) h_{ab}(x). \end{align*} The corresponding map $h_{ab}: V_a \cap V_b \to H$ is smooth because it is the transition function determined by the local sections $t_a$ and $t_b$ of the smooth principal $H$-bundle $Q$. Using $H$-equivariance of $\iota$, for every $x \in V_a \cap V_b$ we obtain \begin{align*} s_b(x) = \iota(t_b(x)) = \iota(t_a(x) h_{ab}(x)) = \iota(t_a(x)) h_{ab}(x) = s_a(x) h_{ab}(x). \end{align*} Thus the transition functions of $P$ with respect to the local sections $(s_a)_{a \in A}$ take values in $H$. [/step]

[step:Glue the local $H$-subbundles when the transition functions are $H$-valued]Conversely, assume there is an open cover $(V_a)_{a \in A}$ of $M$ and smooth local sections $s_a: V_a \to P$ such that the transition maps $g_{ab}: V_a \cap V_b \to G$ satisfy $s_b(x) = s_a(x)g_{ab}(x)$ and $g_{ab}(x) \in H$ for every $x \in V_a \cap V_b$. Since $H \subset G$ is an embedded Lie subgroup, the inclusion map $j: H \hookrightarrow G$ is a smooth embedding, and the $G$-valued smooth map $g_{ab}$ with image in $H$ has a unique corestriction $h_{ab}: V_a \cap V_b \to H$ satisfying $j \circ h_{ab} = g_{ab}$. In the embedded submanifold structure on $H$, this corestriction is smooth. Hence $s_b(x) = s_a(x)h_{ab}(x)$ with $h_{ab}$ smooth as an $H$-valued map. Define a subset $Q \subset P$ by \begin{align*} Q := \{s_a(x)h \in P : a \in A,\ x \in V_a,\ h \in H\}. \end{align*} This definition is independent of the chosen local section on overlaps: if $x \in V_a \cap V_b$ and $h \in H$, then \begin{align*} s_b(x)h = s_a(x)h_{ab}(x)h, \end{align*} and $h_{ab}(x)h \in H$ because $H$ is a subgroup of $G$. For each $a \in A$, define $\psi_a: V_a \times H \to Q \cap \pi^{-1}(V_a)$ by $\psi_a(x,h) = s_a(x)h$. The map $\psi_a$ is bijective: for fixed $x \in V_a$, the right $G$-action on $P_x$ is free, so $s_a(x)h_1 = s_a(x)h_2$ implies $h_1 = h_2$. For surjectivity, if $q \in Q \cap \pi^{-1}(V_a)$, then $q = s_b(x)h$ for some $b \in A$, some $x \in V_a \cap V_b$, and some $h \in H$; the overlap compatibility gives $q = s_a(x)h_{ab}(x)h$, with $h_{ab}(x)h \in H$. On an overlap $V_a \cap V_b$, the coordinate change is \begin{align*} \psi_a^{-1}(\psi_b(x,h)) = (x, h_{ab}(x)h). \end{align*} Indeed, \begin{align*} \psi_b(x,h) = s_b(x)h = s_a(x)h_{ab}(x)h = \psi_a(x,h_{ab}(x)h). \end{align*} Since $h_{ab}: V_a \cap V_b \to H$ is smooth by the embedded-subgroup corestriction argument above and multiplication in the Lie group $H$ is smooth, these coordinate changes are smooth. Therefore the charts $(\psi_a)_{a \in A}$ give $Q$ the structure of a smooth manifold for which $\rho := \pi|_Q: Q \to M$ is locally identified with the projection $V_a \times H \to V_a$. The right action of $H$ on $Q$ is the restriction of the right action of $G$ on $P$: \begin{align*} Q \times H \to Q, \qquad (q,k) \mapsto qk. \end{align*} In the chart $\psi_a$, this action is \begin{align*} (x,h)k = (x,hk), \end{align*} so it is smooth, free, and transitive on every fiber. Hence $\rho: Q \to M$ is a smooth principal right $H$-bundle.[/step]

[guided]The goal is to turn the condition "$h_{ab}$ takes values in $H$" into an actual subbundle of $P$. The natural candidate is: over each set $V_a$, keep only the points obtained from the local section $s_a$ by multiplying on the right by elements of $H$. Define \begin{align*} Q := \{s_a(x)h \in P : a \in A,\ x \in V_a,\ h \in H\}. \end{align*} This definition is compatible on overlaps because the transition functions are $H$-valued. If $x \in V_a \cap V_b$, then $s_b(x) = s_a(x)h_{ab}(x)$ with $h_{ab}(x) \in H$. Therefore \begin{align*} s_b(x)H = s_a(x)h_{ab}(x)H = s_a(x)H. \end{align*} So the subset of the fiber selected using $s_a$ is the same subset selected using $s_b$. For each $a \in A$, define $\psi_a: V_a \times H \to Q \cap \pi^{-1}(V_a)$ by $\psi_a(x,h) = s_a(x)h$. This map is injective because the right action of $G$ on a principal $G$-bundle is free: if $s_a(x)h_1 = s_a(x)h_2$, then $h_1 = h_2$. It is surjective by the definition of $Q$ over $V_a$. We also need the transition maps as $H$-valued smooth maps, not only as $G$-valued smooth maps. Let $j:H\hookrightarrow G$ be the embedded Lie subgroup inclusion. The transition map $g_{ab}:V_a\cap V_b\to G$ is smooth and has image in $H$, so there is a unique map $h_{ab}:V_a\cap V_b\to H$ with $j\circ h_{ab}=g_{ab}$. Smoothness of $h_{ab}$ follows locally from embedded-submanifold charts for $H\subset G$: in such charts, $H$ is cut out by setting the [normal coordinates](/theorems/2713) to zero, and a smooth map into $G$ whose image lies in $H$ has smooth tangential coordinate functions. Thus $h_{ab}$ is smooth as an $H$-valued map. Now compute the chart transition on $V_a \cap V_b$. Since $s_b(x) = s_a(x)h_{ab}(x)$, we have \begin{align*} \psi_b(x,h) = s_b(x)h = s_a(x)h_{ab}(x)h. \end{align*} Thus \begin{align*} \psi_a^{-1}(\psi_b(x,h)) = (x, h_{ab}(x)h). \end{align*} This is a smooth map from $(V_a \cap V_b) \times H$ to itself because $h_{ab}$ is smooth as a map into $H$ and multiplication $H \times H \to H$ is smooth. These transition maps therefore define a smooth manifold structure on $Q$. With this smooth structure, $\rho := \pi|_Q: Q \to M$ is locally the projection $V_a \times H \to V_a$. The right $H$-action on $Q$ is inherited from the right $G$-action on $P$, and in the local chart $\psi_a$ it is just \begin{align*} (x,h)k = (x,hk). \end{align*} This action is smooth, free, and transitive on each fiber because right multiplication in $H$ has those properties. Hence $Q \to M$ is a smooth principal right $H$-bundle.[/guided]

[step:Embed the glued $H$-bundle into $P$] Let $\iota: Q \to P$ be the inclusion map. By construction, $\pi \circ \iota = \rho$, so $\iota$ is a map over $M$. In the local chart $\psi_a: V_a \times H \to Q \cap \pi^{-1}(V_a)$ and the principal $G$-bundle trivialisation determined by $s_a$, the map $\iota$ is represented by the map $V_a \times H \to V_a \times G$ given by $(x,h) \mapsto (x,h)$. Since $H \subset G$ is an embedded Lie subgroup, this local representative is a smooth embedding. The property of being a smooth embedding is local on the source and target in compatible smooth charts, so these local representatives imply that $\iota: Q \hookrightarrow P$ is a smooth embedding. It is $H$-equivariant because both actions are restrictions of the right action on $P$: \begin{align*} \iota(qh) = \iota(q)h \end{align*} for every $q \in Q$ and $h \in H$. [/step]

[step:Identify the extension of structure group with the original bundle] Let $Q \times_H G$ denote the associated bundle formed using the left action of $H$ on $G$ by multiplication. Thus $(qh,g)$ is identified with $(q,hg)$ for $q \in Q$, $h \in H$, and $g \in G$. Define $F: Q \times_H G \to P$ by $F([q,g]) = qg$. This map is well-defined because \begin{align*} F([qh,g]) = qhg = F([q,hg]). \end{align*} It is smooth and right $G$-equivariant, where the right action on $Q \times_H G$ is $[q,g]k := [q,gk]$ and the right action on $P$ is the given principal action: \begin{align*} F([q,g]k) = F([q,gk]) = qgk = F([q,g])k. \end{align*} The map $F$ is surjective. If $p \in P$ and $x = \pi(p)$, choose $a \in A$ with $x \in V_a$. Since $s_a(x)$ lies in the same principal $G$-fiber as $p$, there is a unique $g \in G$ such that \begin{align*} p = s_a(x)g. \end{align*} Since $s_a(x) \in Q$, we have $p = F([s_a(x),g])$. The map $F$ is injective. Suppose $F([q_1,g_1]) = F([q_2,g_2])$. Put $x := \pi(q_1g_1) = \pi(q_2g_2)$, and choose $a \in A$ with $x \in V_a$. Since $q_1,q_2 \in Q_x$, there exist unique $h_1,h_2 \in H$ such that \begin{align*} q_1 = s_a(x)h_1 \end{align*} and \begin{align*} q_2 = s_a(x)h_2. \end{align*} The equality $q_1g_1 = q_2g_2$ becomes \begin{align*} s_a(x)h_1g_1 = s_a(x)h_2g_2. \end{align*} Freeness of the right $G$-action gives \begin{align*} h_1g_1 = h_2g_2. \end{align*} Using the defining [equivalence relation](/page/Equivalence%20Relation) in $Q \times_H G$, we get \begin{align*} [q_1,g_1] = [s_a(x)h_1,g_1] = [s_a(x),h_1g_1] = [s_a(x),h_2g_2] = [s_a(x)h_2,g_2] = [q_2,g_2]. \end{align*} Thus $F$ is injective. Finally, in the local trivialisation over $V_a$, every element of $Q \times_H G$ is represented uniquely as $[s_a(x),g]$, and $F$ sends it to $s_a(x)g$. Therefore locally $F$ is the identity map on $V_a \times G$. Hence $F$ is a diffeomorphism. We have constructed an $H$-reduction of $P$. [/step]

[step:Translate between sections and transition functions] Local sections of a principal bundle are equivalent to local trivialisations: a section $s_a: V_a \to P$ determines the trivialisation $V_a \times G \to \pi^{-1}(V_a)$ given by $(x,g) \mapsto s_a(x)g$. With respect to these trivialisations, the transition functions are precisely the maps $h_{ab}$ defined by $s_b(x) = s_a(x)h_{ab}(x)$. Therefore the existence of local sections with $H$-valued transition maps is exactly the statement that, after refining the cover and changing local trivialisations if necessary, the transition functions of $P$ take values in $H$. Combining the two directions proves the claimed equivalence. [/step]