[proofplan] We construct the total space by gluing the trivial bundles $U_i \times G$ along the prescribed transition functions. The cocycle identities make the gluing relation an [equivalence relation](/page/Equivalence%20Relation), and the quotient inherits local trivializations from the pieces $U_i \times G$. These trivializations define the smooth structure, the projection, the right $G$-action, and the local sections. Finally, any other principal bundle with the same transition functions receives a canonical map from the glued bundle, and the same compatibility identity proves that this map is independent of the chosen trivializing index. [/proofplan]

[step:Glue the local trivial bundles by the transition functions] Let \begin{align*} E := \bigsqcup_{i \in I} (U_i \times G) \end{align*} be the disjoint union of smooth manifolds, and write $(x,h)_i$ for the point in the $i$-th summand with $x \in U_i$ and $h \in G$. Define a relation $\sim$ on $E$ by declaring \begin{align*} (x,h)_j \sim (x, g_{ij}(x)h)_i \end{align*} whenever $x \in U_i \cap U_j$ and $h \in G$, and then equivalently by the explicit condition \begin{align*} (x,h)_i \sim (y,k)_j \quad \Longleftrightarrow \quad x = y \in U_i \cap U_j \text{ and } k = g_{ji}(x)h. \end{align*} We verify that $\sim$ is an equivalence relation. Reflexivity follows from $g_{ii}(x)=e$, because \begin{align*} h = g_{ii}(x)h. \end{align*} Symmetry follows from $g_{ij}(x)^{-1}=g_{ji}(x)$. Indeed, if $k=g_{ji}(x)h$, then \begin{align*} h = g_{ij}(x)k. \end{align*} For transitivity, suppose \begin{align*} (x,h)_i \sim (x,k)_j \end{align*} and \begin{align*} (x,k)_j \sim (x,\ell)_m. \end{align*} Then $x \in U_i \cap U_j \cap U_m$, \begin{align*} k = g_{ji}(x)h \end{align*} and \begin{align*} \ell = g_{mj}(x)k. \end{align*} Substituting the first identity into the second and using the cocycle identity with indices $m,j,i$ gives \begin{align*} \ell = g_{mj}(x)g_{ji}(x)h = g_{mi}(x)h. \end{align*} Hence $(x,h)_i \sim (x,\ell)_m$. Let \begin{align*} P := E/{\sim} \end{align*} be the quotient set, and denote the equivalence class of $(x,h)_i$ by $[(x,h)_i]$. [/step]

[step:Define the projection and the local trivializations] Define $\rho:P \to M$ by \begin{align*} \rho([(x,h)_i]) := x. \end{align*} This is well-defined because equivalent points have the same base point by the definition of $\sim$. For each $i \in I$, define $\Phi_i: \rho^{-1}(U_i) \to U_i \times G$ by \begin{align*} \Phi_i([(x,h)_i]) := (x,h). \end{align*} This map is well-defined on $\rho^{-1}(U_i)$ as follows. If the same class is represented by $(x,k)_j$ with $x \in U_i \cap U_j$, then the defining relation gives \begin{align*} (x,k)_j \sim (x,g_{ij}(x)k)_i, \end{align*} so the representative in the $i$-th chart is uniquely $(x,g_{ij}(x)k)_i$. The inverse map $\Psi_i: U_i \times G \to \rho^{-1}(U_i)$ is defined by \begin{align*} \Psi_i(x,h) := [(x,h)_i]. \end{align*} The identities $\Phi_i \circ \Psi_i = \operatorname{id}_{U_i \times G}$ and $\Psi_i \circ \Phi_i = \operatorname{id}_{\rho^{-1}(U_i)}$ follow directly from the definitions, so $\Phi_i$ is a bijection. On an overlap $U_i \cap U_j$, the coordinate transition map \begin{align*} \Phi_i \circ \Phi_j^{-1}: (U_i \cap U_j) \times G &\to (U_i \cap U_j) \times G \end{align*} is given by \begin{align*} (x,h) \mapsto (x,g_{ij}(x)h). \end{align*} This map is smooth because $g_{ij}:U_i \cap U_j \to G$ is smooth and multiplication \begin{align*} G \times G \to G \end{align*} in the Lie group $G$ is smooth. Its inverse is \begin{align*} (x,h) \mapsto (x,g_{ji}(x)h), \end{align*} which is smooth for the same reason. Declare a subset $A \subset P$ to be open if and only if $\Phi_i(A \cap \rho^{-1}(U_i))$ is open in $U_i \times G$ for every $i \in I$. We will apply the standard smooth manifold atlas construction theorem: a set equipped with bijective charts to open subsets of Euclidean-space manifolds, smooth transition maps, and a Hausdorff second countable chart topology has a unique smooth manifold structure for which those charts are diffeomorphisms. The transition maps computed above are smooth diffeomorphisms, so it remains only to verify the Hausdorff and second countability axioms for this chart topology. The topology is Hausdorff. Let $p,q \in P$ be distinct. If $\rho(p) \neq \rho(q)$, choose disjoint open neighbourhoods $V,W \subset M$ of $\rho(p)$ and $\rho(q)$, respectively, using that the smooth manifold $M$ is Hausdorff. Since $\rho$ is locally the projection $U_i \times G \to U_i$, the sets $\rho^{-1}(V)$ and $\rho^{-1}(W)$ are open in $P$ and separate $p$ from $q$. If $\rho(p)=\rho(q)=x$, choose $i \in I$ with $x \in U_i$. Then $p,q \in \rho^{-1}(U_i)$, and $\Phi_i(p) \neq \Phi_i(q)$ in the Hausdorff manifold $U_i \times G$; disjoint open neighbourhoods of $\Phi_i(p)$ and $\Phi_i(q)$ pull back under $\Phi_i$ to disjoint open neighbourhoods of $p$ and $q$. The topology is second countable. Since $M$ is second countable, every open cover of $M$ has a countable subcover; choose a countable subset $J \subset I$ such that $(U_j)_{j \in J}$ still covers $M$. For each $j \in J$, let $\mathcal{B}_j$ be a countable basis of the second countable manifold $U_j \times G$. Then \begin{align*} \mathcal{B} := \{\Phi_j^{-1}(B) : j \in J \text{ and } B \in \mathcal{B}_j\} \end{align*} is countable. It is a basis for $P$: if $A \subset P$ is open and $p \in A$, choose $j \in J$ with $\rho(p) \in U_j$; then $\Phi_j(A \cap \rho^{-1}(U_j))$ is open in $U_j \times G$, so some $B \in \mathcal{B}_j$ satisfies $\Phi_j(p) \in B \subset \Phi_j(A \cap \rho^{-1}(U_j))$, hence $p \in \Phi_j^{-1}(B) \subset A$. Therefore $P$ is a smooth manifold and each $\Phi_i$ is a diffeomorphism onto $U_i \times G$. Since $\rho$ is expressed in the chart $\Phi_i$ as the projection $U_i \times G \to U_i$, namely $(x,h) \mapsto x$, the map $\rho:P \to M$ is smooth. [/step]

[step:Construct the principal right action and verify local triviality]Define a right action of $G$ on $P$ by the map $P \times G \to P$ given by \begin{align*} ([(x,h)_i],k) \mapsto [(x,hk)_i]. \end{align*} This is well-defined. If $(x,h)_i \sim (x,h')_j$, then $h' = g_{ji}(x)h$, and hence \begin{align*} h'k = g_{ji}(x)hk. \end{align*} Therefore $(x,hk)_i \sim (x,h'k)_j$. The action laws follow from associativity and the identity element in $G$: \begin{align*} ([(x,h)_i]k_1)k_2 = [(x,hk_1k_2)_i] = [(x,h)_i](k_1k_2) \end{align*} and \begin{align*} [(x,h)_i]e = [(x,h)_i]. \end{align*} In the local trivialization $\Phi_i$, this action is the standard right multiplication action $(U_i \times G) \times G \to U_i \times G$ given by \begin{align*} ((x,h),k) \mapsto (x,hk), \end{align*} so it is smooth. The same formula shows that each $\Phi_i$ is $G$-equivariant, where $G$ acts on $U_i \times G$ by right multiplication on the second factor. The action is free and transitive on each fiber. Indeed, in the chart $\Phi_i$, the fiber over $x \in U_i$ is identified with $\{x\} \times G$, and the action on this fiber is right multiplication on $G$. If $(x,h)k=(x,h)$, then $hk=h$, so $k=e$ by left multiplication by $h^{-1}$. If $(x,h_1),(x,h_2) \in \{x\} \times G$, then the unique element carrying $(x,h_1)$ to $(x,h_2)$ is $h_1^{-1}h_2$. Hence $\rho:P \to M$ is a smooth principal right $G$-bundle.[/step]

[guided]We must check that the quotient construction carries the standard principal right action. Define a map $P \times G \to P$ by \begin{align*} ([(x,h)_i],k) \mapsto [(x,hk)_i]. \end{align*} The first issue is independence of representatives. Suppose $(x,h)_i \sim (x,h')_j$. By the definition of the gluing relation, this means $x \in U_i \cap U_j$ and \begin{align*} h' = g_{ji}(x)h. \end{align*} Multiplying on the right by $k \in G$ gives \begin{align*} h'k = g_{ji}(x)hk, \end{align*} so $(x,hk)_i \sim (x,h'k)_j$. Thus the formula defines a well-defined map on equivalence classes. The action laws come directly from the group law in $G$. For $k_1,k_2 \in G$, \begin{align*} ([(x,h)_i]k_1)k_2 = [(x,hk_1k_2)_i] = [(x,h)_i](k_1k_2), \end{align*} and, writing $e \in G$ for the identity element, \begin{align*} [(x,h)_i]e = [(x,h)_i]. \end{align*} In the local trivialization $\Phi_i: \rho^{-1}(U_i) \to U_i \times G$, this action becomes \begin{align*} ((x,h),k) \mapsto (x,hk), \end{align*} which is smooth because multiplication in the Lie group $G$ is smooth. This also shows that $\Phi_i$ is $G$-equivariant when $U_i \times G$ carries right multiplication on its second factor. Finally, we verify the principal-bundle fiber condition. In the same local trivialization, the fiber over $x \in U_i$ is $\{x\} \times G$. Right multiplication by $G$ on itself is free: if $hk=h$, then left multiplication by $h^{-1}$ gives $k=e$. It is also transitive: given $h_1,h_2 \in G$, the unique element carrying $h_1$ to $h_2$ is $h_1^{-1}h_2$. Therefore the action is free and transitive on each fiber of $\rho$, and $\rho:P \to M$ is a smooth principal right $G$-bundle.[/guided]

[step:Recover the prescribed transition functions from the canonical sections] For each $i \in I$, define the local section $s_i: U_i \to P$ by \begin{align*} s_i(x) := [(x,e)_i]. \end{align*} In the local trivialization $\Phi_i$, this section is the map $x \mapsto (x,e)$, so $s_i$ is smooth and satisfies $\rho \circ s_i = \operatorname{id}_{U_i}$. If $x \in U_i \cap U_j$, then the defining relation gives \begin{align*} s_j(x) = [(x,e)_j] = [(x,g_{ij}(x))_i]. \end{align*} By the definition of the right action, \begin{align*} [(x,g_{ij}(x))_i] = [(x,e)_i]g_{ij}(x) = s_i(x)g_{ij}(x). \end{align*} Thus the transition functions of the local sections $(s_i)_{i \in I}$ are exactly the prescribed maps $g_{ij}$. [/step]

[step:Construct the unique isomorphism to any other bundle with the same transitions] Let \begin{align*} \pi: Q \to M \end{align*} be another smooth principal right $G$-bundle with smooth local sections \begin{align*} t_i: U_i \to Q \end{align*} satisfying \begin{align*} t_j(x) = t_i(x)g_{ij}(x) \end{align*} for every $x \in U_i \cap U_j$. Define $F:P \to Q$ by \begin{align*} F([(x,h)_i]) := t_i(x)h. \end{align*} This definition is independent of the representative. If $(x,h)_i \sim (x,k)_j$, then $k=g_{ji}(x)h$. Since $t_i(x)=t_j(x)g_{ji}(x)$, we obtain \begin{align*} t_j(x)k = t_j(x)g_{ji}(x)h = t_i(x)h. \end{align*} Hence $F([(x,h)_i])$ is well-defined. The map $F$ covers the identity on $M$, because \begin{align*} \pi(F([(x,h)_i])) = \pi(t_i(x)h) = x = \rho([(x,h)_i]). \end{align*} It is $G$-equivariant, since for every $k \in G$, \begin{align*} F([(x,h)_i]k) = F([(x,hk)_i]) = t_i(x)hk = F([(x,h)_i])k. \end{align*} In the local trivializations determined by $s_i$ on $P$ and $t_i$ on $Q$, the map $F$ is the identity map $U_i \times G \to U_i \times G$, namely $(x,h) \mapsto (x,h)$, so $F$ is smooth and locally a diffeomorphism. Its inverse is constructed in the same way from the sections $s_i$ and is also smooth. Therefore $F:P \to Q$ is a principal $G$-bundle isomorphism inducing $\operatorname{id}_M$. Finally, any principal bundle isomorphism $F:P \to Q$ covering $\operatorname{id}_M$ and satisfying $F \circ s_i=t_i$ must satisfy \begin{align*} F([(x,h)_i]) = F(s_i(x)h) = F(s_i(x))h = t_i(x)h. \end{align*} Thus the isomorphism is uniquely determined by the chosen local sections and the prescribed transition functions. This proves uniqueness up to principal bundle isomorphism over $M$. [/step]